diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Util/Tactics/RunTacticAsConstr.v | 23 |
2 files changed, 24 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 6a1f9d0ed..c17bda2d7 100644 --- a/_CoqProject +++ b/_CoqProject @@ -5908,6 +5908,7 @@ src/Util/Tactics/PoseTermWithName.v src/Util/Tactics/PrintContext.v src/Util/Tactics/Revert.v src/Util/Tactics/RewriteHyp.v +src/Util/Tactics/RunTacticAsConstr.v src/Util/Tactics/SetEvars.v src/Util/Tactics/SetoidSubst.v src/Util/Tactics/SideConditionsBeforeToAfter.v 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. |