Merge pull request #3436 from mtzguido/shortcircuit

Fixing short circuting operators when --admit
FStarLang · Sep 5, 2024 · c3311e1 · c3311e1
2 parents a2e12be + 460bffd
commit c3311e1
Show file tree

Hide file tree

Showing 15 changed files with 270 additions and 138 deletions.
diff --git a/ocaml/fstar-lib/generated/FStar_Class_PP.ml b/ocaml/fstar-lib/generated/FStar_Class_PP.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml
diff --git a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Err.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Err.ml
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml