Affichage des notations récursives:

- Prise en compte des notations applicatives
- Remplacement du codage des arguments liste des notations récursives 
  sous forme de terme par une représentation directe (permet notamment
  de résoudre un problème de stack overflow de la fonction d'affichage)
+ Correction bug affichage Lemma dans ppvernac.ml
+ Divers util.ml



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

9 files changed, 191 insertions, 154 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index a3393863b..add71a8b0 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -190,8 +190,9 @@ let rec check_same_type ty1 ty2 =
       check_same_type b1 b2
   | CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) ->
       check_same_type a1 a2
-  | CNotation(_,n1,e1), CNotation(_,n2,e2) when n1=n2 ->
-      List.iter2 check_same_type e1 e2
+  | CNotation(_,n1,(e1,el1)), CNotation(_,n2,(e2,el2)) when n1=n2 ->
+      List.iter2 check_same_type e1 e2;
+      List.iter2 (List.iter2 check_same_type) el1 el2
   | CPrim(_,i1), CPrim(_,i2) when i1=i2 -> ()
   | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when s1=s2 ->
       check_same_type e1 e2
@@ -298,7 +299,7 @@ and spaces ntn n =
   if n = String.length ntn then []
   else if ntn.[n] = ' ' then wildcards ntn (n+1) else spaces ntn (n+1)
 
-let expand_curly_brackets loc mknot ntn l =
+let expand_curly_brackets loc mknot ntn (l,ll) =
   let ntn' = ref ntn in
   let rec expand_ntn i =
     function
@@ -311,12 +312,12 @@ let expand_curly_brackets loc mknot ntn l =
             ntn' := 
               String.sub !ntn' 0 p ^ "_" ^ 
               String.sub !ntn' (p+5) (String.length !ntn' -p-5);
-            mknot (loc,"{ _ }",[a]) end
+            mknot (loc,"{ _ }",([a],[])) end
           else a in
         a' :: expand_ntn (i+1) l in
   let l = expand_ntn 0 l in
   (* side effect *)
-  mknot (loc,!ntn',l)
+  mknot (loc,!ntn',(l,ll))
 
 let destPrim = function CPrim(_,t) -> Some t | _ -> None
 let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None
@@ -324,18 +325,18 @@ let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None
 let make_notation_gen loc ntn mknot mkprim destprim l =
   if has_curly_brackets ntn
   then expand_curly_brackets loc mknot ntn l
-  else match ntn,List.map destprim l with
+  else match ntn,List.map destprim (fst l),(snd l) with
     (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *)
-    | "- _", [Some (Numeral p)] when Bigint.is_strictly_pos p ->
-        mknot (loc,ntn,[mknot (loc,"( _ )",l)])
+    | "- _", [Some (Numeral p)],[] when Bigint.is_strictly_pos p ->
+        mknot (loc,ntn,([mknot (loc,"( _ )",l)],[]))
     | _ -> 
 	match decompose_notation_key ntn, l with
-	| [Terminal "-"; Terminal x], [] ->
+	| [Terminal "-"; Terminal x], ([],[]) ->
 	    (try mkprim (loc, Numeral (Bigint.neg (Bigint.of_string x)))
- 	     with _ -> mknot (loc,ntn,[]))
-	| [Terminal x], [] ->
+ 	     with _ -> mknot (loc,ntn,([],[])))
+	| [Terminal x], ([],[]) ->
 	    (try mkprim (loc, Numeral (Bigint.of_string x))
- 	     with _ -> mknot (loc,ntn,[]))
+ 	     with _ -> mknot (loc,ntn,([],[])))
 	| _ ->
 	    mknot (loc,ntn,l)
 
@@ -351,13 +352,13 @@ let make_pat_notation loc ntn l =
     (fun (loc,p) -> CPatPrim (loc,p))
     destPatPrim l
 
-let bind_env sigma var v =
+let bind_env (sigma,sigmalist as fullsigma) var v =
   try
     let vvar = List.assoc var sigma in
-    if v=vvar then sigma else raise No_match
+    if v=vvar then fullsigma else raise No_match
   with Not_found ->
     (* TODO: handle the case of multiple occs in different scopes *)
-    (var,v)::sigma
+    (var,v)::sigma,sigmalist
 
 let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
   | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1
@@ -378,15 +379,18 @@ let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
         (* All parameters must be _ *)
         List.iter (function AHole _ -> () | _ -> raise No_match) p2;
 	List.fold_left2 (match_cases_pattern metas) sigma args1 args2
+  (* TODO: use recursive notations *)
   | _ -> raise No_match
 
-let match_aconstr_cases_pattern c (metas_scl,pat) =
-  let subst = match_cases_pattern (List.map fst metas_scl) [] c pat in
+let match_aconstr_cases_pattern c ((metas_scl,metaslist_scl),pat) =
+  let vars = List.map fst metas_scl @ List.map fst metaslist_scl in
+  let subst,substlist = match_cases_pattern vars ([],[]) c pat in
   (* Reorder canonically the substitution *)
   let find x subst =
-    try List.assoc x subst
+    try List.assoc x subst 
     with Not_found -> anomaly "match_aconstr_cases_pattern" in
