diff options
| author | Hugo Herbelin | 2018-03-29 20:07:34 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-10 13:07:29 +0200 |
| commit | 3b7a6761f5c9bf5026c4517e8032aa4384185528 (patch) | |
| tree | 0ecb7cdd4d12eceea257cd625d4e2421e3d39dbe /stm | |
| parent | 69fb545f0fad2b356f5be1ce3e1a24b5afe26ce2 (diff) | |
Adding a command "Declare Scope" and deprecating scope implicit declaration.
Diffstat (limited to 'stm')
| -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 2170477938..85babd922b 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -168,7 +168,8 @@ let classify_vernac e = | VernacDeclareModuleType ({v=id},bl,_,_) -> VtSideff [id], if bl = [] then VtLater else VtNow (* These commands alter the parser *) - | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _ + | VernacOpenCloseScope _ | VernacDeclareScope _ + | VernacDelimiters _ | VernacBindScope _ | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ | VernacSyntaxExtension _ | VernacSyntacticDefinition _ |