From 6c7913c216f117d2069400d6dc81cbed407007e2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 26 Nov 2017 12:27:12 -0500 Subject: Add Tactics.RunTacticAsConstr --- src/Util/Tactics/RunTacticAsConstr.v | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 src/Util/Tactics/RunTacticAsConstr.v (limited to 'src/Util/Tactics') 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. -- cgit v1.2.3