Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace par un niveau ajoute dynamiquement

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

2 files changed, 11 insertions, 21 deletions

diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index bd8ca6aadb..eaaa0c5b2c 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -171,8 +171,7 @@ GEXTEND Gram
     [ [ c = operconstr LEVEL "9" -> c ] ]
   ;
   operconstr:
-    [ "250" LEFTA [ ]
-    | "200" RIGHTA
+    [ "200" RIGHTA
       [ c = binder_constr -> c ]
     | "100" RIGHTA
       [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1,c2)
@@ -195,7 +194,7 @@ GEXTEND Gram
     | "0"
       [ c=atomic_constr -> c
       | c=match_constr -> c
-      | "("; c = operconstr LEVEL "250"; ")" ->
+      | "("; c = operconstr; ")" ->
           CNotation(loc,"( _ )",[c]) ] ]
   ;
   binder_constr:
@@ -288,8 +287,7 @@ GEXTEND Gram
     [ [ pl = LIST1 pattern LEVEL "200" SEP ","; "=>"; rhs = lconstr -> (loc,pl,rhs) ] ]
   ;
   pattern:
-    [ "250" LEFTA [ ]
-    | "10" LEFTA
+    [ "10" LEFTA
       [ p = pattern ; lp = LIST1 (pattern LEVEL "0") ->
         (match p with
           | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp)
@@ -303,16 +301,10 @@ GEXTEND Gram
     | "0"
       [ r = Prim.reference -> CPatAtom (loc,Some r)
       | "_" -> CPatAtom (loc,None)
-      | "("; p = pattern LEVEL "250"; ")" ->
+      | "("; p = pattern; ")" ->
           CPatNotation(loc,"( _ )",[p])
       | n = INT -> CPatNumeral (loc,Bignat.POS(Bignat.of_string n)) ] ]
   ;
-(*
-  lpattern:
-    [ [ c = pattern -> c
-      | p1=pattern; ","; p2=lpattern ->  CPatCstr (loc, pair loc, [p1;p2]) ] ]
-  ;
-*)
   binder_list:
     [ [ idl=LIST1 name; bl=LIST0 binder_let -> 
           LocalRawAssum (idl,CHole loc)::bl
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 7cbda15980..e0b60e6243 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -545,8 +545,7 @@ let default_levels_v7 =
    0,Gramext.RightA]
 
 let default_levels_v8 =
-  [250,Gramext.LeftA;
-   200,Gramext.RightA;
+  [200,Gramext.RightA;
    100,Gramext.RightA;
    99,Gramext.RightA;
    90,Gramext.RightA;
@@ -556,8 +555,7 @@ let default_levels_v8 =
    0,Gramext.RightA]
 
 let default_pattern_levels_v8 =
-  [250,Gramext.LeftA;
-   10,Gramext.LeftA;
+  [10,Gramext.LeftA;
    0,Gramext.RightA]
 
 let level_stack = 
@@ -592,8 +590,7 @@ let error_level_assoc p current expected =
      pr_assoc expected ++ str " associative")
 
 let find_position forpat other assoc lev =
-  let default =
-    if !Options.v7 then (10,Gramext.RightA) else (200,Gramext.RightA) in
+  let default = if !Options.v7 then Some (10,Gramext.RightA) else None in
   let ccurrent,pcurrent as current = List.hd !level_stack in 
   match lev with
   | None ->
@@ -604,7 +601,7 @@ let find_position forpat other assoc lev =
 	error "Left associativity not allowed at level 8";
       let after = ref default in
       let rec add_level q = function
-        | (p,_ as pa)::l when p > n -> pa :: add_level pa l
+        | (p,_ as pa)::l when p > n -> pa :: add_level (Some pa) l
         | (p,a as pa)::l as l' when p = n ->
 	    if admissible_assoc (a,assoc) then raise (Found a);
 	    (* No duplication of levels in v8 *)
@@ -613,7 +610,7 @@ let find_position forpat other assoc lev =
 	    if a = Gramext.LeftA then
 	      match l with
 		| (p,a)::_ as l' when p = n -> raise (Found a)
-		| _ -> after := pa; pa::(n,create_assoc assoc)::l
+		| _ -> after := Some pa; pa::(n,create_assoc assoc)::l
 	    else
 	      (* This was not (p,LeftA) hence assoc is RightA *)
 	      (after := q; (n,create_assoc assoc)::l')
@@ -627,7 +624,8 @@ let find_position forpat other assoc lev =
 	  else (add_level default ccurrent, pcurrent) in
         level_stack := updated:: !level_stack;
 	let assoc = create_assoc assoc in
-        Some (Gramext.After (constr_level2 !after)),
+	(if !after = None then Some Gramext.First
+	else Some (Gramext.After (constr_level2 (out_some !after)))),
 	Some assoc, Some (constr_level2 (n,assoc))
       with
           Found a ->