1 files changed, 7 insertions, 0 deletions
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index 880f5824a..a318f469b 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -20,6 +20,13 @@ Ltac head expr :=
 
 Ltac head_hnf expr := let expr' := eval hnf in expr in head expr'.
 
+(** [contains x expr] succeeds iff [x] appears in [expr] *)
+Ltac contains search_for in_term :=
+  idtac;
+  lazymatch in_term with
+  | 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) :=