diff options
Diffstat (limited to 'src/Util/Tactics/DoWithHyp.v')
-rw-r--r-- | src/Util/Tactics/DoWithHyp.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/Util/Tactics/DoWithHyp.v b/src/Util/Tactics/DoWithHyp.v index b31072a63..3c068fe01 100644 --- a/src/Util/Tactics/DoWithHyp.v +++ b/src/Util/Tactics/DoWithHyp.v @@ -1,3 +1,4 @@ +Require Import Crypto.Util.Tactics.Not. Require Export Crypto.Util.FixCoqMistakes. (** Do something with every hypothesis. *) @@ -5,3 +6,13 @@ Ltac do_with_hyp' tac := match goal with | [ H : _ |- _ ] => tac H end. + +(** Do something with any hypothesis, as long as there is only one hypothesis that it works with *) +Ltac do_with_exactly_one_hyp tac := + match goal with + | [ H : _ |- _ ] + => not (idtac; match goal with + | [ H' : _ |- _ ] => tryif constr_eq H H' then fail else tac H' + end); + tac H + end. |