From 3b7a6761f5c9bf5026c4517e8032aa4384185528 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 29 Mar 2018 20:07:34 +0200
Subject: Adding a command "Declare Scope" and deprecating scope implicit
 declaration.

---
 stm/vernac_classifier.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 2170477938..85babd922b 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -168,7 +168,8 @@ let classify_vernac e =
     | VernacDeclareModuleType ({v=id},bl,_,_) ->
         VtSideff [id], if bl = [] then VtLater else VtNow
     (* These commands alter the parser *)
-    | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _
+    | VernacOpenCloseScope _ | VernacDeclareScope _
+    | VernacDelimiters _ | VernacBindScope _
     | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
     | VernacSyntaxExtension _
     | VernacSyntacticDefinition _
-- 
cgit v1.2.3