diff options
Diffstat (limited to 'src/Util/Tactics/RunTacticAsConstr.v')
-rw-r--r-- | src/Util/Tactics/RunTacticAsConstr.v | 23 |
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. |