Add do_with_exactly_one_hyp

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.