Treat must_erase_for_extraction as an alias for erasable.

FStarLang · Oct 2, 2024 · 7e628f2 · 7e628f2
1 parent 6c7225f
commit 7e628f2
Show file tree

Hide file tree

Showing 21 changed files with 177 additions and 331 deletions.
diff --git a/ocaml/fstar-lib/generated/FStar_GSet.ml b/ocaml/fstar-lib/generated/FStar_GSet.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Monotonic_HyperHeap.ml b/ocaml/fstar-lib/generated/FStar_Monotonic_HyperHeap.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Monotonic_HyperStack.ml b/ocaml/fstar-lib/generated/FStar_Monotonic_HyperStack.ml
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml