diff options
author | Jason Gross <jagro@google.com> | 2018-08-29 17:17:26 -0400 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2018-08-29 17:17:26 -0400 |
commit | fd02de94fdbd176dc6b7f731e357c0d0d96014a6 (patch) | |
tree | 98e42db0f7e3a7ed2cf52afd48ed38236d902235 /src/Util/Tactics/DoWithHyp.v | |
parent | 673534439ac5002e995ebcf49ea640692c83f2d8 (diff) |
Add do_with_exactly_one_hyp
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. |