Fix recordgen

upamanyus · upamanyus · commit 307188828000 · 2025-01-15T15:50:55.000-05:00
diff --git a/recordgen/recordgen.go b/recordgen/recordgen.go
@@ -178,7 +178,7 @@ Admitted.
 					for i := 0; i < s.NumFields(); i++ {
 						fmt.Fprintf(w, " %s", toCoqName(s.Field(i).Name()))
 					}
-					fmt.Fprintf(w, ":\n  PureWp True\n    (struct.make %s (struct.fields_val [", name)
+					fmt.Fprintf(w, ":\n  PureWp True\n    (struct.make %s (alist_val [", name)
 					sep := ""
 					for i := 0; i < s.NumFields(); i++ {
 						fmt.Fprintf(w, "%s\n      \"%s\" ::= #%s", sep, s.Field(i).Name(), toCoqName(s.Field(i).Name()))

Original file line number	Diff line number	Diff line change
`@@ -178,7 +178,7 @@ Admitted.`
`178`	`178`	`for i := 0; i < s.NumFields(); i++ {`
`179`	`179`	`fmt.Fprintf(w, " %s", toCoqName(s.Field(i).Name()))`
`180`	`180`	`}`
`181`		`- fmt.Fprintf(w, ":\n PureWp True\n (struct.make %s (struct.fields_val [", name)`
	`181`	`+ fmt.Fprintf(w, ":\n PureWp True\n (struct.make %s (alist_val [", name)`
`182`	`182`	`sep := ""`
`183`	`183`	`for i := 0; i < s.NumFields(); i++ {`
`184`	`184`	`fmt.Fprintf(w, "%s\n \"%s\" ::= #%s", sep, s.Field(i).Name(), toCoqName(s.Field(i).Name()))`