-  List.map (fun (x,scl) -> (find x subst,scl)) metas_scl
+  List.map (fun (x,scl) -> (find x subst,scl)) metas_scl,
+  List.map (fun (x,scl) -> (find x substlist,scl)) metaslist_scl
 
  (* Better to use extern_rawconstr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
@@ -424,7 +428,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
 	  | PatCstr (loc,_,_,na),_ -> loc,na
 	  | PatVar (loc,na),_ -> loc,na in
 	(* Try matching ... *)
-	let subst = match_aconstr_cases_pattern t pat in
+	let subst,substlist = match_aconstr_cases_pattern t pat in
 	(* Try availability of interpretation ... *)
 	let p = match keyrule with
           | NotationRule (sc,ntn) ->
@@ -438,7 +442,13 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
 		    List.map (fun (c,(scopt,scl)) ->
 		      extern_cases_pattern_in_scope (scopt,scl@scopes') vars c)
                       subst in
-		  insert_pat_delimiters loc (make_pat_notation loc ntn l) key)
+		  let ll =
+		    List.map (fun (c,(scopt,scl)) ->
+		      let subscope = (scopt,scl@scopes') in
+		      List.map (extern_cases_pattern_in_scope subscope vars) c)
+                      substlist in
+		  insert_pat_delimiters loc 
+		    (make_pat_notation loc ntn (l,ll)) key)
           | SynDefRule kn ->
 	      let qid = shortest_qualid_of_syndef vars kn in
               CPatAtom (loc,Some (Qualid (loc, qid))) in
@@ -817,7 +827,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
           | _, None -> t,[]
           | _ -> raise No_match in
 	(* Try matching ... *)
-	let subst = match_aconstr t pat in
+	let subst,substlist = match_aconstr t pat in
 	(* Try availability of interpretation ... *)
         let e =
           match keyrule with
@@ -833,7 +843,11 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
 		      extern (* assuming no overloading: *) true
 		        (scopt,scl@scopes') vars c)
                       subst in
-	          insert_delimiters (make_notation loc ntn l) key)
+		  let ll =
+		    List.map (fun (c,(scopt,scl)) ->
+		      List.map (extern true (scopt,scl@scopes') vars) c)
+                      substlist in
+	          insert_delimiters (make_notation loc ntn (l,ll)) key)
           | SynDefRule kn ->
 	      let l =
 		List.map (fun (c,(scopt,scl)) ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 15c816b5b..2faa86622 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -147,31 +147,31 @@ let expand_notation_string ntn n =
 
 (* This contracts the special case of "{ _ }" for sumbool, sumor notations *)
 (* Remark: expansion of squash at definition is done in metasyntax.ml *)
-let contract_notation ntn l =
+let contract_notation ntn (l,ll) =
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
-    | CNotation (_,"{ _ }",[a]) :: l -> 
+    | CNotation (_,"{ _ }",([a],[])) :: l -> 
         ntn' := expand_notation_string !ntn' n;
         contract_squash n (a::l)
     | a :: l ->
         a::contract_squash (n+1) l in
   let l = contract_squash 0 l in
   (* side effect; don't inline *)
-  !ntn',l
+  !ntn',(l,ll)
 
-let contract_pat_notation ntn l =
+let contract_pat_notation ntn (l,ll) =
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
-    | CPatNotation (_,"{ _ }",[a]) :: l -> 
+    | CPatNotation (_,"{ _ }",([a],[])) :: l -> 
         ntn' := expand_notation_string !ntn' n;
         contract_squash n (a::l)
     | a :: l ->
         a::contract_squash (n+1) l in
   let l = contract_squash 0 l in
   (* side effect; don't inline *)
-  !ntn',l
+  !ntn',(l,ll)
 
 (**********************************************************************)
 (* Remembering the parsing scope of variables in notations            *)
@@ -191,7 +191,7 @@ let set_var_scope loc id (_,scopt,scopes) varscopes =
 (**********************************************************************)
 (* Syntax extensions                                                  *)
 
-let traverse_binder subst (renaming,(ids,tmpsc,scopes as env)) id =
+let traverse_binder (subst,substlist) (renaming,(ids,tmpsc,scopes as env)) id =
   try
     (* Binders bound in the notation are considered first-order objects *)
     let _,id' = coerce_to_id (fst (List.assoc id subst)) in
@@ -200,22 +200,21 @@ let traverse_binder subst (renaming,(ids,tmpsc,scopes as env)) id =
     (* Binders not bound in the notation do not capture variables *)
     (* outside the notation (i.e. in the substitution) *)
     let fvs1 = List.map (fun (_,(c,_)) -> free_vars_of_constr_expr c) subst in
-    let fvs2 = List.map snd renaming in
-    let fvs = List.flatten (List.map Idset.elements fvs1) @ fvs2 in
+    let fvs2 = List.flatten (List.map (fun (_,(l,_)) -> List.map free_vars_of_constr_expr l) substlist) in
+    let fvs3 = List.map snd renaming in
+    let fvs = List.flatten (List.map Idset.elements (fvs1@fvs2)) @ fvs3 in
     let id' = next_ident_away id fvs in
     let renaming' = if id=id' then renaming else (id,id')::renaming in
     (renaming',env), id'
 
-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 (renaming,(ids,_,scopes)) =
-  function
+let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c =
+  let (renaming,(ids,_,scopes)) = infos in
+  let subinfos = renaming,(ids,None,scopes) in
+  match c with
   | AVar id ->
       begin
 	(* subst remembers the delimiters stack in the interpretation *)
@@ -233,30 +232,27 @@ let rec subst_aconstr_in_rawconstr loc interp subst (renaming,(ids,_,scopes)) =
   | AList (x,_,iter,terminator,lassoc) ->
       (try 
         (* All elements of the list are in scopes (scopt,subscopes) *)
-	let (a,(scopt,subscopes)) = List.assoc x subst in
+	let (l,(scopt,subscopes)) = List.assoc x substlist in
         let termin = 
-          subst_aconstr_in_rawconstr loc interp subst 
-	    (renaming,(ids,None,scopes)) terminator in
-        let l = decode_constrlist_value a in
+          subst_aconstr_in_rawconstr loc interp sub subinfos terminator in
 	List.fold_right (fun a t -> 
           subst_iterator ldots_var t
             (subst_aconstr_in_rawconstr loc interp 
-              ((x,(a,(scopt,subscopes)))::subst)
-	      (renaming,(ids,None,scopes)) iter))
+              ((x,(a,(scopt,subscopes)))::subst,substlist) subinfos iter))
             (if lassoc then List.rev l else l) termin
       with Not_found -> 
           anomaly "Inconsistent substitution of recursive notation")
   | t ->
-      rawconstr_of_aconstr_with_binders loc (traverse_binder subst)
-      (subst_aconstr_in_rawconstr loc interp subst)
-      (renaming,(ids,None,scopes)) t
+      rawconstr_of_aconstr_with_binders loc (traverse_binder sub)
+      (subst_aconstr_in_rawconstr loc interp sub) subinfos t
 
-let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args =
-  let ntn,args = contract_notation ntn args in
-  let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
-    Dumpglob.dump_notation_location (Topconstr.ntn_loc loc args ntn) df;
-    let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
-      subst_aconstr_in_rawconstr loc intern subst ([],env) c
+let intern_notation intern (_,tmp_scope,scopes as env) loc ntn fullargs =
+  let ntn,(args,argslist as fullargs) = contract_notation ntn fullargs in
+  let (((ids,idsl),c),df) = interp_notation loc ntn (tmp_scope,scopes) in
+  Dumpglob.dump_notation_location (ntn_loc loc fullargs ntn) df;
+  let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
+  let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl argslist in
+  subst_aconstr_in_rawconstr loc intern (subst,substlist) ([],env) c
 
 let set_type_scope (ids,tmp_scope,scopes) =
   (ids,Some Notation.type_scope,scopes)
@@ -353,7 +349,7 @@ let intern_qualid loc qid intern env args =
       let args1,args2 = list_chop nids args in
       check_no_explicitation args1;
       let subst = List.map2 (fun (id,scl) a -> (id,(fst a,scl))) ids args1 in
-      subst_aconstr_in_rawconstr loc intern subst ([],env) c, args2
+      subst_aconstr_in_rawconstr loc intern (subst,[]) ([],env) c, args2
   with Not_found ->
     error_global_not_found_loc loc qid
 
@@ -460,8 +456,8 @@ let check_constructor_length env loc cstr pl pl0 =
 
   (* [merge_aliases] returns the sets of all aliases encountered at this
      point and a substitution mapping extra aliases to the first one *)
-let merge_aliases (ids,subst as _aliases) id =
-  ids@[id], if ids=[] then subst else (id, List.hd ids)::subst
+let merge_aliases (ids,asubst as _aliases) id =
+  ids@[id], if ids=[] then asubst else (id, List.hd ids)::asubst
 
 let alias_of = function
   | ([],_) -> Anonymous
@@ -483,10 +479,6 @@ let chop_aconstr_constructor loc (ind,k) args =
     | _ -> error_invalid_pattern_notation loc) params;
   args
 
-let decode_patlist_value = function
-  | CPatCstr (_,_,l) -> l
-  | _ -> anomaly "Ill-formed list argument of notation"
-
 let rec subst_pat_iterator y t (subst,p) = match p with
   | PatVar (_,id) as x ->
       if id = Name y then t else [subst,x]
@@ -495,8 +487,8 @@ let rec subst_pat_iterator y t (subst,p) = match p with
       let pl = simple_product_of_cases_patterns l' in
       List.map (fun (subst',pl) -> subst'@subst,PatCstr (loc,id,pl,alias)) pl
 
-let subst_cases_pattern loc alias intern subst scopes a =
-  let rec aux alias subst = function
+let subst_cases_pattern loc alias intern fullsubst scopes a =
+  let rec aux alias (subst,substlist as fullsubst) = function
   | AVar id ->
       begin
 	(* subst remembers the delimiters stack in the interpretation *)
@@ -518,30 +510,29 @@ let subst_cases_pattern loc alias intern subst scopes a =
       ([],[[], PatCstr (loc,c, [], alias)])
   | AApp (ARef (ConstructRef cstr),args) ->
       let args = chop_aconstr_constructor loc cstr args in
-      let idslpll = List.map (aux Anonymous subst) args in
+      let idslpll = List.map (aux Anonymous fullsubst) args in
       let ids',pll = product_of_cases_patterns [] idslpll in
-      let pl' = List.map (fun (subst,pl) -> 
-        subst,PatCstr (loc,cstr,pl,alias)) pll in
+      let pl' = List.map (fun (asubst,pl) -> 
+        asubst,PatCstr (loc,cstr,pl,alias)) pll in
 	ids', pl'
   | AList (x,_,iter,terminator,lassoc) ->
       (try 
         (* All elements of the list are in scopes (scopt,subscopes) *)
-	let (a,(scopt,subscopes)) = List.assoc x subst in
-        let termin = aux Anonymous subst terminator in
-        let l = decode_patlist_value a in
+	let (l,(scopt,subscopes)) = List.assoc x substlist in
+        let termin = aux Anonymous fullsubst terminator in
         let idsl,v =
 	  List.fold_right (fun a (tids,t) -> 
-            let uids,u = aux Anonymous ((x,(a,(scopt,subscopes)))::subst) iter in
+            let uids,u = aux Anonymous ((x,(a,(scopt,subscopes)))::subst,substlist) iter in
             let pll = List.map (subst_pat_iterator ldots_var t) u in
             tids@uids, List.flatten pll)
             (if lassoc then List.rev l else l) termin in
-        idsl, List.map (fun ((subst, pl) as x) -> 
-	  match pl with PatCstr (loc, c, pl, Anonymous) -> (subst, PatCstr (loc, c, pl, alias)) | _ -> x) v
+        idsl, List.map (fun ((asubst, pl) as x) ->
+	  match pl with PatCstr (loc, c, pl, Anonymous) -> (asubst, PatCstr (loc, c, pl, alias)) | _ -> x) v
       with Not_found -> 
           anomaly "Inconsistent substitution of recursive notation")
   | t -> error_invalid_pattern_notation loc
-  in aux alias subst a
-    
+  in aux alias fullsubst a
+
 (* Differentiating between constructors and matching variables *)
 type pattern_qualid_kind =
   | ConstrPat of constructor * (identifier list * 
@@ -566,7 +557,7 @@ let find_constructor ref f aliases pats scopes =
 	   if List.length pats < nvars then error_not_enough_arguments loc;
 	   let pats1,pats2 = list_chop nvars pats in
 	   let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in
-	   let idspl1 = List.map (subst_cases_pattern loc (alias_of aliases) f subst scopes) args in
+	   let idspl1 = List.map (subst_cases_pattern loc (alias_of aliases) f (subst,[]) scopes) args in
 	   cstr, idspl1, pats2
        | _ -> raise Not_found)
       
@@ -604,7 +595,7 @@ let mustbe_constructor loc ref f aliases patl scopes =
   with (Environ.NotEvaluableConst _ | Not_found) ->
     raise (InternalisationError (loc,NotAConstructor ref))
 
-let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
+let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
   let intern_pat = intern_cases_pattern genv in 
   match pat with
   | CPatAlias (loc, p, id) ->
@@ -616,28 +607,30 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
       let argscs2 = find_remaining_constructor_scopes idslpl1 pl2 c in
       let idslpl2 = List.map2 (intern_pat scopes ([],[])) argscs2 pl2 in
       let (ids',pll) = product_of_cases_patterns ids (idslpl1@idslpl2) in
-      let pl' = List.map (fun (subst,pl) ->
-        (subst, PatCstr (loc,c,pl,alias_of aliases))) pll in
+      let pl' = List.map (fun (asubst,pl) ->
+        (asubst, PatCstr (loc,c,pl,alias_of aliases))) pll in
       ids',pl'
-  | CPatNotation (loc,"- _",[CPatPrim(_,Numeral p)]) 
+  | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[])) 
       when Bigint.is_strictly_pos p ->
       intern_pat scopes aliases tmp_scope (CPatPrim(loc,Numeral(Bigint.neg p)))
-  | CPatNotation (_,"( _ )",[a]) ->
+  | CPatNotation (_,"( _ )",([a],[])) ->
       intern_pat scopes aliases tmp_scope a
-  | CPatNotation (loc, ntn, args) ->
-      let ntn,args = contract_pat_notation ntn args in
-      let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
-      Dumpglob.dump_notation_location (Topconstr.patntn_loc loc args ntn) df;
+  | CPatNotation (loc, ntn, fullargs) ->
+      let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in
+      let (((ids',idsl'),c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
+      Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) df;
       let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in
-      let ids'',pl = subst_cases_pattern loc (alias_of aliases) intern_pat subst scopes 
-	c
+      let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl' argsl in
+      let ids'',pl =
+	subst_cases_pattern loc (alias_of aliases) intern_pat (subst,substlist)
+	  scopes c
       in ids@ids'', pl
   | CPatPrim (loc, p) ->
       let a = alias_of aliases in
       let (c,df) = Notation.interp_prim_token_cases_pattern loc p a 
 	(tmp_scope,scopes) in
       Dumpglob.dump_notation_location (fst (unloc loc)) df;
-      (ids,[subst,c])
+      (ids,[asubst,c])
   | CPatDelimiters (loc, key, e) ->
       intern_pat (find_delimiters_scope loc key::scopes) aliases None e
   | CPatAtom (loc, Some head) ->
@@ -645,13 +638,13 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
 	 | ConstrPat (c,idspl) ->
 	     check_constructor_length genv loc c idspl [];
 	     let (ids',pll) = product_of_cases_patterns ids idspl in
-	     (ids,List.map (fun (subst,pl) ->
-	       (subst, PatCstr (loc,c,pl,alias_of aliases))) pll)
+	     (ids,List.map (fun (asubst,pl) ->
+	       (asubst, PatCstr (loc,c,pl,alias_of aliases))) pll)
 	 | VarPat id ->
-	     let ids,subst = merge_aliases aliases id in
-	     (ids,[subst, PatVar (loc,alias_of (ids,subst))]))
+	     let ids,asubst = merge_aliases aliases id in
+	     (ids,[asubst, PatVar (loc,alias_of (ids,asubst))]))
   | CPatAtom (loc, None) ->
-      (ids,[subst, PatVar (loc,alias_of aliases)])
+      (ids,[asubst, PatVar (loc,alias_of aliases)])
   | CPatOr (loc, pl) ->
       assert (pl <> []);
       let pl' = List.map (intern_pat scopes aliases tmp_scope) pl in
@@ -888,10 +881,10 @@ let internalise sigma globalenv env allow_patvar lvar c =
     | CLetIn (loc,(loc1,na),c1,c2) ->
 	RLetIn (loc, na, intern (reset_tmp_scope env) c1,
           intern (push_loc_name_env lvar env loc1 na) c2)
-    | CNotation (loc,"- _",[CPrim (_,Numeral p)])
+    | CNotation (loc,"- _",([CPrim (_,Numeral p)],[]))
 	when Bigint.is_strictly_pos p -> 
 	intern env (CPrim (loc,Numeral (Bigint.neg p)))
-    | CNotation (_,"( _ )",[a]) -> intern env a
+    | CNotation (_,"( _ )",([a],[])) -> intern env a
     | CNotation (loc,ntn,args) ->
         intern_notation intern env loc ntn args
     | CPrim (loc, p) ->
@@ -915,8 +908,8 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	let (c,impargs,args_scopes,l),args =
           match f with
             | CRef ref -> intern_applied_reference intern env lvar args ref
-            | CNotation (loc,ntn,[]) ->
-                let c = intern_notation intern env loc ntn [] in
+            | CNotation (loc,ntn,([],[])) ->
+                let c = intern_notation intern env loc ntn ([],[]) in
                 find_appl_head_data lvar c, args
             | x -> (intern env f,[],[],[]), args in
 	let args = 
@@ -992,9 +985,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
     (* Linearity implies the order in ids is irrelevant *)
     check_linearity lhs eqn_ids;
     let env_ids = List.fold_right Idset.add eqn_ids ids in
-    List.map (fun (subst,pl) ->
-      let rhs = replace_vars_constr_expr subst rhs in
-      List.iter message_redundant_alias subst;
+    List.map (fun (asubst,pl) ->
+      let rhs = replace_vars_constr_expr asubst rhs in
+      List.iter message_redundant_alias asubst;
       let rhs' = intern (env_ids,tmp_scope,scopes) rhs in
       (loc,eqn_ids,pl,rhs')) pll
 
@@ -1209,19 +1202,19 @@ type ltac_sign = identifier list * unbound_ltac_var_map
 let interp_constrpattern sigma env c =
   pattern_of_rawconstr (intern_gen false sigma env ~allow_patvar:true c)
 
-let interp_aconstr impls vars a =
+let interp_aconstr impls (vars,varslist) a =
   let env = Global.env () in
   (* [vl] is intended to remember the scope of the free variables of [a] *)
-  let vl = List.map (fun id -> (id,ref None)) vars in
+  let vl = List.map (fun id -> (id,ref None)) (vars@varslist) in
   let c = internalise Evd.empty (Global.env()) (extract_ids env, None, [])
     false (([],[]),Environ.named_context env,vl,([],impls)) a in
   (* Translate and check that [c] has all its free variables bound in [vars] *)
   let a = aconstr_of_rawconstr vars c in
   (* Returns [a] and the ordered list of variables with their scopes *)
   (* Variables occurring in binders have no relevant scope since bound *)
-  List.map
-    (fun (id,r) -> (id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl,
-  a
+  let vl = List.map (fun (id,r) -> 
+    (id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl in
+  list_chop (List.length vars) vl, a
 
 (* Interpret binders and contexts  *)
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 9169e5fbf..1554d4289 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -141,8 +141,8 @@ val global_reference_in_absolute_module : dir_path -> identifier -> constr
 
 (* Interprets into a abbreviatable constr *)
 
-val interp_aconstr : implicits_env -> identifier list -> constr_expr ->
-  interpretation
+val interp_aconstr : implicits_env -> identifier list * identifier list 
+  -> constr_expr -> interpretation
 
 (* Globalization leak for Grammar *)
 val for_grammar : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 8bacbcd8c..7801f048f 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -58,7 +58,7 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
   in
   let rec aux bdvars l c = match c with
     | CRef (Ident (_,id)) -> found id bdvars l
-    | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id))) :: _) when not (Idset.mem id bdvars) ->
+    | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [])) when not (Idset.mem id bdvars) ->
 	fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
     | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
   in aux bound l c
diff --git a/interp/notation.ml b/interp/notation.ml
index 0915304c3..b6c1bfa40 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -193,10 +193,6 @@ let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
   | ARef ref -> RefKey ref, None
   | _ -> Oth, None
 
-let pattern_key = function
-  | PatCstr (_,cstr,_,_) -> RefKey (ConstructRef cstr)
-  | _ -> Oth
-
 (**********************************************************************)
 (* Interpreting numbers (not in summary because functional objects)   *)
 
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 4c2b7eaef..8f303ea61 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -70,11 +70,18 @@ let (in_syntax_constant, out_syntax_constant) =
     classify_function = classify_syntax_constant;
     export_function = export_syntax_constant } 
 
+type syndef_interpretation = (identifier * subscopes) list * aconstr
+
+(* Coercions to the general format of notation that also supports
+   variables bound to list of expressions *)
+let in_pat (ids,ac) = ((ids,[]),ac)
+let out_pat ((ids,idsl),ac) = assert (idsl=[]); (ids,ac)
+
 let declare_syntactic_definition local id onlyparse pat =
-  let _ = add_leaf id (in_syntax_constant (local,pat,onlyparse)) in ()
+  let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()
 
 let search_syntactic_definition loc kn =
-  KNmap.find kn !syntax_table
+  out_pat (KNmap.find kn !syntax_table)
 
 let locate_global_with_alias (loc,qid) =
   match Nametab.extended_locate qid with
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index bbbea07f3..1599e844b 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -18,10 +18,12 @@ open Libnames
 
 (* Syntactic definitions. *)
 
-val declare_syntactic_definition : bool -> identifier -> bool -> interpretation
-  -> unit
+type syndef_interpretation = (identifier * subscopes) list * aconstr
 
-val search_syntactic_definition : loc -> kernel_name -> interpretation
+val declare_syntactic_definition : bool -> identifier -> bool -> 
+  syndef_interpretation -> unit
+
+val search_syntactic_definition : loc -> kernel_name -> syndef_interpretation
 
 (* [locate_global_with_alias] locates global reference possibly following
    a notation if this notation has a role of aliasing; raise Not_found
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index c684c6adb..058d997e0 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -389,8 +389,9 @@ let rec subst_aconstr subst bound raw =
 	      if r1' == r1 then raw else
 		ACast (r1',CastCoerce)
 		  
-let subst_interpretation subst (metas,pat) = 
-  (metas,subst_aconstr subst (List.map fst metas) pat)
+let subst_interpretation subst (metas,pat) =
+  let bound = List.map fst (fst metas @ snd metas) in
+  (metas,subst_aconstr subst bound pat)
 
 let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
 
@@ -427,16 +428,16 @@ let rec alpha_var id1 id2 = function
 
 let alpha_eq_val (x,y) = x = y
 
-let bind_env alp sigma var v =
+let bind_env alp (sigma,sigmalist as fullsigma) var v =
   try
     let vvar = List.assoc var sigma in
-    if alpha_eq_val (v,vvar) then sigma
+    if alpha_eq_val (v,vvar) then fullsigma
     else raise No_match
   with Not_found ->
     (* Check that no capture of binding variables occur *)
     if List.exists (fun (id,_) ->occur_rawconstr id v) alp then raise No_match;
     (* TODO: handle the case of multiple occs in different scopes *)
-    (var,v)::sigma
+    ((var,v)::sigma,sigmalist)
 
 let match_fix_kind fk1 fk2 =
   match (fk1,fk2) with
@@ -467,6 +468,10 @@ let rec match_cases_pattern metas acc pat1 pat2 =
 	(match_names metas acc na1 na2) patl1 patl2
   | _ -> raise No_match
 
+let adjust_application_n n loc f l =
+  let l1,l2 = list_chop (List.length l - n) l in
+  if l1 = [] then f,l else RApp (loc,f,l1), l2
+
 let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
   | r1, AVar id2 when List.mem id2 metas -> bind_env alp sigma id2 r1
   | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
@@ -481,8 +486,9 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
 	  let l11,l12 = list_chop (n1-n2) l1 in RApp (loc,f1,l11),l12, f2,l2
 	else f1,l1, f2, l2 in
       List.fold_left2 (match_ alp metas) (match_ alp metas sigma f1 f2) l1 l2
-  | RApp (_,f1,l1), AList (x,_,(AApp (f2,l2) as iter),termin,lassoc) 
-      when List.length l1 = List.length l2 ->
+  | RApp (loc,f1,l1), AList (x,_,(AApp (f2,l2) as iter),termin,lassoc) 
+      when List.length l1 >= List.length l2 ->
+      let f1,l1 = adjust_application_n (List.length l2) loc f1 l1 in
       match_alist alp metas sigma (f1::l1) (f2::l2) x iter termin lassoc
   | RLambda (_,na1,_,t1,b1), ALambda (na2,t2,b2) ->
      match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
@@ -535,24 +541,26 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
 
 and match_alist alp metas sigma l1 l2 x iter termin lassoc =
   (* match the iterator at least once *)
-  let sigma = List.fold_left2 (match_ alp (ldots_var::metas)) sigma l1 l2 in
+  let sigmavar,sigmalist =
+    List.fold_left2 (match_ alp (ldots_var::metas)) sigma l1 l2 in
   (* Recover the recursive position *)
-  let rest = List.assoc ldots_var sigma in
+  let rest = List.assoc ldots_var sigmavar in
   (* Recover the first element *)
-  let t1 = List.assoc x sigma in
-  let sigma = List.remove_assoc x (List.remove_assoc ldots_var sigma) in
+  let t1 = List.assoc x sigmavar in
+  let sigmavar = List.remove_assoc x (List.remove_assoc ldots_var sigmavar) 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 (ldots_var::metas) sigma rest iter in
-      let rest = List.assoc ldots_var sigma in
-      let t = List.assoc x sigma in
-      let sigma = List.remove_assoc x (List.remove_assoc ldots_var sigma) in
-      match_alist_tail alp metas sigma (t::acc) rest
+      let sigmavar,sigmalist = match_ alp (ldots_var::metas) sigma rest iter in
+      let rest = List.assoc ldots_var sigmavar in
+      let t = List.assoc x sigmavar in
+      let sigmavar =
+	List.remove_assoc x (List.remove_assoc ldots_var sigmavar) in
+      match_alist_tail alp metas (sigmavar,sigmalist) (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 (if lassoc then List.rev tl else tl))::sigma
+      List.rev acc, match_ alp metas (sigmavar,sigmalist) rest termin in
+  let tl,(sigmavar,sigmalist) = match_alist_tail alp metas sigma [t1] rest in
+  (sigmavar, (x,if lassoc then List.rev tl else tl)::sigmalist)
 
 and match_binders alp metas na1 na2 sigma b1 b2 =
   let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in
@@ -569,19 +577,24 @@ type scope_name = string
 
 type tmp_scope_name = scope_name
 
-type interpretation = 
-    (identifier * (tmp_scope_name option * scope_name list)) list * aconstr
+type subscopes = tmp_scope_name option * scope_name list
+
+type interpretation =
+    (* regular vars of notation    / recursive parts of notation    / body *)
+    ((identifier * subscopes) list * (identifier * subscopes) list) * aconstr
 
-let match_aconstr c (metas_scl,pat) =
-  let subst = match_ [] (List.map fst metas_scl) [] c pat in
+let match_aconstr c ((metas_scl,metaslist_scl),pat) =
+  let vars = List.map fst metas_scl @ List.map fst metaslist_scl in
+  let subst,substlist = match_ [] vars ([],[]) c pat in
   (* Reorder canonically the substitution *)
-  let find x subst =
+  let find x =
     try List.assoc x subst
     with Not_found ->
       (* Happens for binders bound to Anonymous *)
       (* Find a better way to propagate Anonymous... *)
       RVar (dummy_loc,x) in
-  List.map (fun (x,scl) -> (find x subst,scl)) metas_scl
+  List.map (fun (x,scl) -> (find x,scl)) metas_scl,
+  List.map (fun (x,scl) -> (List.assoc x substlist,scl)) metaslist_scl
 
 (**********************************************************************)
 (*s Concrete syntax for terms *)
@@ -596,12 +609,15 @@ type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
 
 type prim_token = Numeral of Bigint.bigint | String of string
 
+type 'a notation_substitution =
+    'a list * (* for recursive notations: *) 'a list list
+
 type cases_pattern_expr =
   | CPatAlias of loc * cases_pattern_expr * identifier
   | CPatCstr of loc * reference * cases_pattern_expr list
   | CPatAtom of loc * reference option
   | CPatOr of loc * cases_pattern_expr list
-  | CPatNotation of loc * notation * cases_pattern_expr list
+  | CPatNotation of loc * notation * cases_pattern_expr notation_substitution
   | CPatPrim of loc * prim_token
   | CPatDelimiters of loc * string * cases_pattern_expr
 
@@ -628,7 +644,7 @@ type constr_expr =
   | CEvar of loc * existential_key * constr_expr list option
   | CSort of loc * rawsort
   | CCast of loc * constr_expr * constr_expr cast_type
-  | CNotation of loc * notation * constr_expr list
+  | CNotation of loc * notation * constr_expr notation_substitution
   | CPrim of loc * prim_token
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
@@ -718,7 +734,7 @@ let ids_of_cases_indtype =
   let rec vars_of = function
     (* We deal only with the regular cases *)
     | CApp (_,_,l) -> List.fold_left add_var [] (List.map fst l)
-    | CNotation (_,_,l)
+    | CNotation (_,_,(l,[])) 
     (* assume the ntn is applicative and does not instantiate the head !! *)
     | CAppExpl (_,_,l) -> List.fold_left add_var [] l
     | CDelimiters(_,_,c) -> vars_of c
@@ -738,8 +754,10 @@ let is_constructor id =
  
 let rec cases_pattern_fold_names f a = function
   | CPatAlias (_,pat,id) -> f id a
-  | CPatCstr (_,_,patl) | CPatOr (_,patl) | CPatNotation (_,_,patl) ->
+  | CPatCstr (_,_,patl) | CPatOr (_,patl) ->
       List.fold_left (cases_pattern_fold_names f) a patl
+  | CPatNotation (_,_,(patl,patll)) ->
+      List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)
   | CPatDelimiters (_,_,pat) -> cases_pattern_fold_names f a pat
   | CPatAtom (_,Some (Ident (_,id))) when not (is_constructor id) -> f id a
   | CPatPrim _ | CPatAtom _ -> a
@@ -776,7 +794,7 @@ let fold_constr_expr_with_binders g f n acc = function
   | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],default_binder_kind,a]
   | CCast (loc,a,CastConv(_,b)) -> f n (f n acc a) b
   | CCast (loc,a,CastCoerce) -> f n acc a
-  | CNotation (_,_,l) -> List.fold_left (f n) acc l
+  | CNotation (_,_,(l,ll)) -> List.fold_left (f n) acc (l@List.flatten ll)
   | CDelimiters (loc,_,a) -> f n acc a
   | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _  | CRef _ ->
       acc
@@ -887,7 +905,8 @@ let map_constr_expr_with_binders g f e = function
   | CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b)
   | CCast (loc,a,CastConv (k,b)) -> CCast (loc,f e a,CastConv(k, f e b))
   | CCast (loc,a,CastCoerce) -> CCast (loc,f e a,CastCoerce)
