Mise en place de motifs récursifs dans Notation; quelques simplifications au passage

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

16 files changed, 369 insertions, 86 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 46f8ff5b24..ddd9ef0447 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -634,7 +634,16 @@ let traverse_binder subst id (ids,tmpsc,scopes as env) =
   let id = try coerce_to_id (fst (List.assoc id subst)) with Not_found -> id in
   id,(Idset.add id ids,tmpsc,scopes)
 
-let rec subst_rawconstr loc interp subst (ids,_,scopes as env) = function
+let decode_constrlist_value = function
+  | CAppExpl (_,_,l) -> l
+  | _ -> anomaly "Ill-formed list argument of notation"
+
+let rec subst_iterator y t = function
+  | RVar (_,id) as x -> if id = y then t else x
+  | x -> map_rawconstr (subst_iterator y t) x
+
+let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as env) =
+  function
   | AVar id ->
       begin
 	(* subst remembers the delimiters stack in the interpretation *)
@@ -646,9 +655,25 @@ let rec subst_rawconstr loc interp subst (ids,_,scopes as env) = function
 	  (* Happens for local notation joint with inductive/fixpoint defs *)
 	  RVar (loc,id)
       end
+  | AList (x,y,iter,terminator) ->
+      (try 
+        (* All elements of the list are in scopes (scopt,subscopes) *)
+	let (a,(scopt,subscopes)) = List.assoc x subst in
+        let termin = 
+          subst_aconstr_in_rawconstr loc interp subst (ids,None,scopes) 
+            terminator in
+        let l = decode_constrlist_value a in
+	List.fold_right (fun a t -> 
+          subst_iterator y t
+            (subst_aconstr_in_rawconstr loc interp 
+              ((x,(a,(scopt,subscopes)))::subst)
+              (ids,None,scopes) iter))
+            l termin
+      with Not_found -> 
+          anomaly "Inconsistent substitution of recursive notation")
   | t ->
       rawconstr_of_aconstr_with_binders loc (traverse_binder subst)
-      (subst_rawconstr loc interp subst) (ids,None,scopes) t
+      (subst_aconstr_in_rawconstr loc interp subst) (ids,None,scopes) t
 
 let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args =
   let ntn,args = contract_notation ntn args in
@@ -656,7 +681,7 @@ let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args =
   let ((ids,c),df) = Symbols.interp_notation loc ntn scopes in
   if !dump then dump_notation_location (ntn_loc loc args ntn) ntn df;
   let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
-  subst_rawconstr loc intern subst env c
+  subst_aconstr_in_rawconstr loc intern subst env c
 
 let set_type_scope (ids,tmp_scope,scopes) =
   (ids,Some Symbols.type_scope,scopes)
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 713306690b..bbaf399b09 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -51,7 +51,8 @@ let ppcmd_of_cut = function
   | PpTbrk(n1,n2) -> tbrk(n1,n2)
 
 type unparsing = 
-  | UnpMetaVar of tolerability
+  | UnpMetaVar of int * parenRelation
+  | UnpListMetaVar of int * parenRelation * unparsing list
   | UnpTerminal of string
   | UnpBox of ppbox * unparsing list
   | UnpCut of ppcut
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index 4d83eda3d2..0664d10f36 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -41,7 +41,8 @@ val ppcmd_of_box : ppbox -> std_ppcmds -> std_ppcmds
 val ppcmd_of_cut : ppcut -> std_ppcmds
 
 type unparsing = 
-  | UnpMetaVar of tolerability
+  | UnpMetaVar of int * parenRelation
+  | UnpListMetaVar of int * parenRelation * unparsing list
   | UnpTerminal of string
   | UnpBox of ppbox * unparsing list
   | UnpCut of ppcut
diff --git a/interp/symbols.ml b/interp/symbols.ml
index 89a65a6590..eb2e60d0d6 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -175,6 +175,7 @@ let cases_pattern_key = function
 
 let aconstr_key = function
   | AApp (ARef ref,args) -> RefKey ref, Some (List.length args)
+  | AList (_,_,AApp (ARef ref,args),_) -> RefKey ref, Some (List.length args)
   | ARef ref -> RefKey ref, Some 0
   | _ -> Oth, None
 
@@ -430,11 +431,14 @@ let declare_ref_arguments_scope ref =
 type symbol =
   | Terminal of string
   | NonTerminal of identifier
+  | SProdList of identifier * symbol list
   | Break of int
 
-let string_of_symbol = function
+let rec string_of_symbol = function
   | NonTerminal _ -> ["_"]
   | Terminal s -> [s]
+  | SProdList (_,l) -> 
+     let l = List.flatten (List.map string_of_symbol l) in "_"::l@".."::l@["_"]
   | Break _ -> []
 
 let make_notation_key symbols =
diff --git a/interp/symbols.mli b/interp/symbols.mli
index 4932b90d5f..1add7570e4 100644
--- a/interp/symbols.mli
+++ b/interp/symbols.mli
@@ -133,6 +133,7 @@ val declare_ref_arguments_scope : global_reference -> unit
 type symbol =
   | Terminal of string
   | NonTerminal of identifier
+  | SProdList of identifier * symbol list
   | Break of int
 
 val make_notation_key : symbol list -> notation
@@ -155,4 +156,3 @@ val find_notation_printing_rule : notation -> unparsing_rule
 
 (**********************************************************************)
 (* Rem: printing rules for numerals are trivial *)
-
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 1fe8edaca3..832a6ab68e 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -21,11 +21,16 @@ open Term
 (**********************************************************************)
 (* This is the subtype of rawconstr allowed in syntactic extensions *)
 
+(* For AList: first constr is iterator, second is terminator;
+   first id is place of n-th argument in iterator and snd id is recursive
+   place in iterator *)
+
 type aconstr =
   (* Part common to rawconstr and cases_pattern *)
   | ARef of global_reference
   | AVar of identifier
   | AApp of aconstr * aconstr list
+  | AList of identifier * identifier * aconstr * aconstr
   (* Part only in rawconstr *)
   | ALambda of name * aconstr * aconstr
   | AProd of name * aconstr * aconstr
@@ -48,6 +53,7 @@ let name_app f e = function
 let rawconstr_of_aconstr_with_binders loc g f e = function
   | AVar id -> RVar (loc,id)
   | AApp (a,args) -> RApp (loc,f e a, List.map (f e) args)
