diff options
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 10 | ||||
| -rw-r--r-- | translate/ppvernacnew.ml | 27 |
2 files changed, 21 insertions, 16 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) diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 250e2aa98..384397955 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -546,14 +546,14 @@ let rec pr_vernac = function | Some sc -> str sc in str"Arguments Scope" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" | VernacInfix (local,a,p,s,q,_,ov8,sn) -> (* A Verifier *) - let (a,p,s) = match ov8 with - Some mv8 -> mv8 - | None -> (a,p,s) in + let mv8,s = match ov8 with + | Some (a,p,s) -> + (match p with None -> [] | Some p -> [SetLevel p])@ + (match a with None -> [] | Some a -> [SetAssoc a]),s + | None -> [],s in hov 0 (hov 0 (str"Infix " ++ pr_locality local ++ qs s ++ spc() ++ pr_reference q) ++ - pr_syntax_modifiers - ((match p with None -> [] | Some p -> [SetLevel p])@ - (match a with None -> [] | Some a -> [SetAssoc a])) ++ + pr_syntax_modifiers mv8 ++ (match sn with | None -> mt() | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) @@ -580,7 +580,7 @@ let rec pr_vernac = function let (s,l) = match mv8 with None -> out_some sl | Some ml -> ml in - str"Uninterpreted Notation" ++ spc() ++ pr_locality local ++ qs s ++ + str"Reserved Notation" ++ spc() ++ pr_locality local ++ qs s ++ pr_syntax_modifiers l (* Gallina *) @@ -971,8 +971,8 @@ pr_vbinders bl ++ spc()) hov 1 (str"Implicit Arguments" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep int l ++ str"]") | VernacReserve (idl,c) -> - hov 1 (str"Implicit Variable" ++ - str (if List.length idl > 1 then "s " else " ") ++ str "Type " ++ + hov 1 (str"Implicit Type" ++ + str (if List.length idl > 1 then "s " else " ") ++ prlist_with_sep spc pr_id idl ++ str " :" ++ spc () ++ pr_type c) | VernacSetOpacity (fl,l) -> hov 1 ((if fl then str"Opaque" else str"Transparent") ++ @@ -982,16 +982,21 @@ pr_vbinders bl ++ spc()) str"Set Implicit Arguments" ++ (if !Options.translate_strict_impargs then - sep_end () ++ fnl () ++ str"Unset Strict Implicits" + sep_end () ++ fnl () ++ str"Unset Strict Implicit" else mt ()) | VernacUnsetOption (Goptions.SecondaryTable ("Implicit","Arguments")) | VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"),BoolValue false) -> (if !Options.translate_strict_impargs then - str"Set Strict Implicits" ++ sep_end () ++ fnl () + str"Set Strict Implicit" ++ sep_end () ++ fnl () else mt ()) ++ str"Unset Implicit Arguments" + | VernacSetOption (Goptions.SecondaryTable (a,"Implicits"),BoolValue true) -> + str("Set "^a^" Implicit") + | VernacUnsetOption (Goptions.SecondaryTable (a,"Implicits")) -> + str("Unset "^a^" Implicit") + | VernacUnsetOption na -> hov 1 (str"Unset" ++ spc() ++ pr_printoption na None) | VernacSetOption (na,v) -> hov 2 (str"Set" ++ spc() ++ pr_set_option na v) |