3 files changed, 35 insertions, 24 deletions
diff --git a/_CoqProject b/_CoqProject
index 3722bd752..513c2f7c6 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -409,4 +409,5 @@ src/Util/Tactics/Head.v
 src/Util/Tactics/RewriteHyp.v
 src/Util/Tactics/SpecializeBy.v
 src/Util/Tactics/SplitInContext.v
+src/Util/Tactics/UniquePose.v
 src/WeierstrassCurve/Pre.v
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index dffd6e581..f76660830 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -8,6 +8,7 @@ Require Export Crypto.Util.Tactics.DoWithHyp.
 Require Export Crypto.Util.Tactics.RewriteHyp.
 Require Export Crypto.Util.Tactics.SpecializeBy.
 Require Export Crypto.Util.Tactics.SplitInContext.
+Require Export Crypto.Util.Tactics.UniquePose.
 
 (** Test if a tactic succeeds, but always roll-back the results *)
 Tactic Notation "test" tactic3(tac) :=
@@ -26,30 +27,6 @@ Ltac contains search_for in_term :=
   | appcontext[search_for] => idtac
   end.
 
-(* [pose proof defn], but only if no hypothesis of the same type exists.
-   most useful for proofs of a proposition *)
-Tactic Notation "unique" "pose" "proof" constr(defn) :=
-  let T := type of defn in
-  match goal with
-  | [ H : T |- _ ] => fail 1
-  | _ => pose proof defn
-  end.
-(* [assert T], but only if no hypothesis of the same type exists.
-   most useful for proofs of a proposition *)
-Tactic Notation "unique" "assert" constr(T) :=
-  match goal with
-  | [ H : T |- _ ] => fail 1
-  | _ => assert T
-  end.
-
-(* [assert T], but only if no hypothesis of the same type exists.
-   most useful for proofs of a proposition *)
-Tactic Notation "unique" "assert" constr(T) "by" tactic3(tac) :=
-  match goal with
-  | [ H : T |- _ ] => fail 1
-  | _ => assert T by tac
-  end.
-
 Ltac set_evars :=
   repeat match goal with
          | [ |- appcontext[?E] ] => is_evar E; let e := fresh "e" in set (e := E)
diff --git a/src/Util/Tactics/UniquePose.v b/src/Util/Tactics/UniquePose.v
new file mode 100644
index 000000000..da6c6974e
--- /dev/null
+++ b/src/Util/Tactics/UniquePose.v
@@ -0,0 +1,33 @@
+Require Export Crypto.Util.FixCoqMistakes.
+
+(** [pose proof defn], but only if no hypothesis of the same type exists.
+    most useful for proofs of a proposition *)
+Tactic Notation "unique" "pose" "proof" constr(defn) :=
+  let T := type of defn in
+  match goal with
+  | [ H : T |- _ ] => fail 1
+  | _ => pose proof defn
+  end.
+
+(** [pose defn], but only if that hypothesis doesn't exist *)
+Tactic Notation "unique" "pose" constr(defn) :=
+  lazymatch goal with
+  | [ H := defn |- _ ] => fail
+  | _ => pose defn
+  end.
+
+(** [assert T], but only if no hypothesis of the same type exists.
+    most useful for proofs of a proposition *)
+Tactic Notation "unique" "assert" constr(T) :=
+  match goal with
+  | [ H : T |- _ ] => fail 1
+  | _ => assert T
+  end.
+
+(** [assert T], but only if no hypothesis of the same type exists.
+    most useful for proofs of a proposition *)
+Tactic Notation "unique" "assert" constr(T) "by" tactic3(tac) :=
+  match goal with
+  | [ H : T |- _ ] => fail 1
+  | _ => assert T by tac
+  end.