diff options
| -rw-r--r-- | parsing/g_constrnew.ml4 | 11 | ||||
| -rw-r--r-- | parsing/g_tacticnew.ml4 | 27 | ||||
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 6 |
3 files changed, 23 insertions, 21 deletions
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4 index ba8be907c..ffc7d403c 100644 --- a/parsing/g_constrnew.ml4 +++ b/parsing/g_constrnew.ml4 @@ -153,7 +153,7 @@ GEXTEND Gram | "("; c=operconstr; ")" -> c ] ] ; binder_constr: - [ [ "!"; bl = LIST1 binder; "."; c = operconstr LEVEL "200" -> + [ [ "!"; bl = binder_list; "."; c = operconstr LEVEL "200" -> CProdN(loc,bl,c) | "fun"; bl = LIST1 binder; ty = type_cstr; "=>"; c = operconstr LEVEL "200" -> @@ -244,11 +244,14 @@ GEXTEND Gram [ [ c = pattern -> c | p1=pattern; ","; p2=lpattern -> CPatCstr (loc, pair loc, [p1;p2]) ] ] ; + binder_list: + [ [ idl=LIST1 name; bl=LIST0 binder -> (idl,CHole loc)::bl + | "("; idl=LIST1 name; ":"; c=lconstr; ")"; bl=LIST0 binder ->(idl,c)::bl + | idl=LIST1 name; ":"; c=constr -> [(idl,c)] ] ] + ; binder: [ [ id=name -> ([id],CHole loc) - | "("; id=name; ")" -> ([id],CHole loc) - | "("; id=name; ":"; c=lconstr; ")" -> ([id],c) - | id=name; ":"; c=constr -> ([id],c) ] ] (* tolerance *) + | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,c) ] ] ; type_cstr: [ [ c=OPT [":"; c=lconstr -> c] -> (loc,c) ] ] diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index 725a3432f..f5a0f851e 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -22,11 +22,15 @@ let _ = List.iter (fun s -> Lexer.add_token("",s)) tactic_kw (* Hack to parse "with n := c ..." as a binder without conflicts with the *) (* admissible notation "with c1 c2..." *) -let test_coloneq2 = - Gram.Entry.of_parser "test_int_coloneq" +let test_lparcoloneq2 = + Gram.Entry.of_parser "test_lparcoloneq2" (fun strm -> - match Stream.npeek 2 strm with - | [_; ("", ":=")] -> () + match Stream.npeek 1 strm with + | [("", "(")] -> + begin match Stream.npeek 3 strm with + | [_; _; ("", ":=")] -> () + | _ -> raise Stream.Failure + end | _ -> raise Stream.Failure) (* open grammar entries, possibly in quotified form *) @@ -168,19 +172,12 @@ GEXTEND Gram ] ] ; simple_binding: - [ [ id = base_ident; ":="; c = constr -> (loc, NamedHyp id, c) - | n = natural; ":="; c = constr -> (loc, AnonHyp n, c) ] ] + [ [ "("; id = base_ident; ":="; c = lconstr; ")" -> (loc, NamedHyp id, c) + | "("; n = natural; ":="; c = lconstr; ")" -> (loc, AnonHyp n, c) ] ] ; binding_list: - [ [ test_coloneq2; n = natural; ":="; c = constr; - bl = LIST0 simple_binding -> - ExplicitBindings ((join_to_constr loc c,AnonHyp n, c) :: bl) - | test_coloneq2; id = base_ident; ":="; c2 = constr; - bl = LIST0 simple_binding -> - ExplicitBindings - ((join_to_constr loc c2,NamedHyp id, c2) :: bl) - | c1 = constr; bl = LIST0 constr -> - ImplicitBindings (c1 :: bl) ] ] + [ [ test_lparcoloneq2; bl = LIST1 simple_binding -> ExplicitBindings bl + | bl = LIST1 constr -> ImplicitBindings bl ] ] ; constr_with_bindings: [ [ c = constr; l = with_binding_list -> (c, l) ] ] diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 4a6d3ca69..19a03a22e 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -670,8 +670,10 @@ GEXTEND Gram sc = OPT [ ":"; sc = IDENT -> sc ] -> let (a,n,b) = Metasyntax.interp_infix_modifiers a n modl in VernacInfix (local,a,n,op,p,b,None,sc) - | IDENT "Notation"; local = locality; s = IDENT; ":="; c = constr -> - VernacNotation (local,"'"^s^"'",c,[],None,None) + | IDENT "Notation"; local = locality; s = IDENT; ":="; c = constr; + l = [ "("; IDENT "only"; IDENT "parsing"; ")" -> [SetOnlyParsing] + | -> [] ] -> + VernacNotation (local,"'"^s^"'",c,l,None,None) | IDENT "Notation"; local = locality; s = STRING; ":="; c = constr; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> |