Factorisation des produits de même type; parenthèses autour des x:=c et n:=c dans les 'with bindings'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3974 85f007b7-540e-0410-9357-904b9bb8a0f7

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 ] ->