-  | CNotation (loc,n,l) -> CNotation (loc,n,List.map (f e) l)
+  | CNotation (loc,n,(l,ll)) ->
+      CNotation (loc,n,(List.map (f e) l,List.map (List.map (f e)) ll))
   | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
   | CHole _ | CEvar _ | CPatVar _ | CSort _ 
   | CPrim _ | CDynamic _ | CRef _ as x -> x
@@ -948,7 +967,7 @@ type include_ast =
   | CIMTE of module_type_ast
   | CIME of module_ast
 
-let loc_of_notation f loc args ntn =
+let loc_of_notation f loc (args,_) ntn =
   if args=[] or ntn.[0] <> '_' then fst (Util.unloc loc)
   else snd (Util.unloc (f (List.hd args)))
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index aed67975d..eb166bc25 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -77,11 +77,14 @@ type scope_name = string
 
 type tmp_scope_name = scope_name
 
-type interpretation = 
-    (identifier * (tmp_scope_name option * scope_name list)) list * aconstr
+type subscopes = tmp_scope_name option * scope_name list
+
+type interpretation =
+    (* regular vars of notation    / recursive parts of notation    / body *)
+    ((identifier * subscopes) list * (identifier * subscopes) list) * aconstr
 
 val match_aconstr : rawconstr -> interpretation ->
