4 files changed, 29 insertions, 18 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 74b275fab..f51cc0869 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -114,27 +114,33 @@ let make_constr_prod_item univ assoc from forpat = function
 let prepare_empty_levels entry (pos,p4assoc,name,reinit) =
   grammar_extend entry pos reinit [(name, p4assoc, [])]
 
-let extend_constr entry (n,assoc,pos,p4assoc,name,reinit) mkact (forpat,pt) =
+let pure_sublevels level symbs =
+  map_succeed (function
+  | Gramext.Snterml (_,n) when Some (int_of_string n) <> level ->
+      int_of_string n
+  | _ ->
+      failwith "") symbs
+
+let extend_constr (entry,level) (n,assoc) mkact forpat pt =
   let univ = get_univ "constr" in
   let pil = List.map (make_constr_prod_item univ assoc n forpat) pt in
   let (symbs,ntl) = List.split pil in
-  let needed_levels = register_empty_levels forpat symbs in
+  let pure_sublevels = pure_sublevels level symbs in
+  let needed_levels = register_empty_levels forpat pure_sublevels in
+  let pos,p4assoc,name,reinit = find_position forpat assoc level in
   List.iter (prepare_empty_levels entry) needed_levels;
   grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact ntl])]
 
 let extend_constr_notation (n,assoc,ntn,rule) =
   (* Add the notation in constr *)
   let mkact loc env = CNotation (loc,ntn,List.map snd env) in
-  let (e,level) = get_constr_entry false (ETConstr (n,())) in
-  let pos,p4assoc,name,reinit = find_position false assoc level in
-  extend_constr e (ETConstr(n,()),assoc,pos,p4assoc,name,reinit)
-    (make_constr_action mkact) (false,rule);
+  let e = get_constr_entry false (ETConstr (n,())) in
+  extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rule;
   (* Add the notation in cases_pattern *)
   let mkact loc env = CPatNotation (loc,ntn,List.map snd env) in
-  let (e,level) = get_constr_entry true (ETConstr (n,())) in
-  let pos,p4assoc,name,reinit = find_position true assoc level in
-  extend_constr e (ETConstr (n,()),assoc,pos,p4assoc,name,reinit)
-    (make_cases_pattern_action mkact) (true,rule)
+  let e = get_constr_entry true (ETConstr (n,())) in
+  extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact)
+    true rule
 
 (**********************************************************************)
 (** Making generic actions in type generic_argument                   *)
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 73db83636..f9c2f90dd 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -628,13 +628,13 @@ let rec list_mem_assoc_triple x = function
   | [] -> false
   | (a,b,c) :: l -> a = x or list_mem_assoc_triple x l
 
-let register_empty_levels forpat symbs =
-  map_succeed (function
-    | Gramext.Snterml (_,n) when
-	let levels = (if forpat then snd else fst) (List.hd !level_stack) in
-	not (list_mem_assoc_triple (int_of_string n) levels) ->
-	find_position_gen forpat true None (Some (int_of_string n))
-    | _ -> failwith "") symbs
+let register_empty_levels forpat levels =
+  map_succeed (fun n ->
+    let levels = (if forpat then snd else fst) (List.hd !level_stack) in
+    if not (list_mem_assoc_triple n levels) then
+      find_position_gen forpat true None (Some n)
+    else
+      failwith "") levels
 
 let find_position forpat assoc level =
   find_position_gen forpat false assoc level
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index aaf4324e2..19b7dd17e 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -229,7 +229,7 @@ val find_position :
 
 val synchronize_level_positions : unit -> unit
 
-val register_empty_levels : bool -> Compat.token Gramext.g_symbol list ->
+val register_empty_levels : bool -> int list ->
     (Gramext.position option * Gramext.g_assoc option *
      string option * Gramext.g_assoc option) list
 
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index facd55099..6dce0401d 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -21,3 +21,8 @@ Definition marker := O.
 Notation "x +1" := (S x) (at level 8, left associativity).
 Reset marker.
 Notation "x +1" := (S x) (at level 8, right associativity).
+
+(* Check that empty levels (here 8 and 2 in pattern) are added in the
+   right order *)
+
+Notation "' 'C_' G ( A )" := (A,G) (at level 8, G at level 2).