diff options
Diffstat (limited to 'src/Util/Tactics.v')
-rw-r--r-- | src/Util/Tactics.v | 25 |
1 files changed, 1 insertions, 24 deletions
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) |