+  | AList _ -> anomaly "Recursive patterns of notations are not supported while translating to rawconstr"
   | ALambda (na,ty,c) ->
       let na,e = name_app g e na in RLambda (loc,na,f e ty,f e c)
   | AProd (na,ty,c) ->
@@ -104,6 +110,11 @@ let rec subst_aconstr subst raw =
 	if r' == r && rl' == rl then raw else
 	  AApp(r',rl')
 
+  | AList (id1,id2,r1,r2) -> 
+      let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  AList (id1,id2,r1',r2')
+
   | ALambda (n,r1,r2) -> 
       let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
 	if r1' == r1 && r2' == r2 then raw else
@@ -182,13 +193,55 @@ let add_name r = function
   | Anonymous -> ()
   | Name id -> r := id :: !r
 
-let aconstr_of_rawconstr vars a =
+let ldots_var = id_of_string ".."
+
+let has_ldots =
+  List.exists
+    (function RApp (_,RVar(_,v),_) when v = ldots_var -> true | _ -> false)
+
+let compare_rawconstr f t1 t2 = match t1,t2 with
+  | RRef (_,r1), RRef (_,r2) -> r1 = r2
+  | RVar (_,v1), RVar (_,v2) -> v1 = v2
+  | RApp (_,f1,l1), RApp (_,f2,l2) -> f f1 f2 & List.for_all2 f l1 l2
+  | RLambda (_,na1,ty1,c1), RLambda (_,na2,ty2,c2) when na1 = na2 ->
+      f ty1 ty2 & f c1 c2
+  | RProd (_,na1,ty1,c1), RProd (_,na2,ty2,c2) when na1 = na2 ->
+      f ty1 ty2 & f c1 c2
+  | RHole _, RHole _ -> true
+  | RSort (_,s1), RSort (_,s2) -> s1 = s2
+  | (RLetIn _ | RCases _ | ROrderedCase _ | RRec _ | RDynamic _
+    | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_
+  | _,(RLetIn _ | RCases _ | ROrderedCase _ | RRec _ | RDynamic _
+      | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _)
+      -> error "Unsupported construction in recursive notations"
+  | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ | RHole _ | RSort _), _
+      -> false
+
+let rec eq_rawconstr t1 t2 = compare_rawconstr eq_rawconstr t1 t2
+
+let discriminate_patterns nl l1 l2 =
+  let diff = ref None in
+  let rec aux n c1 c2 = match c1,c2 with
+  | RVar (_,v1), RVar (_,v2) when v1<>v2 ->
+      if !diff = None then (diff := Some (v1,v2,(n<nl)); true)
+      else 
+        !diff = Some (v1,v2,(n<nl)) or !diff = Some (v2,v1,(n>=nl))
+        or (error
+          "Both ends of the recursive pattern differ in more than one place")
+  | _ -> compare_rawconstr (aux (n+1)) c1 c2 in
+  let l = list_map2_i aux 0 l1 l2 in
+  if not (List.for_all ((=) true) l) then
+    error "Both ends of the recursive pattern differ";
+  !diff
+
+let aconstr_and_vars_of_rawconstr a =
   let found = ref [] in
   let bound_binders = ref [] in
   let rec aux = function
   | RVar (_,id) -> 
       if not (List.mem id !bound_binders) then found := id::!found;
       AVar id
+  | RApp (_,f,args) when has_ldots args -> make_aconstr_list f args 
   | RApp (_,g,args) -> AApp (aux g, List.map aux args)
   | RLambda (_,na,ty,c) -> add_name bound_binders na; ALambda (na,aux ty,aux c)
   | RProd (_,na,ty,c) -> add_name bound_binders na; AProd (na,aux ty,aux c)
@@ -219,14 +272,56 @@ let aconstr_of_rawconstr vars a =
   | RDynamic _ | RRec _ | REvar _ ->
       error "Fixpoints, cofixpoints, existential variables and pattern-matching  not \
 allowed in abbreviatable expressions"
