diff options
| author | Hugo Herbelin | 2018-06-28 19:29:06 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-07-29 02:40:22 +0200 |
| commit | 8da77fc099183c5c79fdb433b3555a63adba820d (patch) | |
| tree | 17a1a8afaf6145a9f74ccf34ab74cd0dd95aefc6 | |
| parent | 90a1d7202182205b3a66b4e8edf751e82b117551 (diff) | |
Classify "Declare Custom" as VtNow for the stm.
When parsing of a document shall be possible independently of
interpretation, this shall however be indicated as shall be
interpreted now so that the notation commands coming next work.
| -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 _ |