diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-21 22:51:40 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-21 22:51:40 +0000 |
| commit | 3be30b13b1fb0bba12411e9fefb7b53f0d8fa9e5 (patch) | |
| tree | 8f4d77ae174bd06c44c22dbfb39127af5e9237ad /parsing | |
| parent | 8ed294710b082e8331efe0a592de0afabb701bfd (diff) | |
Renommages divers.
Changement de la politique de V8only: V8only tout seul signifie
'seulement interprétation' en V8; héritage des paramêtres de V7
seulement si pas V8only; sinon, il faut tout expliciter (pas
d'héritage partiel)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4434 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 86658e2bb..4c096964d 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -439,7 +439,7 @@ GEXTEND Gram pos = OPT [ "["; l = LIST0 natural; "]" -> l ] -> VernacDeclareImplicits (qid,pos) - | IDENT "Implicit"; ["Variable"; "Type" | IDENT "Variables"; "Type"]; + | IDENT "Implicit"; ["Type" | "Types"]; idl = LIST1 ident; ":"; c = lconstr -> VernacReserve (idl,c) (* For compatibility *) @@ -685,15 +685,15 @@ GEXTEND Gram modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> let (a,n,b) = Metasyntax.interp_infix_modifiers None None modl in - VernacInfix (local,a,n,op,p,b,None,sc) + VernacInfix (local,a,n,op,p,b,Some(a,n,op),sc) | IDENT "Notation"; local = locality; s = IDENT; ":="; c = constr; l = [ "("; IDENT "only"; IDENT "parsing"; ")" -> [SetOnlyParsing] | -> [] ] -> - VernacNotation (local,c,Some("'"^s^"'",l),None,None) + VernacNotation (local,c,Some("'"^s^"'",l),Some("'"^s^"'",l),None) | IDENT "Notation"; local = locality; s = STRING; ":="; c = constr; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> - VernacNotation (local,c,Some(s,modl),None,sc) + VernacNotation (local,c,Some(s,modl),Some(s,modl),sc) | IDENT "Tactic"; IDENT "Notation"; s = STRING; pil = LIST0 production_item; ":="; t = Tactic.tactic -> @@ -719,7 +719,7 @@ GEXTEND Gram VernacSyntax (u,el) *) - | IDENT "Uninterpreted"; IDENT "Notation"; local = locality; s = STRING; + | IDENT "Reserved"; IDENT "Notation"; local = locality; s = STRING; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] -> VernacSyntaxExtension (local,Some(s,l),None) |