+
+  (* Recognizing recursive notations *)
+  and terminator_of_pat f1 ll1 lr1 = function
+  | RApp (loc,f2,l2) ->
+      if not (eq_rawconstr f1 f2) then error
+	"Cannot recognize the same head to both ends of the recursive pattern";
+      let nl = List.length ll1 in
+      let nr = List.length lr1 in
+      if List.length l2 <> nl + nr + 1 then
+	error "Both ends of the recursive pattern have different lengths";
+      let ll2,l2' = list_chop nl l2 in
+      let t = List.hd l2' and lr2 = List.tl l2' in
+      let discr = discriminate_patterns nl (ll1@lr1) (ll2@lr2) in
+      let x,y,order = match discr with Some z -> z | None -> 
+	error "Both ends of the recursive pattern are the same" in
+      List.iter (fun id ->
+        if List.mem id !bound_binders or List.mem id !found 
+        then error "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part";
+        found := id::!found) [x;y];
+      let iter =
+        if order then RApp (loc,f1,ll1@RVar (loc,ldots_var)::lr1)
+        else RApp (loc,f2,ll2@RVar (loc,ldots_var)::lr2) in
+      (if order then x else y), ldots_var, aux iter, aux t
+  | _ -> error "One end of the recursive pattern is not an application"
+    
+  and make_aconstr_list f args =
+    let rec find_patterns acc = function
+      | RApp(_,RVar (_,a),[c]) :: l when a = ldots_var ->
+          (* We've found the recursive part *)
+	  let x,y,iter,terminator = terminator_of_pat f (List.rev acc) l c in
+	  AList (x,y,iter,terminator)
+      | a::l -> find_patterns (a::acc) l
+      | [] -> error "Ill-formed recursive notation"
+    in find_patterns [] args
+
   in
-  let a = aux a in
+  let t = aux a in
+  (* Side effect *)
+  t, !found, !bound_binders
+
+let aconstr_of_rawconstr vars a =
+  let a,notbindingvars,binders = aconstr_and_vars_of_rawconstr a in
   let check_type x =
-    if not (List.mem x !found or List.mem x !bound_binders) then
+    if not (List.mem x notbindingvars or List.mem x binders) then
       error ((string_of_id x)^" is unbound in the right-hand-side") in
   List.iter check_type vars;
   a
 
+let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
+
 (* Pattern-matching rawconstr and aconstr *)
 
 let rec adjust_scopes = function
@@ -260,6 +355,9 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
   | RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma
   | RApp (_,f1,l1), AApp (f2,l2) when List.length l1 = List.length l2 ->
       List.fold_left2 (match_ alp metas) (match_ alp metas sigma f1 f2) l1 l2
+  | RApp (_,f1,l1), AList (x,y,(AApp (f2,l2) as iter),termin) 
+      when List.length l1 = List.length l2 ->
+      match_alist alp metas sigma (f1::l1) (f2::l2) x y iter termin
   | RLambda (_,na1,t1,b1), ALambda (na2,t2,b2) ->
      match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2
   | RProd (_,na1,t1,b1), AProd (na2,t2,b2) ->
@@ -285,6 +383,27 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
   | (RDynamic _ | RRec _ | REvar _), _ 
   | _,_ -> raise No_match
 
+and match_alist alp metas sigma l1 l2 x y iter termin =
+  (* match the iterator at least once *)
+  let sigma = List.fold_left2 (match_ alp (y::metas)) sigma l1 l2 in
+  (* Recover the recursive position *)
+  let rest = List.assoc y sigma in
+  (* Recover the first element *)
+  let t1 = List.assoc x sigma in
+  let sigma = List.remove_assoc x (List.remove_assoc y sigma) in
+  (* try to find the remaining elements or the terminator *)
+  let rec match_alist_tail alp metas sigma acc rest =
+    try 
+      let sigma = match_ alp (y::metas) sigma rest iter in
+      let rest = List.assoc y sigma in
+      let t = List.assoc x sigma in
+      let sigma = List.remove_assoc x (List.remove_assoc y sigma) in
+      match_alist_tail alp metas sigma (t::acc) rest
+    with No_match ->
+      List.rev acc, match_ alp metas sigma rest termin in
+  let tl,sigma = match_alist_tail alp metas sigma [t1] rest in
+  (x,encode_list_value tl)::sigma
+
 and match_binders alp metas sigma b1 b2 na1 na2 = match (na1,na2) with
   | (Name id1,Name id2) when List.mem id2 metas ->
       let sigma = bind_env sigma id2 (RVar (dummy_loc,id1)) in 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index a56a96dea6..1fe1f95cda 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -27,6 +27,7 @@ type aconstr =
   | ARef of global_reference
   | AVar of identifier
   | AApp of aconstr * aconstr list
+  | AList of identifier * identifier * aconstr * aconstr
   (* Part only in rawconstr *)
   | ALambda of name * aconstr * aconstr
   | AProd of name * aconstr * aconstr
@@ -166,3 +167,6 @@ type module_type_ast =
 type module_ast = 
   | CMEident of qualid located
   | CMEapply of module_ast * module_ast
+
+(* Special identifier to encode recursive notations *)
+val ldots_var : identifier
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index c8f167eb3b..20cec7a959 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -94,6 +94,10 @@ let make_act (f : loc -> constr_expr action_env -> constr_expr) pil =
     | Some (p, ETBigint) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:Bignat.bigint) ->
 	  make ((p,CNumeral (dummy_loc,v)) :: env) tl)
+    | Some (p, ETConstrList _) :: tl ->
+        Gramext.action (fun (v:constr_expr list) ->
+          let dummyid = Ident (dummy_loc,id_of_string "") in
+	  make ((p,CAppExpl (dummy_loc,(None,dummyid),v)) :: env) tl)
     | Some (p, ETPattern) :: tl -> 
 	failwith "Unexpected entry of type cases pattern" in
   make [] (List.rev pil)
@@ -116,11 +120,16 @@ let make_act_in_cases_pattern (* For Notations *)
     | Some (p, ETBigint) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:Bignat.bigint) ->
 	  make ((p,CPatNumeral (dummy_loc,v)) :: env) tl)
+    | Some (p, ETConstrList _) :: tl ->
+        Gramext.action (fun (v:cases_pattern_expr list) ->
+          let dummyid = Ident (dummy_loc,id_of_string "") in
+	  make ((p,CPatCstr (dummy_loc,dummyid,v)) :: env) tl)
     | Some (p, (ETPattern | ETOther _)) :: tl -> 
 	failwith "Unexpected entry of type cases pattern or other" in
   make [] (List.rev pil)
 
-let make_cases_pattern_act (* For Grammar *)
+(* For V7 Grammar only *)
+let make_cases_pattern_act
   (f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil =
   let rec make (env : cases_pattern_expr action_env) = function
     | [] ->
@@ -134,7 +143,7 @@ let make_cases_pattern_act (* For Grammar *)
 	  tl)
     | Some (p, ETBigint) :: tl -> (* non-terminal *)
 	Gramext.action (fun v -> make ((p,CPatNumeral(dummy_loc,v)) :: env) tl)
-    | Some (p, (ETIdent | ETConstr _ | ETOther _)) :: tl ->
+    | Some (p, (ETConstrList _ | ETIdent | ETConstr _ | ETOther _)) :: tl ->
 	error "ident and constr entry not admitted in patterns cases syntax extensions" in
   make [] (List.rev pil)
 
@@ -145,16 +154,10 @@ let make_cases_pattern_act (* For Grammar *)
  * annotations are added when type-checking the command, function
  * Extend.of_ast) *)
 
-let rec build_prod_item univ assoc fromlevel pat = function
-  | ProdList0 s -> Gramext.Slist0 (build_prod_item univ assoc fromlevel pat s)
-  | ProdList1 s -> Gramext.Slist1 (build_prod_item univ assoc fromlevel pat s)
-  | ProdOpt s   -> Gramext.Sopt   (build_prod_item univ assoc fromlevel pat s)
-  | ProdPrimitive typ -> symbol_of_production assoc fromlevel pat typ
-
 let symbol_of_prod_item univ assoc from forpat = function
   | Term tok -> (Gramext.Stoken tok, None)
   | NonTerm (nt, ovar) ->
-      let eobj = build_prod_item univ assoc from forpat nt in
+      let eobj = symbol_of_production assoc from forpat nt in
       (eobj, ovar)
 
 let coerce_to_id = function
@@ -252,7 +255,9 @@ let subst_constr_expr a loc subs =
          subst t,subst d)) dl)
   in subst a
 
+(* For V7 Grammar only *)
 let make_rule univ assoc etyp rule =
+  if not !Options.v7 then anomaly "No Grammar in new syntax";
   let pil = List.map (symbol_of_prod_item univ assoc etyp false) rule.gr_production in
   let (symbs,ntl) = List.split pil in
   let act = match etyp with
