Add Tactics.RunTacticAsConstr

1 files changed, 23 insertions, 0 deletions

diff --git a/src/Util/Tactics/RunTacticAsConstr.v b/src/Util/Tactics/RunTacticAsConstr.v
new file mode 100644
index 000000000..d3d5ee096
--- /dev/null
+++ b/src/Util/Tactics/RunTacticAsConstr.v
@@ -0,0 +1,23 @@
+Require Export Crypto.Util.FixCoqMistakes.
+
+(** Runs a tactic during expression evaluation phase, returns the constr [I] *)
+Ltac run_tactic tac :=
+  let dummy := match goal with _ => tac () end in
+  I.
+
+(** Runs a tactic during expression evaluation phase, returning [true] on success and [false] on failure. *)
+Ltac run_tactic_as_bool tac :=
+  match goal with
+  | _ => let dummy := run_tactic tac in
+         true
+  | _ => false
+  end.
+
+(** Runs a tactic during expression evaluation phase; on success,
+    returns [then_tac ()], otherwise returns [else_tac ()] *)
+Ltac constr_tryif_then_else tac then_tac else_tac :=
+  let success := run_tactic_as_bool tac in
+  lazymatch success with
+  | true => then_tac ()
+  | false => else_tac ()
+  end.