diff options
| -rw-r--r-- | stm/vernac_classifier.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index a9a27e8100..2170477938 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -155,6 +155,7 @@ let classify_vernac e = | VernacDeclareClass _ | VernacDeclareInstances _ | VernacRegister _ | VernacNameSectionHypSet _ + | VernacDeclareCustomEntry _ | VernacComments _ -> VtSideff [], VtLater (* Who knows *) | VernacLoad _ -> VtSideff [], VtNow @@ -169,7 +170,7 @@ let classify_vernac e = (* These commands alter the parser *) | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _ | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ - | VernacSyntaxExtension _ | VernacDeclareCustomEntry _ + | VernacSyntaxExtension _ | VernacSyntacticDefinition _ | VernacRequire _ | VernacImport _ | VernacInclude _ | VernacDeclareMLModule _ |