diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-12 14:52:02 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-12 14:52:02 +0000 |
| commit | 44a556b977c782a3a507c4d470fe02afd6c09459 (patch) | |
| tree | 1998c7c3d05ef3042b87feb00ebc8171a5f246e4 /parsing | |
| parent | 296d226de9b058a69ce2f5951468c9ae11965b24 (diff) | |
Ajout 'Print Scopes' et 'Bind Scope with classes'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4378 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -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 0b815a0c6..d32384c86 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) |