Merge pull request #3003 from FStarLang/guido_tactics

Misc tactics improvements
FStarLang · Aug 4, 2023 · b02beda · b02beda
2 parents 928f044 + 448c037
commit b02beda
Show file tree

Hide file tree

Showing 17 changed files with 274 additions and 256 deletions.
diff --git a/ocaml/fstar-lib/FStar_Tactics_V1_Builtins.ml b/ocaml/fstar-lib/FStar_Tactics_V1_Builtins.ml
@@ -142,10 +142,3 @@ let ctrl_rewrite
     (t2 : unit -> unit __tac)
   : unit __tac
   = from_tac_3 CTRW.ctrl_rewrite d (to_tac_1 t1) (to_tac_0 (t2 ()))
-
-let log_issues (i:FStar_Issue.issue list)
-  : unit __tac
-  = fun ps ->
-       FStar_Errors.add_many i;
-       FStar_Tactics_Result.Success ((), ps)
-
diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml
diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Embedding.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Embedding.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Types.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Types.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml