diff options
| author | Enrico Tassi | 2019-01-29 11:23:44 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-01-29 11:23:44 +0100 |
| commit | a9b141469fe3036355be95d8cf5f0bf5c240fe37 (patch) | |
| tree | 1ced7154c46778ec3135bc024e6a640ae205ca6e | |
| parent | 1f3536e89b7235aaa0007e8ab7298040407df8ba (diff) | |
| parent | da420fd8315db308a013bb3cca3512fd9c9bf627 (diff) | |
Merge PR #9421: [vernac] Fix classification of `Declare Custom Entry`
Reviewed-by: 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 _ |