From fd02de94fdbd176dc6b7f731e357c0d0d96014a6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 29 Aug 2018 17:17:26 -0400 Subject: Add do_with_exactly_one_hyp --- src/Util/Tactics/DoWithHyp.v | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'src') 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. -- cgit v1.2.3