From 06b6a53bbc16ac2fd53213d693910c73105564c5 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 3 Nov 2014 19:06:28 +0100
Subject: vernac_classifier: VernacDeclareTacticDefinition does not alter the
 parser

---
 stm/vernac_classifier.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 63b9e2e7f5..53eb1a3f29 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -168,6 +168,7 @@ let rec classify_vernac e =
     | VernacDeclareReduction _
     | VernacDeclareClass _ | VernacDeclareInstances _
     | VernacRegister _
+    | VernacDeclareTacticDefinition _
     | VernacComments _ -> VtSideff [], VtLater
     (* Who knows *)
     | VernacLoad _ -> VtSideff [], VtNow
@@ -181,9 +182,10 @@ let rec classify_vernac e =
         VtSideff [id], if bl = [] then VtLater else VtNow
     (* These commands alter the parser *)
     | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _
-    | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ | VernacSyntaxExtension _ 
+    | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
+    | VernacSyntaxExtension _ 
     | VernacSyntacticDefinition _
-    | VernacDeclareTacticDefinition _ | VernacTacticNotation _
+    | VernacTacticNotation _
     | VernacRequire _ | VernacImport _ | VernacInclude _
     | VernacDeclareMLModule _
     | VernacContext _ (* TASSI: unsure *)
-- 
cgit v1.2.3