diff options
Diffstat (limited to 'stm')
| -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 794fabc910..e810e59072 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -178,7 +178,7 @@ let rec classify_vernac e = VtSideff [id], if bl = [] then VtLater else VtNow (* These commands alter the parser *) | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _ - | VernacInfix _ | VernacNotation _ | VernacSyntaxExtension _ + | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ | VernacSyntaxExtension _ | VernacSyntacticDefinition _ | VernacDeclareTacticDefinition _ | VernacTacticNotation _ | VernacRequire _ | VernacImport _ | VernacInclude _ |