@@ -264,13 +269,14 @@ let make_rule univ assoc etyp rule =
 	      CPatDelimiters (loc,s,a)
           | _ -> error "Unable to handle this grammar extension of pattern" in
 	make_cases_pattern_act f ntl
-    | ETIdent | ETBigint | ETReference -> error "Cannot extend"
+    | ETConstrList _ | ETIdent | ETBigint | ETReference -> error "Cannot extend"
     | ETConstr _ | ETOther _ -> 
 	make_act (subst_constr_expr rule.gr_action) ntl in
   (symbs, act)
 
 (* Rules of a level are entered in reverse order, so that the first rules
    are applied before the last ones *)
+(* For V7 Grammar only *)
 let extend_entry univ (te, etyp, pos, name, ass, p4ass, rls) =
   let rules = List.rev (List.map (make_rule univ ass etyp) rls) in
   grammar_extend te pos [(name, p4ass, rules)]
@@ -282,6 +288,7 @@ let define_entry univ {ge_name=typ; gl_assoc=ass; gl_rules=rls} =
   (e,typ,pos,name,ass,p4ass,rls)
 
 (* Add a bunch of grammar rules. Does not check if it is well formed *)
+(* For V7 Grammar only *)
 let extend_grammar_rules gram =
   let univ = get_univ gram.gc_univ in
   let tl = List.map (define_entry univ) gram.gc_entries in
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 89a3da95f1..0fd620e3c3 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -33,6 +33,7 @@ type ('lev,'pos) constr_entry_key =
   | ETConstr of ('lev * 'pos)
   | ETPattern
   | ETOther of string * string
+  | ETConstrList of ('lev * 'pos) * Token.pattern list
 
 type constr_production_entry =
     (production_level,production_position) constr_entry_key
@@ -41,14 +42,14 @@ type simple_constr_production_entry = (production_level,unit) constr_entry_key
 
 type nonterm_prod =
   | ProdList0 of nonterm_prod
-  | ProdList1 of nonterm_prod
+  | ProdList1 of nonterm_prod * Token.pattern list
   | ProdOpt of nonterm_prod
   | ProdPrimitive of constr_production_entry
 
 type prod_item =
   | Term of Token.pattern
-  | NonTerm of
-      nonterm_prod * (Names.identifier * constr_production_entry) option
+  | NonTerm of constr_production_entry *
+      (Names.identifier * constr_production_entry) option
 
 type grammar_rule = {
   gr_name : string; 
@@ -236,10 +237,10 @@ let prod_item univ env = function
   | VTerm s -> env, Term (terminal s)
   | VNonTerm (loc, nt, Some p) ->
      let typ = nterm loc univ nt in
-      (p :: env, NonTerm (ProdPrimitive typ, Some (p,typ)))
+      (p :: env, NonTerm (typ, Some (p,typ)))
   | VNonTerm (loc, nt, None) ->
       let typ = nterm loc univ nt in 
-      env, NonTerm (ProdPrimitive typ, None)
+      env, NonTerm (typ, None)
 
 let rec prod_item_list univ penv pil current_pos =
   match pil with
@@ -256,7 +257,7 @@ let gram_rule univ (name,pil,act) =
   { gr_name = name; gr_production = pilc; gr_action = a }
 
 let border = function
-  | NonTerm (ProdPrimitive (ETConstr(_,BorderProd (_,a))),_) :: _ -> a
+  | NonTerm (ETConstr(_,BorderProd (_,a)),_) :: _ -> a
   | _ -> None
 
 let clever_assoc ass g =
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 4aae3e3094..a95f1134b0 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -34,6 +34,7 @@ type ('lev,'pos) constr_entry_key =
   | ETConstr of ('lev * 'pos)
   | ETPattern
   | ETOther of string * string
+  | ETConstrList of ('lev * 'pos) * Token.pattern list
 
 type constr_production_entry =
     (production_level,production_position) constr_entry_key
@@ -42,14 +43,14 @@ type simple_constr_production_entry = (production_level,unit) constr_entry_key
 
 type nonterm_prod =
   | ProdList0 of nonterm_prod
-  | ProdList1 of nonterm_prod
+  | ProdList1 of nonterm_prod * Token.pattern list
   | ProdOpt of nonterm_prod
   | ProdPrimitive of constr_production_entry
 
 type prod_item =
   | Term of Token.pattern
-  | NonTerm of
-      nonterm_prod * (Names.identifier * constr_production_entry) option
+  | NonTerm of constr_production_entry * 
+      (Names.identifier * constr_production_entry) option
 
 type grammar_rule = {
   gr_name : string; 
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index 606949e5f9..bf4c3372ef 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -180,7 +180,9 @@ GEXTEND Gram
     | "10" LEFTA
       [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args)
       | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) ]
