From 72efe58cb53c46b9ca8e7b133e9786f0ca8d0c43 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 31 Jan 2017 19:51:17 -0500 Subject: Split off unique {pose,assert} --- src/Util/Tactics.v | 25 +------------------------ 1 file changed, 1 insertion(+), 24 deletions(-) (limited to 'src/Util/Tactics.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) -- cgit v1.2.3