1 files changed, 12 insertions, 0 deletions
diff --git a/tactics/Tauto.v b/tactics/Tauto.v
new file mode 100644
index 0000000000..2f7cbb0eac
--- /dev/null
+++ b/tactics/Tauto.v
@@ -0,0 +1,12 @@
+
+(* $Id$ *)
+
+Declare ML Module "Tauto".
+
+Grammar tactic simple_tactic :=
+  tauto [ "Tauto" ] -> [(Tauto)]
+| intuition [ "Intuition" ] -> [(Intuition)].
+
+Syntax tactic level 0:
+  tauto [(Tauto)] -> ["Tauto"]
+| intuition [(Intuition)] -> ["Intuition"].