Merge pull request #2928 from FStarLang/_aseem_named_records

Use named records in data constructors for some syntax classes
FStarLang · May 15, 2023 · 31e595d · 31e595d
2 parents 2c89426 + 9eb2df7
commit 31e595d
Show file tree

Hide file tree

Showing 94 changed files with 10,877 additions and 5,183 deletions.
diff --git a/examples/hello/TestSeq/TestSeq.fst.hints b/examples/hello/TestSeq/TestSeq.fst.hints
diff --git a/examples/miniparse/MiniParseExample.fst b/examples/miniparse/MiniParseExample.fst
@@ -21,7 +21,7 @@ module T = FStar.Tactics
 
 // #set-options "--no_smt"
 
-#set-options "--z3rlimit 32"
+#set-options "--z3rlimit 128 --fuel 2 --ifuel 1"
 
 let p = T.synth_by_tactic (fun () -> gen_enum_parser T.SMT (`test))
 
@@ -33,4 +33,4 @@ let q = T.synth_by_tactic (fun () -> gen_parser_impl T.Goal)
 let q' : parser_impl p = T.synth_by_tactic (fun () -> gen_parser_impl T.SMT)
 
 #reset-options
- 
+
diff --git a/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml b/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Util.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Util.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Interactive_Ide.ml b/ocaml/fstar-lib/generated/FStar_Interactive_Ide.ml