diff options
Diffstat (limited to 'parsing/g_vernacnew.ml4')
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 12e95d235a..0ad8caaaa0 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -648,7 +648,8 @@ GEXTEND Gram GLOBAL: syntax; syntax: - [ [ IDENT "Open"; IDENT "Scope"; sc = IDENT -> VernacOpenScope sc + [ [ IDENT "Open"; exp = [IDENT "Local" -> false | -> true]; IDENT "Scope"; + sc = IDENT -> VernacOpenScope (exp,sc) | IDENT "Delimits"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT -> VernacDelimiters (sc,key) |