From da420fd8315db308a013bb3cca3512fd9c9bf627 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 28 Jan 2019 13:14:44 +0100
Subject: [vernac] Fix classification of `Declare Custom Entry`

It seems that this command should be classified as modifying the parser.
Fixes #9419

Thanks to @gares
---
 stm/vernac_classifier.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 710ddb5571..292e3966a1 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -161,7 +161,6 @@ let classify_vernac e =
     | VernacExistingClass _ | VernacExistingInstance _
     | VernacRegister _
     | VernacNameSectionHypSet _
-    | VernacDeclareCustomEntry _
     | VernacComments _
     | VernacDeclareInstance _ -> VtSideff [], VtLater
     (* Who knows *)
@@ -175,6 +174,7 @@ let classify_vernac e =
     | VernacDeclareModuleType ({v=id},bl,_,_) ->
         VtSideff [id], if bl = [] then VtLater else VtNow
     (* These commands alter the parser *)
+    | VernacDeclareCustomEntry _
     | VernacOpenCloseScope _ | VernacDeclareScope _
     | VernacDelimiters _ | VernacBindScope _
     | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
-- 
cgit v1.2.3