diff --git a/tactic.ml b/tactic.ml
new file mode 100644
index 0000000..b5b76c9
--- /dev/null
+++ b/tactic.ml
@@ -0,0 +1,5 @@
+open Structs;;
+
+type tactic =
+  | Intro of var_lambda
+  | Assumption;;