-    | "9" [ ]
+    | "9"
+        [ ".."; ".."; c = operconstr LEVEL "0"; ".."; ".." ->
+          CAppExpl (loc,(None,Ident (loc,Topconstr.ldots_var)),[c]) ]
     | "1" LEFTA
       [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
 	CApp(loc,(Some (List.length args+1),CRef f),args@[c,None])
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 5ef39419c6..5e48e5edac 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -722,6 +722,7 @@ let compute_entry allow_create adjust forpat = function
   | ETPattern -> weaken_entry Constr.pattern, None, false
   | ETOther ("constr","annot") -> 
       weaken_entry Constr.annot, None, false
+  | ETConstrList _ -> error "List of entries cannot be registered"
   | ETOther (u,n) ->
       let u = get_univ u in
       let e =
@@ -776,12 +777,23 @@ let is_binder_level from e =
       ETConstr(200,()), ETConstr(NumLevel 200,_) -> not !Options.v7
     | _ -> false
 
-let symbol_of_production assoc from forpat typ =
+let rec symbol_of_production assoc from forpat typ =
   if is_binder_level from typ then
     let eobj = snd (get_entry (get_univ "constr") "operconstr") in
     Gramext.Snterml (Gram.Entry.obj eobj,"200")
   else if is_self from typ then Gramext.Sself
   else
+    match typ with
+    | ETConstrList (typ',[]) ->
+        Gramext.Slist1 (symbol_of_production assoc from forpat (ETConstr typ'))
+    | ETConstrList (typ',tkl) ->
+        Gramext.Slist1sep
+          (symbol_of_production assoc from forpat (ETConstr typ'),
+           Gramext.srules
+             [List.map (fun x -> Gramext.Stoken x) tkl,
+              List.fold_right (fun _ v -> Gramext.action (fun _ -> v)) tkl
+                (Gramext.action (fun loc -> ()))])
+    | _ ->
     match get_constr_production_entry assoc from forpat typ with
       | (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj)
       | (eobj,Some None,_) -> Gramext.Snext
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 335d3b7964..f30ac61cb9 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -45,17 +45,32 @@ let env_assoc_value v env =
   try List.nth env (v-1)
   with Not_found -> anomaly "Inconsistent environment for pretty-print rule"
 
+let decode_constrlist_value = function
+  | CAppExpl (_,_,l) -> l
+  | CApp (_,_,l) -> List.map fst l
+  | _ -> anomaly "Ill-formed list argument of notation"
+
+let decode_patlist_value = function
+  | CPatCstr (_,_,l) -> l
+  | _ -> anomaly "Ill-formed list argument of notation"
+
 open Symbols
 
-let rec print_hunk n pr env = function
+let rec print_hunk n decode pr env = function
   | UnpMetaVar (e,prec) -> pr (n,prec) (env_assoc_value e env)
+  | UnpListMetaVar (e,prec,sl) -> 
+      prlist_with_sep (fun () -> prlist (print_hunk n decode pr env) sl)
+      (pr (n,prec)) (decode (env_assoc_value e env))
   | UnpTerminal s -> str s
-  | UnpBox (b,sub) -> ppcmd_of_box b (prlist (print_hunk n pr env) sub)
+  | UnpBox (b,sub) -> ppcmd_of_box b (prlist (print_hunk n decode pr env) sub)
   | UnpCut cut -> ppcmd_of_cut cut
 
-let pr_notation pr s env =
+let pr_notation_gen decode pr s env =
   let unpl, level = find_notation_printing_rule s in
-  prlist (print_hunk level pr env) unpl, level
+  prlist (print_hunk level decode pr env) unpl, level
+
+let pr_notation = pr_notation_gen decode_constrlist_value
+let pr_patnotation = pr_notation_gen decode_patlist_value
 
 let pr_delimiters key strm =
   let left = "'"^key^":" and right = "'" in
@@ -206,7 +221,7 @@ let rec pr_cases_pattern _inh = function
   | CPatAtom (_,None) -> str "_"
   | CPatNotation (_,"( _ )",[p]) ->
       str"("++ pr_cases_pattern _inh p ++ str")"
-  | CPatNotation (_,s,env) -> fst (pr_notation pr_cases_pattern s env)
+  | CPatNotation (_,s,env) -> fst (pr_patnotation pr_cases_pattern s env)
   | CPatNumeral (_,n) -> Bignat.pr_bigint n
   | CPatDelimiters (_,key,p) -> pr_delimiters key (pr_cases_pattern _inh p)
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a75ca26bd2..b68ce1c4ee 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -379,23 +379,65 @@ let quote_notation_token x =
   if (n > 0 & norm) or (n > 2 & x.[0] = '\'') then "'"^x^"'"
   else x
 
-let rec analyse_notation_tokens = function
+let rec raw_analyse_notation_tokens = function
   | []    -> [], []
+  | String ".." :: sl ->
+      let (vars,l) = raw_analyse_notation_tokens sl in
+      (list_add_set ldots_var vars, NonTerminal ldots_var :: l)
   | String x :: sl when is_normal_token x ->
       Lexer.check_ident x;
       let id = Names.id_of_string x in
-      let (vars,l) = analyse_notation_tokens sl in
+      let (vars,l) = raw_analyse_notation_tokens sl in
       if List.mem id vars then
 	error ("Variable "^x^" occurs more than once");
       (id::vars, NonTerminal id :: l)
   | String s :: sl ->
       Lexer.check_keyword s;
-      let (vars,l) = analyse_notation_tokens sl in
+      let (vars,l) = raw_analyse_notation_tokens sl in
       (vars, Terminal (unquote_notation_token s) :: l)
   | WhiteSpace n :: sl ->
-      let (vars,l) = analyse_notation_tokens sl in
+      let (vars,l) = raw_analyse_notation_tokens sl in
       (vars, Break n :: l)
 
+let rec find_pattern xl = function
+  | Break n as x :: l, Break n' :: l' when n=n' -> 
+      find_pattern (x::xl) (l,l')
+  | Terminal s as x :: l, Terminal s' :: l' when s = s' -> 
+      find_pattern (x::xl) (l,l')
+  | [NonTerminal x], NonTerminal x' :: l' ->
+      (x,x',xl),l'
+  | [NonTerminal _], Terminal s :: _ | Terminal s :: _, _ ->
+      error ("The token "^s^" occurs on one side of \"..\" but not on the other side")
+  | [NonTerminal _], Break s :: _ | Break s :: _, _ ->
+      error ("A break occurs on one side of \"..\" but not on the other side")
+  | ((SProdList _ | NonTerminal _) :: _ | []), _ -> assert false
+
+let rec interp_list_parser hd = function
+  | [] -> [], List.rev hd
+  | NonTerminal id :: tl when id = ldots_var ->
+      let ((x,y,sl),tl') = find_pattern [] (hd,tl) in
+      let yl,tl'' = interp_list_parser [] tl' in
+      (* We remember the second copy of each recursive part variable to *)
+      (* remove it afterwards *)
+      y::yl, SProdList (x,sl) :: tl''
+  | (Terminal _ | Break _) as s :: tl ->
+      if hd = [] then 
+        let yl,tl' = interp_list_parser [] tl in
+        yl, s :: tl'
+      else
+        interp_list_parser (s::hd) tl
+  | NonTerminal _ as x :: tl ->
+      let yl,tl' = interp_list_parser [x] tl in
+      yl, List.rev_append hd tl'
+  | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser"
+
+let analyse_notation_tokens l =
+  let vars,l = raw_analyse_notation_tokens l in
+  let recvars,l = interp_list_parser [] l in
+  ((if recvars = [] then [] else ldots_var::recvars), vars, l)
+
+let remove_vars = List.fold_right List.remove_assoc
+ 
 (* Build the syntax and grammar rules *)
 
 type printing_precedence = int * parenRelation
@@ -495,6 +537,9 @@ let make_hunks_ast symbols etyps from =
     | Break n :: prods ->
 	add_break n (make NoBreak prods)
 
+    | SProdList _ :: _ ->
+        anomaly "Recursive notations not supported in old syntax"
+
     | [] -> []
 
   in make NoBreak symbols
@@ -549,6 +594,11 @@ let make_hunks etyps symbols from =
     | Break n :: prods ->
 	add_break n (make NoBreak prods)
 
+    | SProdList (m,sl) :: prods ->
+	let i = list_index m vars in
+	let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
+	UnpListMetaVar (i,prec,make NoBreak sl) :: make CanBreak prods
+
     | [] -> []
 
   in make NoBreak symbols
@@ -615,11 +665,22 @@ let make_production etyps symbols =
       (fun t l -> match t with
         | NonTerminal m ->
 	    let typ = List.assoc m etyps in
-	    NonTerm (ProdPrimitive typ, Some (m,typ)) :: l
+	    NonTerm (typ, Some (m,typ)) :: l
         | Terminal s ->
 	    Term (Extend.terminal s) :: l
         | Break _ ->
-	    l)
+            l
+        | SProdList (x,sl) ->
+            let sl = List.flatten
+              (List.map (function Terminal s -> [Extend.terminal s] 
+                | Break _ -> []
+                | _ -> anomaly "Found a non terminal token in recursive notation separator") sl) in
+	    let y = match List.assoc x etyps with
+              | ETConstr x -> x
+              | _ ->
+                  error "Component of recursive patterns in notation must be constr" in
+            let typ = ETConstrList (y,sl) in
+            NonTerm (typ, Some (x,typ)) :: l)
       symbols [] in
   define_keywords prod
 
@@ -630,6 +691,8 @@ let rec find_symbols c_current c_next c_last = function
       (id, prec) :: (find_symbols c_next c_next c_last sl)
   | Terminal s :: sl -> find_symbols c_next c_next c_last sl
   | Break n :: sl -> find_symbols c_current c_next c_last sl
+  | SProdList (x,_) :: sl' -> 
+      (x,c_next)::(find_symbols c_next c_next c_last sl')
 
 let border = function
   | (_,ETConstr(_,BorderProd (_,a))) :: _ -> a
@@ -643,9 +706,8 @@ let recompute_assoc typs =
     | _ -> None
 
 let rec expand_squash = function
-  | Term ("","{") :: NonTerm (ProdPrimitive (ETConstr _), n) :: Term ("","}")
-    :: l ->
-      NonTerm (ProdPrimitive (ETConstr (NextLevel,InternalProd)),n)
+  | Term ("","{") :: NonTerm (ETConstr _, n) :: Term ("","}") :: l ->
+      NonTerm (ETConstr (NextLevel,InternalProd),n)
       :: expand_squash l
   | a :: l -> a :: expand_squash l
   | [] -> []
@@ -676,9 +738,6 @@ let make_syntax_rule n name symbols typs ast ntn sc =
     syn_hunks =
       [UNP_SYMBOLIC(sc,ntn,UNP_BOX (PpHOVB 1,make_hunks_ast symbols typs n))]}]
 
-let make_pp_rule (n,typs,symbols) =
-  [UnpBox (PpHOVB 0, make_hunks typs symbols n)]
-
 let make_pp_rule (n,typs,symbols,fmt) =
   match fmt with
     | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)]
@@ -827,6 +886,7 @@ let set_entry_type etyps (x,typ) =
           ETConstr (n,BorderProd (left,None))
       | ETConstr (n,()), (_,InternalProd) -> ETConstr (n,InternalProd)
       | (ETPattern | ETIdent | ETBigint | ETOther _ | ETReference as t), _ -> t
+      | (ETConstrList _, _) -> assert false
     with Not_found -> ETConstr typ
   in (x,typ)
 
@@ -862,6 +922,7 @@ let find_precedence lev etyps symbols =
 	    if lev = None then
 	      error "Need an explicit level"
 	    else out_some lev
+        | ETConstrList _ -> assert false (* internally used in grammar only *)
       with Not_found -> 
 	if lev = None then
 	  error "A left-recursive notation must have an explicit level"
@@ -910,8 +971,7 @@ let compute_syntax_data forv7 (df,modifiers) =
   (* Notation defaults to NONA *)
   let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
   let toks = split_notation_string df in
-  let innerlevel = NumLevel (if forv7 then 10 else 200) in
-  let (vars,symbols) = analyse_notation_tokens toks in
+  let (recvars,vars,symbols) = analyse_notation_tokens toks in
   let ntn_for_interp = make_notation_key symbols in
   let symbols = remove_curly_brackets symbols in
   let notation = make_notation_key symbols in
@@ -919,6 +979,7 @@ let compute_syntax_data forv7 (df,modifiers) =
   let n =
     if !Options.v7 then find_precedence_v7 n etyps symbols
     else find_precedence n etyps symbols in
+  let innerlevel = NumLevel (if forv7 then 10 else 200) in
   let typs =
     find_symbols
       (NumLevel n,BorderProd(true,assoc))
@@ -929,20 +990,21 @@ let compute_syntax_data forv7 (df,modifiers) =
   let typs = List.map (set_entry_type etyps) typs in
   let ppdata = (n,typs,symbols,fmt) in
   let prec = (n,List.map (assoc_of_type n) typs) in
-  ((onlyparse,vars,ntn_for_interp,notation),prec,ppdata,(Lib.library_dp(),df))
+  ((onlyparse,recvars,vars,
+    ntn_for_interp,notation),prec,ppdata,(Lib.library_dp(),df))
 
 let add_syntax_extension local mv mv8 =
   let data8 = option_app (compute_syntax_data false) mv8 in
   let data = option_app (compute_syntax_data !Options.v7) mv in
   let prec,gram_rule = match data with
   | None -> None, None
-  | Some ((_,_,_,notation),prec,(n,typs,symbols,_),_) -> 
+  | Some ((_,_,_,_,notation),prec,(n,typs,symbols,_),_) -> 
       Some prec, Some (make_grammar_rule n typs symbols notation None) in
   match data, data8 with
   | None, None -> (* Nothing to do: V8Notation while not translating *) () 
   | _, Some d | Some d, None ->
-    let ((_,_,_,ntn),ppprec,ppdata,_) = d in
-    let ntn' = match data with Some ((_,_,_,ntn),_,_,_) -> ntn | _ -> ntn in
+    let ((_,_,_,_,ntn),ppprec,ppdata,_) = d in
+    let ntn' = match data with Some ((_,_,_,_,ntn),_,_,_) -> ntn | _ -> ntn in
     let pp_rule = make_pp_rule ppdata in
     Lib.add_anonymous_leaf
       (inSyntaxExtension (local,(prec,ppprec),ntn',gram_rule,pp_rule))
@@ -1042,7 +1104,7 @@ let contract_notation ntn =
   aux ntn 0
 
 let add_notation_in_scope local df c mods omodv8 scope toks =
-  let ((onlyparse,vars,intnot,notation),prec,(n,typs,symbols,_ as ppdata),df')=
+  let ((onlyparse,recs,vars,intnot,notation),prec,(n,typs,symbols,_ as ppdata),df')=
     compute_syntax_data !Options.v7 (df,mods) in
   (* Declare the parsing and printing rules if not already done *)
     (* For both v7 and translate: parsing is as described for v7 in v7 file *)
@@ -1053,13 +1115,13 @@ let add_notation_in_scope local df c mods omodv8 scope toks =
     (* In short: parsing does not depend on omodv8 *)
     (* Printing depends on mv8 if defined, otherwise of mods (scaled by 10) *)
     (* if in v7, or of mods without scaling if in v8 *)
-  let intnot,ntn,ppvars,ppprec,pp_rule =
+  let intnot,ntn,pprecvars,ppvars,ppprec,pp_rule =
     match omodv8 with
     | Some mv8 ->
-        let (_,vars8,intnot8,ntn8),p,d,_ = compute_syntax_data false mv8 in
-        intnot8,ntn8,vars8,p,make_pp_rule d
+        let (_,recs8,vars8,intnot8,ntn8),p,d,_ = compute_syntax_data false mv8 in
+        intnot8,ntn8,recs8,vars8,p,make_pp_rule d
     | None when not !Options.v7 -> 
-        intnot,notation,vars,prec,make_pp_rule ppdata
+        intnot,notation,recs,vars,prec,make_pp_rule ppdata
     | None ->
 	(* means the rule already exists: recover it *)
         (* occurs only with V8only flag alone *)
@@ -1067,7 +1129,7 @@ let add_notation_in_scope local df c mods omodv8 scope toks =
           let ntn = contract_notation notation in
 	  let _, oldprec8 = Symbols.level_of_notation ntn in
 	  let rule,_ = Symbols.find_notation_printing_rule ntn in
-	  notation,ntn,vars,oldprec8,rule
+	  notation,ntn,recs,vars,oldprec8,rule
 	with Not_found -> error "No known parsing rule for this notation in V8"
   in
   let permut = mk_permut vars ppvars in
@@ -1077,15 +1139,15 @@ let add_notation_in_scope local df c mods omodv8 scope toks =
       (local,(Some prec,ppprec),ntn,Some gram_rule,pp_rule));
 
   (* Declare interpretation *)
-  let a = interp_aconstr [] ppvars c in
+  let (acvars,ac) = interp_aconstr [] ppvars c in
+  let a = (remove_vars pprecvars acvars,ac) (* For recursive parts *) in
   let old_pp_rule =
-    (* Used only by v7 *)
-    if onlyparse then None
+    (* Used only by v7; disable if contains a recursive pattern *)
+    if onlyparse or pprecvars <> [] then None
     else
       let r = interp_global_rawconstr_with_vars vars c in
       Some (make_old_pp_rule n symbols typs r intnot scope vars) in
   let onlyparse = onlyparse or !Options.v7_only in
-  let vars = List.map (fun id -> id,[] (* insert the right scope *)) vars in
   Lib.add_anonymous_leaf
     (inNotation(local,old_pp_rule,intnot,scope,a,onlyparse,false,df'))
 
@@ -1102,6 +1164,11 @@ let exists_notation_syntax ntn =
   try fst (Symbols.level_of_notation (contract_notation ntn)) <> None
   with Not_found -> false
 
+let set_data_for_v7_pp recs a vars =
+  if not !Options.v7 then None else
+    if recs=[] then Some (a,vars)
+    else (warning "No recursive notation in v7 syntax";None)
+
 let build_old_pp_rule notation scope symbs (r,vars) =
   let prec = 
     try
@@ -1126,22 +1193,24 @@ let add_notation_interpretation_core local symbs for_old df a scope onlyparse
      (Lib.library_dp(),df)))
 
 let add_notation_interpretation df names c sc =
-  let (vars,symbs) = analyse_notation_tokens (split_notation_string df) in
+  let (recs,vars,symbs) = analyse_notation_tokens (split_notation_string df) in
   check_notation_existence (make_notation_key symbs);
-  let a = interp_aconstr names vars c in
+  let (acvars,ac) = interp_aconstr names vars c in
+  let a = (remove_vars recs acvars,ac) (* For recursive parts *) in
   let a_for_old = interp_rawconstr_with_implicits (Global.env()) vars names c 
   in
-  let for_oldpp = Some (a_for_old,vars) in
+  let for_oldpp = set_data_for_v7_pp recs a_for_old vars in
   add_notation_interpretation_core false symbs for_oldpp df a sc false false
 
 let add_notation_in_scope_v8only local df c mv8 scope toks =
-  let (_,vars,intnot,notation),prec,ppdata,df' = compute_syntax_data false (df,mv8) in
+  let (_,recs,vars,intnot,notation),prec,ppdata,df' = compute_syntax_data false (df,mv8) in
   let pp_rule = make_pp_rule ppdata in
   Lib.add_anonymous_leaf
     (inSyntaxExtension(local,(None,prec),notation,None,pp_rule));
   (* Declare the interpretation *)
   let onlyparse = false in
-  let a = interp_aconstr [] vars c in
+  let (acvars,ac) = interp_aconstr [] vars c in
+  let a = (remove_vars recs acvars,ac) (* For recursive parts *) in
   Lib.add_anonymous_leaf
     (inNotation(local,None,intnot,scope,a,onlyparse,true,df'))
 
@@ -1159,10 +1228,10 @@ let add_notation_v8only local c (df,modifiers) sc =
 		error "Parsing rule for this notation includes no level"
 	      else
 	        (* Declare only interpretation *)
-		let (vars,symbs) = analyse_notation_tokens toks in
+		let (recs,vars,symbs) = analyse_notation_tokens toks in
 		let onlyparse = modifiers = [SetOnlyParsing] in
-		let a = interp_aconstr [] vars c in
-		let a_for_old = interp_global_rawconstr_with_vars vars c in
+                let (acvars,ac) = interp_aconstr [] vars c in
+                let a = (remove_vars recs acvars,ac) in
 		add_notation_interpretation_core local symbs None df a sc 
 		  onlyparse true
 	  | Some n ->
@@ -1194,12 +1263,13 @@ let add_notation local c dfmod mv8 sc =
 		error "Parsing rule for this notation includes no level"
 	      else
 	        (* Declare only interpretation *)
-		let (vars,symbs) = analyse_notation_tokens toks in
+		let (recs,vars,symbs) = analyse_notation_tokens toks in
                 if exists_notation_syntax (make_notation_key symbs) then
 		  let onlyparse = modifiers = [SetOnlyParsing] in
-		  let a = interp_aconstr [] vars c in
+                  let (acvars,ac) = interp_aconstr [] vars c in
+                  let a = (remove_vars recs acvars,ac) in
 		  let a_for_old = interp_global_rawconstr_with_vars vars c in
-		  let for_old = Some (a_for_old,vars) in
+                  let for_old = set_data_for_v7_pp recs a_for_old vars in
 		  add_notation_interpretation_core local symbs for_old df a
 		    sc onlyparse false
                 else
@@ -1263,8 +1333,9 @@ let add_infix local (inf,modl) pr mv8 sc =
     let toks = split_notation_string df in
     if a8=None & n8=None & fmt=None then
       (* Declare only interpretation *)
-      let (vars,symbs) = analyse_notation_tokens toks in
-      let a' = interp_aconstr [] vars a in
+      let (recs,vars,symbs) = analyse_notation_tokens toks in
+      let (acvars,ac) = interp_aconstr [] vars a in
+      let a' = (remove_vars recs acvars,ac) in
       let a_for_old = interp_global_rawconstr_with_vars vars a in
       add_notation_interpretation_core local symbs None df a' sc 
 	onlyparse true
@@ -1291,11 +1362,12 @@ let add_infix local (inf,modl) pr mv8 sc =
     (* En v8, une notation sans information de parsing signifie *)
     (* de ne déclarer que l'interprétation *)
     (* Declare only interpretation *)
-    let (vars,symbs) = analyse_notation_tokens toks in
+    let (recs,vars,symbs) = analyse_notation_tokens toks in
     if exists_notation_syntax (make_notation_key symbs) then
-      let a' = interp_aconstr [] vars a in
+      let (acvars,ac) = interp_aconstr [] vars a in
+      let a' = (remove_vars recs acvars,ac) in
       let a_for_old = interp_global_rawconstr_with_vars vars a in
-      let for_old = Some (a_for_old,vars) in
+      let for_old = set_data_for_v7_pp recs a_for_old vars in
       add_notation_interpretation_core local symbs for_old df a' sc 
         onlyparse false
     else
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 753ac89ddf..164889adf8 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -61,17 +61,32 @@ let env_assoc_value v env =
   try List.nth env (v-1)
   with Not_found -> anomaly ("Inconsistent environment for pretty-print rule")
 
+let decode_constrlist_value = function
+  | CAppExpl (_,_,l) -> l
+  | CApp (_,_,l) -> List.map fst l
+  | _ -> anomaly "Ill-formed list argument of notation"
+
+let decode_patlist_value = function
+  | CPatCstr (_,_,l) -> l
+  | _ -> anomaly "Ill-formed list argument of notation"
+
 open Symbols
 
-let rec print_hunk n pr env = function
+let rec print_hunk n decode pr env = function
   | UnpMetaVar (e,prec) -> pr (n,prec) (env_assoc_value e env)
+  | UnpListMetaVar (e,prec,sl) -> 
+      prlist_with_sep (fun () -> prlist (print_hunk n decode pr env) sl)
+      (pr (n,prec)) (decode (env_assoc_value e env))
   | UnpTerminal s -> str s
-  | UnpBox (b,sub) -> ppcmd_of_box b (prlist (print_hunk n pr env) sub)
+  | UnpBox (b,sub) -> ppcmd_of_box b (prlist (print_hunk n decode pr env) sub)
   | UnpCut cut -> ppcmd_of_cut cut
 
-let pr_notation pr s env =
+let pr_notation_gen decode pr s env =
   let unpl, level = find_notation_printing_rule s in
-  prlist (print_hunk level pr env) unpl, level
+  prlist (print_hunk level decode pr env) unpl, level
+
+let pr_notation = pr_notation_gen decode_constrlist_value
+let pr_patnotation = pr_notation_gen decode_patlist_value
 
 let pr_delimiters key strm =
   strm ++ str ("%"^key)
@@ -154,7 +169,7 @@ let rec pr_patt sep inh p =
   | CPatAtom (_,Some r) -> pr_reference r, latom
   | CPatNotation (_,"( _ )",[p]) ->
       pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
-  | CPatNotation (_,s,env) -> pr_notation (pr_patt mt) s env
+  | CPatNotation (_,s,env) -> pr_patnotation (pr_patt mt) s env
   | CPatNumeral (_,i) -> Bignat.pr_bigint i, latom
   | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1
   in
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 2fd54a006a..adfddea7b4 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -130,6 +130,7 @@ let pr_set_entry_type = function
   | ETConstr _ -> str"constr"
   | ETOther (_,e) -> str e
   | ETBigint -> str "bigint"
+  | ETConstrList _ -> failwith "Internal entry type"
 
 let pr_non_terminal = function
   | NtQual (u,nt) -> (* no more qualified entries *) str nt
@@ -522,9 +523,12 @@ let rec pr_vernac = function
 *)      
   | VernacSyntax (u,el) ->
       msgerrnl (str"Warning : Syntax is discontinued; use Notation");
-      str"(* Syntax is discontinued " ++
+      str"(* <Warning> : Syntax is discontinued" ++ 
+(*
+      fnl () ++
       hov 1 (str"Syntax " ++ str u ++ spc() ++
       prlist_with_sep sep_v2 pr_syntax_entry el) ++ 
+*)
       str " *)"
   | VernacOpenCloseScope (local,opening,sc) ->
       str (if opening then "Open " else "Close ") ++ pr_locality local ++