Merge pull request #2871 from FStarLang/_aseem_2868

Removing with_type (and vcgen.optimize_bind_as_seq)
FStarLang · Apr 3, 2023 · 8db8d76 · 8db8d76
2 parents b9a9452 + bd30ab0
commit 8db8d76
Show file tree

Hide file tree

Showing 19 changed files with 339 additions and 768 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -546,6 +546,10 @@ Guidelines for the changelog:
      expected output location, we raise Warning 321.
 
 ## Command line options
+   * F* no longer supports the vcgen.optimize_bind_as_seq command line
+			  option for tweaking the verification condition generation.
+					The option was not on by-default, and hence was not maintained well.
+					Further, as issue #2868 observed, it relied on a strange SMT axiom.
 
    * [Issue #2385](https://github.com/FStarLang/FStar/issues/2385).
      The behavior of the --extract option was changed so that it no

diff --git a/ocaml/fstar-lib/generated/FStar_Options.ml b/ocaml/fstar-lib/generated/FStar_Options.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Pervasives.ml b/ocaml/fstar-lib/generated/FStar_Pervasives.ml
diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml