Fusion de tuple_constr/tuple_pattern dans operconstr/pattern

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

4 files changed, 13 insertions, 29 deletions

diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index f94a405b9..eaf039b9d 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -121,8 +121,7 @@ let lpar_id_coloneq =
 if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr sort global
-  constr_pattern lconstr_pattern Constr.ident binder binder_let pattern
-  tuple_constr tuple_pattern;
+  constr_pattern lconstr_pattern Constr.ident binder binder_let pattern;
   Constr.ident:
     [ [ id = Prim.ident -> id
 
@@ -158,19 +157,17 @@ GEXTEND Gram
   constr:
     [ [ c = operconstr LEVEL "9" -> c ] ]
   ;
-  tuple_constr:
-    [ [ c = operconstr -> c ] ]
-  ;
   operconstr:
-    [ "200" RIGHTA
+    [ "250" LEFTA [ ]
+    | "200" RIGHTA
       [ c = binder_constr -> c ]
     | "100" RIGHTA
       [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1,c2)
-      | c1 = operconstr; ":"; c2 = operconstr    -> CCast(loc,c1,c2) ]
+      | c1 = operconstr; ":"; c2 = operconstr LEVEL "200" -> CCast(loc,c1,c2) ]
     | "99" RIGHTA [ ]
     | "90" RIGHTA
       [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2)
-      | c1 = operconstr; "->"; c2 = operconstr    -> CArrow(loc,c1,c2) ]
+      | c1 = operconstr; "->"; c2 = operconstr LEVEL"200" -> CArrow(loc,c1,c2)]
     | "10"
       [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args)
       | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args)
@@ -186,7 +183,7 @@ GEXTEND Gram
     | "0"
       [ c=atomic_constr -> c
       | c=match_constr -> c
-      | "("; c=tuple_constr; ")" -> c ] ]
+      | "("; c = operconstr LEVEL "250"; ")" -> c ] ]
   ;
   binder_constr:
     [ [ "forall"; bl = binder_list; ","; c = operconstr LEVEL "200" ->
@@ -211,7 +208,7 @@ GEXTEND Gram
 	  ":="; c1 = operconstr LEVEL "200"; "in";
           c2 = operconstr LEVEL "200" ->
           CLetTuple (loc,List.map snd lb,po,c1,c2)
-      | "if"; c=operconstr; po = return_type;
+      | "if"; c=operconstr LEVEL "200"; po = return_type;
 	"then"; b1=operconstr LEVEL "200";
         "else"; b2=operconstr LEVEL "200" ->
           CIf (loc, c, po, b1, b2)
@@ -279,13 +276,11 @@ GEXTEND Gram
     [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ]
   ;
   eqn:
-    [ [ pl = LIST1 pattern SEP ","; "=>"; rhs = lconstr -> (loc,pl,rhs) ] ]
-  ;
-  tuple_pattern:
-    [ [ c = pattern -> c ] ]
+    [ [ pl = LIST1 pattern LEVEL "200" SEP ","; "=>"; rhs = lconstr -> (loc,pl,rhs) ] ]
   ;
   pattern:
-    [ "200" RIGHTA [ ]
+    [ "250" LEFTA [ ]
+    | "200" RIGHTA [ ]
     | "99" RIGHTA [ ]
     | "90" RIGHTA [ ]
     | "10" LEFTA
@@ -304,7 +299,7 @@ GEXTEND Gram
     | "0"
       [ r = Prim.reference -> CPatAtom (loc,Some r)
       | "_" -> CPatAtom (loc,None)
-      | "("; p = tuple_pattern; ")" -> p
+      | "("; p = pattern LEVEL "250"; ")" -> p
       | n = bigint -> CPatNumeral (loc,n) ] ]
   ;
 (*
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index dc63db097..759030fbe 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -350,8 +350,6 @@ module Constr =
     let lconstr_pattern = gec_constr "lconstr_pattern"
     let binder = Gram.Entry.create "constr:binder"
     let binder_let = Gram.Entry.create "constr:binder_let"
-    let tuple_constr = gec_constr "tuple_constr"
-    let tuple_pattern = Gram.Entry.create "tuple_pattern"
   end
 
 module Module =
@@ -544,7 +542,8 @@ let default_levels_v7 =
    0,Gramext.RightA]
 
 let default_levels_v8 =
-  [200,Gramext.RightA;
+  [250,Gramext.LeftA;
+   200,Gramext.RightA;
    100,Gramext.RightA;
    99,Gramext.RightA;
    90,Gramext.RightA;
@@ -721,12 +720,6 @@ let get_constr_entry forpat en =
 	snd (get_entry (get_univ "constr") "binder_constr"),
         None,
         false
-    | ETConstr(250,()) when not !Options.v7 ->
-        (if forpat then weaken_entry Constr.tuple_pattern
-	else weaken_entry Constr.tuple_constr),
-(*        snd (get_entry (get_univ "constr") "tuple_constr"),*)
-        None,
-        false
     | _ -> compute_entry true (fun (n,()) -> Some n) forpat en
 
 (* This computes the name to give to a production knowing the name and
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 1767f2fcd..a91a3592d 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -141,8 +141,6 @@ module Constr :
     val lconstr_pattern : constr_expr Gram.Entry.e
     val binder : (name located list * constr_expr) Gram.Entry.e
     val binder_let : local_binder Gram.Entry.e
-    val tuple_constr : constr_expr Gram.Entry.e
-    val tuple_pattern : cases_pattern_expr Gram.Entry.e
   end
 
 module Module : 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 2ccdfdc40..cdb9574e6 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -213,9 +213,7 @@ let print_grammar univ entry =
     let te = 
       match entry with
 	| "constr" | "operconstr" -> weaken_entry Pcoq.Constr.operconstr
-	| "tuple_constr" -> weaken_entry Pcoq.Constr.tuple_constr
 	| "pattern" -> weaken_entry Pcoq.Constr.pattern
-	| "tuple_pattern" -> weaken_entry Pcoq.Constr.tuple_pattern
 	| "tactic" -> weaken_entry Pcoq.Tactic.simple_tactic
 	| _ -> error "Unknown or unprintable grammar entry" in
     Gram.Entry.print te