add dep on all idents, regardless of IsMacro

goose.go

@@ -1070,8 +1070,8 @@ func (ctx Ctx) unaryExpr(e *ast.UnaryExpr) coq.Expr {
 
 func (ctx Ctx) variable(s *ast.Ident) coq.Expr {
 	info := ctx.identInfo(s)
+	ctx.dep.addDep(s.Name)
 	if info.IsMacro {
-		ctx.dep.addDep(s.Name)
 		return coq.GallinaIdent(s.Name)
 	}
 	e := coq.IdentExpr(s.Name)

interface.go

@@ -78,7 +78,7 @@ func (ctx Ctx) Decls(fs ...NamedFile) (imports coq.ImportDecls, decls []coq.Decl
 				errs = append(errs, err)
 			}
 
-			// fmt.Printf("Generated %s, depends on %s\n", ctx.dep.names, ctx.dep.deps)
+			// fmt.Printf("%s depends on %s\n", ctx.dep.names, ctx.dep.deps)
 
 			declGroups[id] = newDecls
 			declDeps[id] = ctx.dep.deps

internal/examples/simpledb/simpledb.gold.v

@@ -94,6 +94,19 @@ Definition lazyFileBuf := struct.decl [
   "next" :: slice.T byteT
 ].
 
+Definition bufFile := struct.decl [
+  "file" :: fileT;
+  "buf" :: ptrT
+].
+
+Definition newBuf: val :=
+  rec: "newBuf" "f" :=
+    let: "buf" := ref (zero_val (slice.T byteT)) in
+    struct.mk bufFile [
+      "file" ::= "f";
+      "buf" ::= "buf"
+    ].
+
 (* readTableIndex parses a complete table on disk into a key->offset index *)
 Definition readTableIndex: val :=
   rec: "readTableIndex" "f" "index" :=
@@ -163,19 +176,6 @@ Definition tableRead: val :=
       let: "p" := readValue (struct.get Table "File" "t") "off" in
       ("p", #true)).
 
-Definition bufFile := struct.decl [
-  "file" :: fileT;
-  "buf" :: ptrT
-].
-
-Definition newBuf: val :=
-  rec: "newBuf" "f" :=
-    let: "buf" := ref (zero_val (slice.T byteT)) in
-    struct.mk bufFile [
-      "file" ::= "f";
-      "buf" ::= "buf"
-    ].
-
 Definition bufFlush: val :=
   rec: "bufFlush" "f" :=
     let: "buf" := ![slice.T byteT] (struct.get bufFile "buf" "f") in