-      (rawconstr * (tmp_scope_name option * scope_name list)) list
+      (rawconstr * subscopes) list * (rawconstr list * subscopes) list
 
 (**********************************************************************)
 (* Substitution of kernel names in interpretation data                *)
@@ -101,12 +104,15 @@ type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
 
 type prim_token = Numeral of Bigint.bigint | String of string
 
+type 'a notation_substitution =
+    'a list * (* for recursive notations: *) 'a list list
+
 type cases_pattern_expr =
   | CPatAlias of loc * cases_pattern_expr * identifier
   | CPatCstr of loc * reference * cases_pattern_expr list
   | CPatAtom of loc * reference option
   | CPatOr of loc * cases_pattern_expr list
-  | CPatNotation of loc * notation * cases_pattern_expr list
+  | CPatNotation of loc * notation * cases_pattern_expr notation_substitution
   | CPatPrim of loc * prim_token
   | CPatDelimiters of loc * string * cases_pattern_expr
 
@@ -133,7 +139,7 @@ type constr_expr =
   | CEvar of loc * existential_key * constr_expr list option
   | CSort of loc * rawsort
   | CCast of loc * constr_expr * constr_expr cast_type
-  | CNotation of loc * notation * constr_expr list
+  | CNotation of loc * notation * constr_expr notation_substitution
   | CPrim of loc * prim_token
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
@@ -240,5 +246,5 @@ type include_ast =
   | CIMTE of module_type_ast
   | CIME of module_ast
 
-val ntn_loc : Util.loc -> constr_expr list -> string -> int
-val patntn_loc : Util.loc -> cases_pattern_expr list -> string -> int
+val ntn_loc : Util.loc -> constr_expr notation_substitution -> string -> int
+val patntn_loc : Util.loc -> cases_pattern_expr notation_substitution -> string -> int