diff options
author | Jason Gross <jgross@mit.edu> | 2017-11-26 12:27:12 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-11-26 12:27:48 -0500 |
commit | 6c7913c216f117d2069400d6dc81cbed407007e2 (patch) | |
tree | 0ac0fe3b2ea4913498f2ecafd0c4312d0c7c59b2 /src/Util/Tactics/RunTacticAsConstr.v | |
parent | 43d6b87a35f75f1684ce5d605296203009cf299a (diff) |
Add Tactics.RunTacticAsConstr
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. |