Merge pull request #3460 from FStarLang/gebner_tactics_step

Add normalization step for tactics.
FStarLang · Sep 11, 2024 · 309b2d6 · 309b2d6
2 parents ef93b7d + 084979d
commit 309b2d6
Show file tree

Hide file tree

Showing 62 changed files with 43,483 additions and 38,644 deletions.
diff --git a/ocaml/fstar-lib/generated/FStar_Error.ml b/ocaml/fstar-lib/generated/FStar_Error.ml
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Base.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Base.ml
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Effectful.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Effectful.ml
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_ExploreTerm.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_ExploreTerm.ml
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Output.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Output.ml
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_PostProcess.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_PostProcess.ml
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Propositions.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Propositions.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Pure_BreakVC.ml b/ocaml/fstar-lib/generated/FStar_Pure_BreakVC.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_V1_Embeddings.ml b/ocaml/fstar-lib/generated/FStar_Reflection_V1_Embeddings.ml