1 files changed, 13 insertions, 0 deletions
diff --git a/src/Util/Tactics/Contains.v b/src/Util/Tactics/Contains.v
new file mode 100644
index 000000000..aa4fddac2
--- /dev/null
+++ b/src/Util/Tactics/Contains.v
@@ -0,0 +1,13 @@
+(** [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.
+
+Ltac free_in x y :=
+  idtac;
+  match y with
+    | appcontext[x] => fail 1 x "appears in" y
+    | _ => idtac
+  end.