diff options
| author | herbelin | 2003-09-12 14:40:44 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-12 14:40:44 +0000 |
| commit | d78ac151793dc8df15e7e687e5e20d5f48cd53d1 (patch) | |
| tree | 475f16a3b81d23698709c08eac45380a5302a198 | |
| parent | 2a07006989dbd0d2ccbae49f3e59d7cd5720d92d (diff) | |
Ajout 'Print Scopes' et 'Bind Scope with classes'; 'Delimits' -> 'Delimit'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4358 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 1522d6fa6a..fddda8b687 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -434,7 +434,7 @@ GEXTEND Gram VernacDeclareImplicits (qid,pos) | IDENT "Implicit"; ["Variable"; "Type" | IDENT "Variables"; "Type"]; - idl = LIST1 ident; ":"; c = constr -> VernacReserve (idl,c) + idl = LIST1 ident; ":"; c = lconstr -> VernacReserve (idl,c) (* For compatibility *) | IDENT "Implicit"; IDENT "Arguments"; IDENT "On" -> @@ -593,6 +593,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 ] ] ; class_rawexpr: @@ -661,9 +662,12 @@ GEXTEND Gram [ [ IDENT "Open"; local = locality; IDENT "Scope"; sc = IDENT -> VernacOpenScope (local,sc) - | IDENT "Delimits"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT -> + | IDENT "Delimit"; 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) |