aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/Tauto.v
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/Tauto.v')
-rw-r--r--tactics/Tauto.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/Tauto.v b/tactics/Tauto.v
index 2f4475057..c6283109c 100644
--- a/tactics/Tauto.v
+++ b/tactics/Tauto.v
@@ -3,7 +3,7 @@
Declare ML Module "tauto".
-Grammar tactic simple_tactic: Ast :=
+Grammar tactic simple_tactic: ast :=
tauto [ "Tauto" ] -> [(Tauto)]
| intuition [ "Intuition" ] -> [(Intuition)].