diff options
| author | Emilio Jesus Gallego Arias | 2019-01-28 13:14:44 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-01-28 15:28:33 +0100 |
| commit | da420fd8315db308a013bb3cca3512fd9c9bf627 (patch) | |
| tree | bbc478d4c84bbcc6010f6f33570f2b6bf99df63a | |
| parent | 9d9bc6fa0eb3d83218f7ed025cacab4875e555ea (diff) | |
[vernac] Fix classification of `Declare Custom Entry`
It seems that this command should be classified as modifying the parser.
Fixes #9419
Thanks to @gares
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 _ |