diff options
| -rw-r--r-- | parsing/g_basevernac.ml4 | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 0b815a0c61..d32384c860 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -183,6 +183,7 @@ GEXTEND Gram | IDENT "Hint"; qid = global -> PrintHint qid | IDENT "Hint"; "*" -> PrintHintDb | IDENT "HintDb"; s = IDENT -> PrintHintDbName s + | IDENT "Scopes" -> PrintScopes | IDENT "Scope"; s = IDENT -> PrintScope s ] ] ; locatable: @@ -265,6 +266,9 @@ GEXTEND Gram | IDENT "Delimits"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT -> VernacDelimiters (sc,key) + | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; + refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl) + | IDENT "Arguments"; IDENT "Scope"; qid = global; "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl) |