Imported Upstream version 8.1~gammaupstream/8.1.gamma

7 files changed, 389 insertions, 214 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 570d113d..ffedcfff 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrextern.ml 8997 2006-07-03 16:40:20Z herbelin $ *)
+(* $Id: constrextern.ml 9226 2006-10-09 16:11:01Z herbelin $ *)
 
 (*i*)
 open Pp
@@ -295,9 +295,6 @@ let same_rawconstr c d =
 (**********************************************************************)
 (* mapping patterns to cases_pattern_expr                                *)
 
-let make_current_scopes (scopt,scopes) = 
-  option_fold_right push_scope scopt scopes
-
 let has_curly_brackets ntn =
   String.length ntn >= 6 & (String.sub ntn 0 6 = "{ _ } " or
     String.sub ntn (String.length ntn - 6) 6 = " { _ }" or
@@ -401,14 +398,14 @@ let match_aconstr_cases_pattern c (metas_scl,pat) =
   List.map (fun (x,scl) -> (find x subst,scl)) metas_scl
 
  (* Better to use extern_rawconstr composed with injection/retraction ?? *)
-let rec extern_cases_pattern_in_scope scopes vars pat =
+let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
   try 
     if !Options.raw_print or !print_no_symbol then raise No_match;
     let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
-    match availability_of_prim_token sc (make_current_scopes scopes) with
+    match availability_of_prim_token sc scopes with
     | None -> raise No_match
     | Some key ->
-      let loc = pattern_loc pat in
+      let loc = cases_pattern_loc pat in
       insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na
   with No_match ->
   try 
@@ -440,17 +437,15 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
 	(* Try availability of interpretation ... *)
         match keyrule with
           | NotationRule (sc,ntn) ->
-	      let scopes' = make_current_scopes (tmp_scope, scopes) in
-	      (match availability_of_notation (sc,ntn) scopes' with
+	      (match availability_of_notation (sc,ntn) allscopes with
                   (* Uninterpretation is not allowed in current context *)
               | None -> raise No_match
                   (* Uninterpretation is allowed in current context *)
 	      | Some (scopt,key) ->
-	          let scopes = make_current_scopes (scopt, scopes) in
+	          let scopes' = option_cons scopt scopes in
 	          let l =
 		    List.map (fun (c,(scopt,scl)) ->
-		      extern_cases_pattern_in_scope 
-		        (scopt,List.fold_right push_scope scl scopes) vars c)
+		      extern_cases_pattern_in_scope (scopt,scl@scopes') vars c)
                       subst in
 		  insert_pat_delimiters loc (make_pat_notation loc ntn l) key)
           | SynDefRule kn ->
@@ -460,7 +455,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
 	  No_match -> extern_symbol_pattern allscopes vars t rules
 
 let extern_cases_pattern vars p = 
-  extern_cases_pattern_in_scope (None,Notation.current_scopes()) vars p
+  extern_cases_pattern_in_scope (None,[]) vars p
 
 (**********************************************************************)
 (* Externalising applications *)
@@ -607,7 +602,7 @@ let rec share_fix_binders n rbl ty def =
 let extern_possible_prim_token scopes r =
   try
     let (sc,n) = uninterp_prim_token r in
-    match availability_of_prim_token sc (make_current_scopes scopes) with
+    match availability_of_prim_token sc scopes with
     | None -> None
     | Some key -> Some (insert_delimiters (CPrim (loc_of_rawconstr r,n)) key)
   with No_match ->
@@ -754,11 +749,16 @@ let rec extern inctx scopes vars r =
 
   | RDynamic (loc,d) -> CDynamic (loc,d)
 
-and extern_typ (_,scopes) = extern true (Some Notation.type_scope,scopes)
+and extern_typ (_,scopes) = 
+  extern true (Some Notation.type_scope,scopes)
 
 and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
 
-and factorize_prod scopes vars aty = function
+and factorize_prod scopes vars aty c =
+  try 
+    if !Options.raw_print or !print_no_symbol then raise No_match;
+    ([],extern_symbol scopes vars c (uninterp_notations c))
+  with No_match -> match c with
   | RProd (loc,(Name id as na),ty,c)
       when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
 	& not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *)
@@ -766,7 +766,11 @@ and factorize_prod scopes vars aty = function
            ((loc,Name id)::nal,c)
   | c -> ([],extern_typ scopes vars c)
 
-and factorize_lambda inctx scopes vars aty = function
+and factorize_lambda inctx scopes vars aty c =
+  try 
+    if !Options.raw_print or !print_no_symbol then raise No_match;
+    ([],extern_symbol scopes vars c (uninterp_notations c))
+  with No_match -> match c with
   | RLambda (loc,na,ty,c)
       when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
 	& not (occur_name na aty) (* To avoid na in ty' escapes scope *)
@@ -817,17 +821,16 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
         let e =
           match keyrule with
           | NotationRule (sc,ntn) ->
-	      let scopes' = make_current_scopes (tmp_scope, scopes) in
-	      (match availability_of_notation (sc,ntn) scopes' with
+	      (match availability_of_notation (sc,ntn) allscopes with
                   (* Uninterpretation is not allowed in current context *)
               | None -> raise No_match
                   (* Uninterpretation is allowed in current context *)
 	      | Some (scopt,key) ->
-	          let scopes = make_current_scopes (scopt, scopes) in
+	          let scopes' = option_cons scopt scopes in
 	          let l =
 		    List.map (fun (c,(scopt,scl)) ->
 		      extern (* assuming no overloading: *) true
-		        (scopt,List.fold_right push_scope scl scopes) vars c)
+		        (scopt,scl@scopes') vars c)
                       subst in
 	          insert_delimiters (make_notation loc ntn l) key)
           | SynDefRule kn ->
@@ -847,10 +850,10 @@ and extern_recursion_order scopes vars = function
 
 
 let extern_rawconstr vars c =
-  extern false (None,Notation.current_scopes()) vars c
+  extern false (None,[]) vars c
 
 let extern_rawtype vars c =
-  extern_typ (None,Notation.current_scopes()) vars c
+  extern_typ (None,[]) vars c
 
 (******************************************************************)
 (* Main translation function from constr -> constr_expr *)
@@ -861,7 +864,7 @@ let extern_constr_gen at_top scopt env t =
   let avoid = if at_top then ids_of_context env else [] in
   let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
   let vars = vars_of_env env in
-  extern (not at_top) (scopt,Notation.current_scopes()) vars r
+  extern (not at_top) (scopt,[]) vars r
 
 let extern_constr_in_scope at_top scope env t =
   extern_constr_gen at_top (Some scope) env t
@@ -962,5 +965,4 @@ and raw_of_eqn env constr construct_nargs branch =
   buildrec [] [] env construct_nargs branch
 
 let extern_constr_pattern env pat =
-  extern true (None,Notation.current_scopes()) Idset.empty
-    (raw_of_pat env pat)
+  extern true (None,[]) Idset.empty (raw_of_pat env pat)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 355bac1d..d09430dc 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrintern.ml 8997 2006-07-03 16:40:20Z herbelin $ *)
+(* $Id: constrintern.ml 9226 2006-10-09 16:11:01Z herbelin $ *)
 
 open Pp
 open Util
@@ -118,6 +118,11 @@ let error_bad_inductive_type loc =
   user_err_loc (loc,"",str 
     "This should be an inductive type applied to names or \"_\"")
 
+let error_inductive_parameter_not_implicit loc =
+  user_err_loc (loc,"", str
+   ("The parameters of inductive types do not bind in\n"^
+    "the 'return' clauses; they must be replaced by '_' in the 'in' clauses."))
+
 (**********************************************************************)
 (* Dump of globalization (to be used by coqdoc)                       *)
 let token_number = ref 0
@@ -151,7 +156,7 @@ let loc_of_notation f loc args ntn =
   else snd (unloc (f (List.hd args)))
 
 let ntn_loc = loc_of_notation constr_loc
-let patntn_loc = loc_of_notation cases_pattern_loc
+let patntn_loc = loc_of_notation cases_pattern_expr_loc
 
 let dump_notation_location pos ((path,df),sc) =
   let rec next growing =
@@ -216,7 +221,7 @@ let contract_pat_notation ntn l =
 (**********************************************************************)
 (* Remembering the parsing scope of variables in notations            *)
 
-let make_current_scope (scopt,scopes) = option_cons scopt scopes
+let make_current_scope (tmp_scope,scopes) = option_cons tmp_scope scopes
 
 let set_var_scope loc id (_,scopt,scopes) varscopes =
   let idscopes = List.assoc id varscopes in
@@ -356,8 +361,8 @@ let rec has_duplicate = function
   | x::l -> if List.mem x l then (Some x) else has_duplicate l
 
 let loc_of_lhs lhs = 
- join_loc (cases_pattern_loc (List.hd (List.hd lhs)))
-          (cases_pattern_loc (list_last (list_last lhs)))
+ join_loc (cases_pattern_expr_loc (List.hd (List.hd lhs)))
+          (cases_pattern_expr_loc (list_last (list_last lhs)))
 
 let check_linearity lhs ids =
   match has_duplicate ids with
@@ -553,16 +558,15 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope =
       intern_cases_pattern genv scopes aliases tmp_scope a
   | CPatNotation (loc, ntn, args) ->
       let ntn,args = contract_pat_notation ntn args in
-      let scopes = option_cons tmp_scope scopes in
-      let ((ids,c),df) = Notation.interp_notation loc ntn scopes in
+      let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
       if !dump then dump_notation_location (patntn_loc loc args ntn) df;
       let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
       subst_cases_pattern loc aliases (intern_cases_pattern genv) subst scopes 
 	c
   | CPatPrim (loc, p) ->
-      let scopes = option_cons tmp_scope scopes in
       let a = alias_of aliases in
-      let (c,df) = Notation.interp_prim_token_cases_pattern loc p a scopes in
+      let (c,df) = Notation.interp_prim_token_cases_pattern loc p a 
+	(tmp_scope,scopes) in
       if !dump then dump_notation_location (fst (unloc loc)) df;
       (ids,[subst,c])
   | CPatDelimiters (loc, key, e) ->
@@ -689,15 +693,20 @@ let extract_explicit_arg imps args =
 (**********************************************************************)
 (* Syntax extensions                                                  *)
 
-let traverse_binder subst id (ids,tmpsc,scopes as env) =
+let traverse_binder subst (renaming,(ids,tmpsc,scopes as env)) id =
   try
-    (* Binders bound in the notation are consider first-order object *)
-    (* and binders not bound in the notation do not capture variables *)
-    (* outside the notation *)
+    (* Binders bound in the notation are considered first-order objects *)
     let _,id' = coerce_to_id (fst (List.assoc id subst)) in
-    id', (Idset.add id' ids,tmpsc,scopes)
+    (renaming,(Idset.add id' ids,tmpsc,scopes)), id'
   with Not_found ->
-    id, env
+    (* 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 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
@@ -707,7 +716,7 @@ 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) =
+let rec subst_aconstr_in_rawconstr loc interp subst (renaming,(ids,_,scopes)) =
   function
   | AVar id ->
       begin
@@ -717,6 +726,9 @@ let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as _env) =
 	  let (a,(scopt,subscopes)) = List.assoc id subst in
 	  interp (ids,scopt,subscopes@scopes) a
 	with Not_found -> 
+	try 
+	  RVar (loc,List.assoc id renaming)
+	with Not_found -> 
 	  (* Happens for local notation joint with inductive/fixpoint defs *)
 	  RVar (loc,id)
       end
@@ -725,28 +737,28 @@ let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as _env) =
         (* 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
+          subst_aconstr_in_rawconstr loc interp subst 
+	    (renaming,(ids,None,scopes)) terminator in
         let l = decode_constrlist_value a in
 	List.fold_right (fun a t -> 
           subst_iterator ldots_var t
             (subst_aconstr_in_rawconstr loc interp 
               ((x,(a,(scopt,subscopes)))::subst)
-              (ids,None,scopes) iter))
+	      (renaming,(ids,None,scopes)) 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) (ids,None,scopes) t
+      (subst_aconstr_in_rawconstr loc interp subst)
+      (renaming,(ids,None,scopes)) t
 
 let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args =
   let ntn,args = contract_notation ntn args in
-  let scopes = option_cons tmp_scope scopes in
-  let ((ids,c),df) = Notation.interp_notation loc ntn scopes in
+  let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
   if !dump then dump_notation_location (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
+  subst_aconstr_in_rawconstr loc intern subst ([],env) c
 
 let set_type_scope (ids,tmp_scope,scopes) =
   (ids,Some Notation.type_scope,scopes)
@@ -844,8 +856,7 @@ let internalise sigma globalenv env allow_soapp lvar c =
     | CNotation (loc,ntn,args) ->
         intern_notation intern env loc ntn args
     | CPrim (loc, p) ->
-	let scopes = option_cons tmp_scope scopes in
-	let c,df = Notation.interp_prim_token loc p scopes in
+	let c,df = Notation.interp_prim_token loc p (tmp_scope,scopes) in
 	if !dump then dump_notation_location (fst (unloc loc)) df;
 	c
     | CDelimiters (loc, key, e) ->
@@ -913,8 +924,7 @@ let internalise sigma globalenv env allow_soapp lvar c =
 
     | CDynamic (loc,d) -> RDynamic (loc,d)
 
-  and intern_type (ids,_,scopes) =
-    intern (ids,Some Notation.type_scope,scopes)
+  and intern_type env = intern (set_type_scope env)
 
   and intern_local_binder ((ids,ts,sc as env),bl) = function
     | LocalRawAssum(nal,ty) ->
@@ -961,29 +971,25 @@ let internalise sigma globalenv env allow_soapp lvar c =
     let tm' = intern env tm in
     let ids,typ = match t with
     | Some t -> 
-	let tids = names_of_cases_indtype t in
+	let tids = ids_of_cases_indtype t in
 	let tids = List.fold_right Idset.add tids Idset.empty in
 	let t = intern_type (tids,None,scopes) t in
-	let (_,_,_,nal as indsign) =
-	  match t with
-	  | RRef (loc,IndRef ind) -> (loc,ind,0,[])
-	  | RApp (loc,RRef (_,IndRef ind),l) ->
-	      let nparams, nrealargs = inductive_nargs globalenv ind in
-	      let nindargs = nparams + nrealargs in
-	      if List.length l <> nindargs then
-		error_wrong_numarg_inductive_loc loc globalenv ind nindargs;
-	      let nal = List.map (function
-		| RHole _ -> Anonymous
-		| RVar (_,id) -> Name id
-		| c ->
-		    user_err_loc (loc_of_rawconstr c,"",str "Not a name")) l in
-	      let parnal,realnal = list_chop nparams nal in
-	      if List.exists ((<>) Anonymous) parnal then
-		user_err_loc (loc,"",
-		  str "The parameters of inductive type must be implicit");
-	      (loc,ind,nparams,realnal)
-	  | _ -> error_bad_inductive_type (loc_of_rawconstr t) in
-	nal, Some indsign
+	let loc,ind,l = match t with
+	    | RRef (loc,IndRef ind) -> (loc,ind,[])
+	    | RApp (loc,RRef (_,IndRef ind),l) -> (loc,ind,l)
+	    | _ -> error_bad_inductive_type (loc_of_rawconstr t) in
+	let nparams, nrealargs = inductive_nargs globalenv ind in
+	let nindargs = nparams + nrealargs in
+	if List.length l <> nindargs then
+	  error_wrong_numarg_inductive_loc loc globalenv ind nindargs;
+	let nal = List.map (function
+	  | RHole loc -> Anonymous
+	  | RVar (_,id) -> Name id
+	  | c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name")) l in
+	let parnal,realnal = list_chop nparams nal in
+	if List.exists ((<>) Anonymous) parnal then
+	  error_inductive_parameter_not_implicit loc;
+	realnal, Some (loc,ind,nparams,realnal)
     | None -> 
 	[], None in
     let na = match tm', na with
@@ -1067,12 +1073,21 @@ let extract_ids env =
 let intern_gen isarity sigma env
                ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
                c =
-  let tmp_scope = if isarity then Some Notation.type_scope else None in
+  let tmp_scope = 
+    if isarity then Some Notation.type_scope else None in
   internalise sigma env (extract_ids env, tmp_scope,[])
     allow_soapp (ltacvars,Environ.named_context env, [], impls) c
 
 let intern_constr sigma env c = intern_gen false sigma env c 
 
+let intern_pattern env patt =
+  try
+    intern_cases_pattern env [] ([],[]) None patt 
+  with 
+      InternalisationError (loc,e) ->
+	user_err_loc (loc,"internalize",explain_internalisation_error e)
+
+
 let intern_ltac isarity ltacvars sigma env c =
   intern_gen isarity sigma env ~ltacvars:ltacvars c
 
@@ -1100,6 +1115,21 @@ let interp_open_constr sigma env c =
 let interp_constr_judgment sigma env c =
   Default.understand_judgment sigma env (intern_constr sigma env c)
 
+
+let interp_constr_evars_gen isevars env ?(impls=([],[])) kind c =
+  Default.understand_tcc_evars isevars env kind
+    (intern_gen (kind=IsType) ~impls (Evd.evars_of !isevars) env c)
+
+let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ =
+  interp_constr_evars_gen isevars env ~impls (OfType (Some typ)) c
+
+let interp_type_evars isevars env ?(impls=([],[])) c =
+  interp_constr_evars_gen isevars env IsType ~impls c
+
+let interp_constr_judgment_evars isevars env c =
+  Default.understand_judgment_tcc isevars env
+    (intern_constr (Evd.evars_of !isevars) env c)
+
 type ltac_sign = identifier list * unbound_ltac_var_map
 
 let interp_constrpattern sigma env c =
@@ -1123,7 +1153,13 @@ let interp_aconstr impls vars a =
 
 let interp_binder sigma env na t =
   let t = intern_gen true sigma env t in
-  Default.understand_type sigma env (locate_if_isevar (loc_of_rawconstr t) na t)
+  let t' = locate_if_isevar (loc_of_rawconstr t) na t in
+  Default.understand_type sigma env t'
+
+let interp_binder_evars isevars env na t =
+  let t = intern_gen true (Evd.evars_of !isevars) env t in
+  let t' = locate_if_isevar (loc_of_rawconstr t) na t in
+  Default.understand_tcc_evars isevars env IsType t'
 
 open Environ
 open Term
@@ -1146,6 +1182,24 @@ let interp_context sigma env params =
 	  (push_rel d env,d::params))
     (env,[]) params
 
+let interp_context_evars isevars env params =
+  List.fold_left
+    (fun (env,params) d -> match d with
+      | LocalRawAssum ([_,na],(CHole _ as t)) ->
+	  let t = interp_binder_evars isevars env na t in
+	  let d = (na,None,t) in
+	  (push_rel d env, d::params)
+      | LocalRawAssum (nal,t) ->
+	  let t = interp_type_evars isevars env t in
+	  let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
+	  let ctx = List.rev ctx in
+	  (push_rel_context ctx env, ctx@params)
+      | LocalRawDef ((_,na),c) ->
+	  let c = interp_constr_judgment_evars isevars env c in
+	  let d = (na, Some c.uj_val, c.uj_type) in
+	  (push_rel d env,d::params))
+    (env,[]) params
+
 (**********************************************************************)
 (* Locating reference, possibly via an abbreviation *)
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index cdd87a7c..d88a058d 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: constrintern.mli 7732 2005-12-26 13:51:24Z herbelin $ i*)
+(*i $Id: constrintern.mli 9154 2006-09-20 17:18:18Z corbinea $ i*)
 
 (*i*)
 open Names
@@ -55,6 +55,14 @@ val intern_gen : bool -> evar_map -> env ->
   ?impls:full_implicits_env -> ?allow_soapp:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> rawconstr
 
+val intern_pattern : env -> cases_pattern_expr ->
+  Names.identifier list *
+    ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list
+
+val intern_pattern : env -> cases_pattern_expr ->
+  Names.identifier list *
+    ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list
+
 (*s Composing internalisation with pretyping *)
 
 (* Main interpretation function *)
@@ -76,6 +84,12 @@ val interp_type : evar_map -> env -> ?impls:full_implicits_env ->
 
 val interp_open_constr   : evar_map -> env -> constr_expr -> evar_map * constr
 
+val interp_casted_constr_evars : evar_defs ref -> env -> 
+  ?impls:full_implicits_env -> constr_expr -> types -> constr
+
+val interp_type_evars : evar_defs ref -> env -> ?impls:full_implicits_env ->
+  constr_expr -> types
+
 (*s Build a judgment  *)
 
 val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment
@@ -95,6 +109,9 @@ val interp_binder  : evar_map -> env -> name -> constr_expr -> types
 
 val interp_context : evar_map -> env -> local_binder list -> env * rel_context
 
+val interp_context_evars : 
+  evar_defs ref -> env -> local_binder list -> env * rel_context
+
 (* Locating references of constructions, possibly via a syntactic definition *)
 
 val locate_reference : qualid -> global_reference
diff --git a/interp/notation.ml b/interp/notation.ml
index 7e101784..5b6692e9 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: notation.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
+(* $Id: notation.ml 9258 2006-10-23 07:15:04Z courtieu $ *)
 
 (*i*)
 open Util
@@ -130,6 +130,11 @@ let push_scope sc scopes = Scope sc :: scopes
 
 let push_scopes = List.fold_right push_scope
 
+type local_scopes = tmp_scope_name option * scope_name list
+
+let make_current_scopes (tmp_scope,scopes) =
+  option_fold_right push_scope tmp_scope (push_scopes scopes !scope_stack)
+
 (**********************************************************************)
 (* Delimiters *)
 
@@ -146,7 +151,7 @@ let declare_delimiters scope key =
   scope_map := Gmap.add scope sc !scope_map;
   if Gmap.mem key !delimiters_map then begin
     let oldsc = Gmap.find key !delimiters_map in
-    Options.if_verbose warning ("Hidding binding of key "^key^" to "^oldsc)
+    Options.if_verbose warning ("Hiding binding of key "^key^" to "^oldsc)
   end;
   delimiters_map := Gmap.add key scope !delimiters_map
 
@@ -295,8 +300,8 @@ let declare_notation_interpretation ntn scopt pat df =
   let scope = match scopt with Some s -> s | None -> default_scope in
   let sc = find_scope scope in
   if Gmap.mem ntn sc.notations && Options.is_verbose () then
-    warning ("Notation "^ntn^" was already used"^
-    (if scopt = None then "" else " in scope "^scope));
+    msg_warning (str ("Notation "^ntn^" was already used"^
+    (if scopt = None then "" else " in scope "^scope)));
   let sc = { sc with notations = Gmap.add ntn (pat,df) sc.notations } in
   scope_map := Gmap.add scope sc !scope_map;
   if scopt = None then scope_stack := SingleNotation ntn :: !scope_stack
@@ -336,9 +341,9 @@ let find_prim_token g loc p sc =
   check_required_module loc sc spdir;
   g (interp ()), (dirpath (fst spdir),"")
 
-let interp_prim_token_gen g loc p scopes =
-  let all_scopes = push_scopes scopes !scope_stack in
-  try find_interpretation (find_prim_token g loc p) all_scopes
+let interp_prim_token_gen g loc p local_scopes =
+  let scopes = make_current_scopes local_scopes in
+  try find_interpretation (find_prim_token g loc p) scopes
   with Not_found ->
     user_err_loc (loc,"interp_prim_token",
     (match p with
@@ -351,8 +356,9 @@ let interp_prim_token =
 let interp_prim_token_cases_pattern loc p name =
   interp_prim_token_gen (cases_pattern_of_rawconstr name) loc p
 
-let rec interp_notation loc ntn scopes =
-  try find_interpretation (find_notation ntn) (push_scopes scopes !scope_stack) 
+let rec interp_notation loc ntn local_scopes =
+  let scopes = make_current_scopes local_scopes in
+  try find_interpretation (find_notation ntn) scopes
   with Not_found ->
     user_err_loc
     (loc,"",str ("Unknown interpretation for notation \""^ntn^"\""))
@@ -366,7 +372,7 @@ let uninterp_cases_pattern_notations c =
 let availability_of_notation (ntn_scope,ntn) scopes =
   let f scope =
     Gmap.mem ntn (Gmap.find scope !scope_map).notations in
-  find_without_delimiters f (ntn_scope,Some ntn) scopes
+  find_without_delimiters f (ntn_scope,Some ntn) (make_current_scopes scopes)
 
 let uninterp_prim_token c =
   try 
@@ -387,8 +393,9 @@ let uninterp_prim_token_cases_pattern c =
       | Some n -> (na,sc,n)
   with Not_found -> raise No_match
 
-let availability_of_prim_token printer_scope scopes =
+let availability_of_prim_token printer_scope local_scopes =
   let f scope = Hashtbl.mem prim_token_interpreter_tab scope in
+  let scopes = make_current_scopes local_scopes in
   option_map snd (find_without_delimiters f (Some printer_scope,None) scopes)
 
 (* Miscellaneous *)
@@ -494,7 +501,7 @@ let make_notation_key symbols =
 let decompose_notation_key s =
   let len = String.length s in
   let rec decomp_ntn dirs n =
-    if n>=len then dirs else
+    if n>=len then List.rev dirs else
     let pos =
       try
 	String.index_from s n ' ' 
diff --git a/interp/notation.mli b/interp/notation.mli
index 32ec7a96..840274c5 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: notation.mli 7984 2006-02-04 20:14:55Z herbelin $ i*)
+(*i $Id: notation.mli 9208 2006-10-05 07:45:01Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -32,12 +32,15 @@ type delimiters = string
 type scope
 type scopes (* = [scope_name list] *)
 
+type local_scopes = tmp_scope_name option * scope_name list
+
 val type_scope : scope_name
 val declare_scope : scope_name -> unit
 
+val current_scopes : unit -> scopes
+
 (* Open scope *)
 
-val current_scopes : unit -> scopes
 val open_close_scope : 
   (* locality *) bool * (* open *) bool * scope_name -> unit
 
@@ -76,10 +79,10 @@ val declare_string_interpreter : scope_name -> required_module ->
 (* Return the [term]/[cases_pattern] bound to a primitive token in a
    given scope context*)
 
-val interp_prim_token : loc -> prim_token -> scope_name list -> 
+val interp_prim_token : loc -> prim_token -> local_scopes ->
   rawconstr * (notation_location * scope_name option)
 val interp_prim_token_cases_pattern : loc -> prim_token -> name -> 
-  scope_name list -> cases_pattern * (notation_location * scope_name option)
+  local_scopes -> cases_pattern * (notation_location * scope_name option)
 
 (* Return the primitive token associated to a [term]/[cases_pattern];
    raise [No_match] if no such token *)
@@ -90,7 +93,7 @@ val uninterp_prim_token_cases_pattern :
   cases_pattern -> name * scope_name * prim_token
 
 val availability_of_prim_token : 
-  scope_name -> scopes -> delimiters option option
+  scope_name -> local_scopes -> delimiters option option
 
 (*s Declare and interpret back and forth a notation *)
 
@@ -105,7 +108,7 @@ val declare_notation_interpretation : notation -> scope_name option ->
 val declare_uninterpretation : interp_rule -> interpretation -> unit
 
 (* Return the interpretation bound to a notation *)
-val interp_notation : loc -> notation -> scope_name list -> 
+val interp_notation : loc -> notation -> local_scopes ->
       interpretation * (notation_location * scope_name option)
 
 (* Return the possible notations for a given term *)
@@ -117,7 +120,7 @@ val uninterp_cases_pattern_notations : cases_pattern ->
 (* Test if a notation is available in the scopes *)
 (* context [scopes]; if available, the result is not None; the first *)
 (* argument is itself not None if a delimiters is needed *)
-val availability_of_notation : scope_name option * notation -> scopes -> 
+val availability_of_notation : scope_name option * notation -> local_scopes -> 
   (scope_name option * delimiters option) option
 
 (*s Declare and test the level of a (possibly uninterpreted) notation *)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index f3099346..936b6830 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: topconstr.ml 9032 2006-07-07 16:30:34Z herbelin $ *)
+(* $Id: topconstr.ml 9226 2006-10-09 16:11:01Z herbelin $ *)
 
 (*i*)
 open Pp
@@ -39,17 +39,24 @@ type aconstr =
   | ALetIn of name * aconstr * aconstr
   | ACases of aconstr option *
       (aconstr * (name * (inductive * int * name list) option)) list *
-      (identifier list * cases_pattern list * aconstr) list
+      (cases_pattern list * aconstr) list
   | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
   | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
   | ASort of rawsort
   | AHole of Evd.hole_kind
   | APatVar of patvar
   | ACast of aconstr * cast_type * aconstr
-  
-let name_app f e = function
-  | Name id -> let (id, e) = f id e in (e, Name id)
-  | Anonymous -> e,Anonymous
+
+(**********************************************************************)
+(* Re-interpret a notation as a rawconstr, taking care of binders     *)
+
+let rec cases_pattern_fold_map loc g e = function
+  | PatVar (_,na) ->
+      let e',na' = name_fold_map g e na in e', PatVar (loc,na')
+  | PatCstr (_,cstr,patl,na) ->
+      let e',na' = name_fold_map g e na in
+      let e',patl' = list_fold_map (cases_pattern_fold_map loc g) e patl in
+      e', PatCstr (loc,cstr,patl',na')
 
 let rec subst_rawvars l = function
   | RVar (_,id) as r -> (try List.assoc id l with Not_found -> r)
@@ -67,32 +74,33 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
       let outerl = (ldots_var,inner)::(if swap then [x,RVar(loc,y)] else []) in
       subst_rawvars outerl it
   | ALambda (na,ty,c) ->
-      let e,na = name_app g e na in RLambda (loc,na,f e ty,f e c)
+      let e,na = name_fold_map g e na in RLambda (loc,na,f e ty,f e c)
   | AProd (na,ty,c) ->
-      let e,na = name_app g e na in RProd (loc,na,f e ty,f e c)
+      let e,na = name_fold_map g e na in RProd (loc,na,f e ty,f e c)
   | ALetIn (na,b,c) ->
-      let e,na = name_app g e na in RLetIn (loc,na,f e b,f e c)
+      let e,na = name_fold_map g e na in RLetIn (loc,na,f e b,f e c)
   | ACases (rtntypopt,tml,eqnl) ->
       let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
 	let e',t' = match t with
 	| None -> e',None
 	| Some (ind,npar,nal) -> 
 	  let e',nal' = List.fold_right (fun na (e',nal) -> 
-	      let e',na' = name_app g e' na in e',na'::nal) nal (e',[]) in
+	      let e',na' = name_fold_map g e' na in e',na'::nal) nal (e',[]) in
 	  e',Some (loc,ind,npar,nal') in
-	let e',na' = name_app g e' na in
+	let e',na' = name_fold_map g e' na in
 	(e',(f e tm,(na',t'))::tml')) tml (e,[]) in
-      let fold id (idl,e) = let (id,e) = g id e in (id::idl,e) in
-      let eqnl' = List.map (fun (idl,pat,rhs) ->
-        let (idl,e) = List.fold_right fold idl ([],e) in
-	(loc,idl,pat,f e rhs)) eqnl in
+      let fold (idl,e) id = let (e,id) = g e id in ((id::idl,e),id) in
+      let eqnl' = List.map (fun (patl,rhs) ->
+	let ((idl,e),patl) =
+	  list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in
+	(loc,idl,patl,f e rhs)) eqnl in
       RCases (loc,option_map (f e') rtntypopt,tml',eqnl')
   | ALetTuple (nal,(na,po),b,c) ->
-      let e,nal = list_fold_map (name_app g) e nal in 
-      let e,na = name_app g e na in
+      let e,nal = list_fold_map (name_fold_map g) e nal in 
+      let e,na = name_fold_map g e na in
       RLetTuple (loc,nal,(na,option_map (f e) po),f e b,f e c)
   | AIf (c,(na,po),b1,b2) ->
-      let e,na = name_app g e na in
+      let e,na = name_fold_map g e na in
       RIf (loc,f e c,(na,option_map (f e) po),f e b1,f e b2)
   | ACast (c,k,t) -> RCast (loc,f e c, k,f e t)
   | ASort x -> RSort (loc,x)
@@ -102,17 +110,11 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
 
 let rec rawconstr_of_aconstr loc x =
   let rec aux () x = 
-    rawconstr_of_aconstr_with_binders loc (fun id () -> (id,())) aux () x
+    rawconstr_of_aconstr_with_binders loc (fun () id -> ((),id)) aux () x
   in aux () x
 
-let rec subst_pat subst pat = 
-  match pat with
-  | PatVar _ -> pat
-  | PatCstr (loc,((kn,i),j),cpl,n) -> 
-      let kn' = subst_kn subst kn 
-      and cpl' = list_smartmap (subst_pat subst) cpl in
-        if kn' == kn && cpl' == cpl then pat else
-          PatCstr (loc,((kn',i),j),cpl',n)
+(****************************************************************************)
+(* Translating a rawconstr into a notation, interpreting recursive patterns *)
 
 let add_name r = function
   | Anonymous -> ()
@@ -179,9 +181,7 @@ let aconstr_and_vars_of_rawconstr a =
   | RProd (_,na,ty,c) -> add_name found na; AProd (na,aux ty,aux c)
   | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c)
   | RCases (_,rtntypopt,tml,eqnl) ->
-      let f (_,idl,pat,rhs) =
-        found := idl@(!found);
-        (idl,pat,aux rhs) in
+      let f (_,idl,pat,rhs) = found := idl@(!found); (pat,aux rhs) in
       ACases (option_map aux rtntypopt,
         List.map (fun (tm,(na,x)) ->
 	  add_name found na;
@@ -246,9 +246,20 @@ let aconstr_of_rawconstr vars a =
   List.iter check_type vars;
   a
 
+(* Substitution of kernel names, avoiding a list of bound identifiers *)
+
 let aconstr_of_constr avoiding t =
  aconstr_of_rawconstr [] (Detyping.detype false avoiding [] t)
 
+let rec subst_pat subst pat = 
+  match pat with
+  | PatVar _ -> pat
+  | PatCstr (loc,((kn,i),j),cpl,n) -> 
+      let kn' = subst_kn subst kn 
+      and cpl' = list_smartmap (subst_pat subst) cpl in
+        if kn' == kn && cpl' == cpl then pat else
+          PatCstr (loc,((kn',i),j),cpl',n)
+
 let rec subst_aconstr subst bound raw =
   match raw with
   | ARef ref -> 
@@ -265,22 +276,26 @@ let rec subst_aconstr subst bound raw =
 	  AApp(r',rl')
 
   | AList (id1,id2,r1,r2,b) -> 
-      let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in
+      let r1' = subst_aconstr subst bound r1
+      and r2' = subst_aconstr subst bound r2 in
 	if r1' == r1 && r2' == r2 then raw else
 	  AList (id1,id2,r1',r2',b)
 
   | ALambda (n,r1,r2) -> 
-      let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in
+      let r1' = subst_aconstr subst bound r1
+      and r2' = subst_aconstr subst bound r2 in
 	if r1' == r1 && r2' == r2 then raw else
 	  ALambda (n,r1',r2')
 
   | AProd (n,r1,r2) -> 
-      let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in
+      let r1' = subst_aconstr subst bound r1
+      and r2' = subst_aconstr subst bound r2 in
 	if r1' == r1 && r2' == r2 then raw else
 	  AProd (n,r1',r2')
 
   | ALetIn (n,r1,r2) -> 
-      let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in
+      let r1' = subst_aconstr subst bound r1 
+      and r2' = subst_aconstr subst bound r2 in
 	if r1' == r1 && r2' == r2 then raw else
 	  ALetIn (n,r1',r2')
 
@@ -295,11 +310,11 @@ let rec subst_aconstr subst bound raw =
 	  if a' == a && signopt' == signopt then x else (a',(n,signopt')))
         rl
       and branches' = list_smartmap 
-                        (fun (idl,cpl,r as branch) ->
+                        (fun (cpl,r as branch) ->
                            let cpl' = list_smartmap (subst_pat subst) cpl
                            and r' = subst_aconstr subst bound r in
                              if cpl' == cpl && r' == r then branch else
-                               (idl,cpl',r'))
+                               (cpl',r'))
                         branches
       in
         if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' &
@@ -331,7 +346,8 @@ let rec subst_aconstr subst bound raw =
       Evd.InternalHole | Evd.TomatchTypeParameter _) -> raw
 
   | ACast (r1,k,r2) -> 
-      let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in
+      let r1' = subst_aconstr subst bound r1 
+      and r2' = subst_aconstr subst bound r2 in
 	if r1' == r1 && r2' == r2 then raw else
 	  ACast (r1',k,r2')
 
@@ -394,6 +410,15 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
   | (Anonymous,Anonymous) -> alp,sigma
   | _ -> raise No_match
 
+let rec match_cases_pattern metas acc pat1 pat2 =
+  match (pat1,pat2) with
+  | PatVar (_,na1), PatVar (_,na2) -> match_names metas acc na1 na2
+  | PatCstr (_,c1,patl1,na1), PatCstr (_,c2,patl2,na2)
+      when c1 = c2 & List.length patl1 = List.length patl2 ->
+      List.fold_left2 (match_cases_pattern metas)
+	(match_names metas acc na1 na2) patl1 patl2
+  | _ -> raise No_match
+
 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
@@ -411,7 +436,8 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
   | RLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) ->
      match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
   | RCases (_,rtno1,tml1,eqnl1), ACases (rtno2,tml2,eqnl2) 
-      when List.length tml1 = List.length tml2 ->
+      when List.length tml1 = List.length tml2
+	 & List.length eqnl1 = List.length eqnl2 ->
       let rtno1' = abstract_return_type_context_rawconstr tml1 rtno1 in
       let rtno2' = abstract_return_type_context_aconstr tml2 rtno2 in
       let sigma = option_fold_left2 (match_ alp metas) sigma rtno1' rtno2' in
@@ -461,15 +487,19 @@ and match_binders alp metas na1 na2 sigma b1 b2 =
   let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in
   match_ alp metas sigma b1 b2
 
-and match_equations alp metas sigma (_,idl1,pat1,rhs1) (idl2,pat2,rhs2) =
-  if idl1 = idl2 & pat1 = pat2 (* Useful to reason up to alpha ?? *) then
-    match_ alp metas sigma rhs1 rhs2
-  else raise No_match
+and match_equations alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) =
+  (* patl1 and patl2 have the same length because they respectively
+     correspond to some tml1 and tml2 that have the same length *)
+  let (alp,sigma) = 
+    List.fold_left2 (match_cases_pattern metas) (alp,sigma) patl1 patl2 in
+  match_ alp metas sigma rhs1 rhs2
 
 type scope_name = string
 
+type tmp_scope_name = scope_name
+
 type interpretation = 
-    (identifier * (scope_name option * scope_name list)) list * aconstr
+    (identifier * (tmp_scope_name option * scope_name list)) list * aconstr
 
 let match_aconstr c (metas_scl,pat) =
   let subst = match_ [] (List.map fst metas_scl) [] c pat in
@@ -592,7 +622,7 @@ let constr_loc = function
   | CDelimiters (loc,_,_) -> loc
   | CDynamic _ -> dummy_loc
 
-let cases_pattern_loc = function
+let cases_pattern_expr_loc = function
   | CPatAlias (loc,_,_) -> loc
   | CPatCstr (loc,_,_) -> loc
   | CPatAtom (loc,_) -> loc
@@ -605,35 +635,98 @@ let occur_var_constr_ref id = function
   | Ident (loc,id') -> id = id'
   | Qualid _ -> false
 
-let rec occur_var_constr_expr id = function
-  | CRef r -> occur_var_constr_ref id r
-  | CArrow (loc,a,b) -> occur_var_constr_expr id a or occur_var_constr_expr id b
-  | CAppExpl (loc,(_,r),l) ->
-      occur_var_constr_ref id r or List.exists (occur_var_constr_expr id) l
-  | CApp (loc,(_,f),l) ->
-      occur_var_constr_expr id f or
-      List.exists (fun (a,_) -> occur_var_constr_expr id a) l
-  | CProdN (_,l,b) -> occur_var_binders id b l
-  | CLambdaN (_,l,b) -> occur_var_binders id b l
-  | CLetIn (_,na,a,b) -> occur_var_binders id b [[na],a]
-  | CCast (loc,a,_,b) -> 
-    occur_var_constr_expr id a or occur_var_constr_expr id b
-  | CNotation (_,_,l) -> List.exists (occur_var_constr_expr id) l
-  | CDelimiters (loc,_,a) -> occur_var_constr_expr id a
-  | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ -> false
-  | CCases (loc,_,_,_) 
-  | CLetTuple (loc,_,_,_,_) 
-  | CIf (loc,_,_,_,_) 
-  | CFix (loc,_,_) 
+let ids_of_cases_indtype =
+  let add_var ids = function CRef (Ident (_,id)) -> id::ids | _ -> ids in
+  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)
+    (* assume the ntn is applicative and does not instantiate the head !! *)
+    | CAppExpl (_,_,l) -> List.fold_left add_var [] l
+    | CDelimiters(_,_,c) -> vars_of c
+    | _ -> [] in
+  vars_of
+
+let ids_of_cases_tomatch tms =
+  List.fold_right
+    (fun (_,(ona,indnal)) l ->
+      option_fold_right (fun t -> (@) (ids_of_cases_indtype t))
+      indnal (option_fold_right name_cons ona l))
+    tms []
+
+let is_constructor id =
+  try ignore (Nametab.extended_locate (make_short_qualid id)); true
+  with Not_found -> true
+ 
+let rec cases_pattern_fold_names f a = function
+  | CPatAlias (_,pat,id) -> f id a
+  | CPatCstr (_,_,patl) | CPatOr (_,patl) | CPatNotation (_,_,patl) ->
+      List.fold_left (cases_pattern_fold_names f) a patl
+  | CPatDelimiters (_,_,pat) -> cases_pattern_fold_names f a pat
+  | CPatAtom (_,Some (Ident (_,id))) when not (is_constructor id) -> f id a
+  | CPatPrim _ | CPatAtom _ -> a
+
+let ids_of_pattern_list =
+  List.fold_left (List.fold_left (cases_pattern_fold_names Idset.add))
+    Idset.empty
+
+let rec fold_constr_expr_binders g f n acc b = function
+  | (nal,t)::l ->
+      let nal = snd (List.split nal) in
+      let n' = List.fold_right (name_fold g) nal n in
+      f n (fold_constr_expr_binders g f n' acc b l) t
+  | [] ->
+      f n acc b
+
+let rec fold_local_binders g f n acc b = function
+  | LocalRawAssum (nal,t)::l ->
+      let nal = snd (List.split nal) in
+      let n' = List.fold_right (name_fold g) nal n in
+      f n (fold_local_binders g f n' acc b l) t
+  | LocalRawDef ((_,na),t)::l ->
+      f n (fold_local_binders g f (name_fold g na n) acc b l) t
+  | _ ->
+      f n acc b
+
+let fold_constr_expr_with_binders g f n acc = function
+  | CArrow (loc,a,b) -> f n (f n acc a) b
+  | CAppExpl (loc,(_,_),l) -> List.fold_left (f n) acc l
+  | CApp (loc,(_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
+  | CProdN (_,l,b) | CLambdaN (_,l,b) -> fold_constr_expr_binders g f n acc b l
+  | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],a]
+  | CCast (loc,a,_,b) -> f n (f n acc a) b
+  | CNotation (_,_,l) -> List.fold_left (f n) acc l
+  | CDelimiters (loc,_,a) -> f n acc a
+  | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _  | CRef _ ->
+      acc
+  | CCases (loc,rtnpo,al,bl) ->
+      let ids = ids_of_cases_tomatch al in
+      let acc = option_fold_left (f (List.fold_right g ids n)) acc rtnpo in
+      let acc = List.fold_left (f n) acc (List.map fst al) in
+      List.fold_right (fun (loc,patl,rhs) acc ->
+	let ids = ids_of_pattern_list patl in
+	f (Idset.fold g ids n) acc rhs) bl acc
+  | CLetTuple (loc,nal,(ona,po),b,c) ->
+      let n' = List.fold_right (name_fold g) nal n in
+      f (option_fold_right (name_fold g) ona n') (f n acc b) c
+  | CIf (_,c,(ona,po),b1,b2) ->
+      let acc = f n (f n (f n acc b1) b2) c in
+      option_fold_left (f (option_fold_right (name_fold g) ona n)) acc po
+  | CFix (loc,_,l) ->
+      let n' = List.fold_right (fun (id,_,_,_,_) -> g id) l n in
+      List.fold_right (fun (_,(_,o),lb,t,c) acc ->
+	fold_local_binders g f n' 
+	  (fold_local_binders g f n acc t lb) c lb) l acc
   | CCoFix (loc,_,_) -> 
-      Pp.warning "Capture check in multiple binders not done"; false
+      Pp.warning "Capture check in multiple binders not done"; acc
+
+let free_vars_of_constr_expr c = 
+  let rec aux bdvars l = function
+  | CRef (Ident (_,id)) -> if List.mem id bdvars then l else Idset.add id l
+  | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c
+  in aux [] Idset.empty c
 
-and occur_var_binders id b = function
-  | (idl,a)::l -> 
-      occur_var_constr_expr id a or
-      (not (List.mem (Name id) (snd (List.split idl)))
-      & occur_var_binders id b l)
-  | [] -> occur_var_constr_expr id b
+let occur_var_constr_expr id c = Idset.mem id (free_vars_of_constr_expr c)
 
 let mkIdentC id  = CRef (Ident (dummy_loc, id))
 let mkRefC r     = CRef r
@@ -665,19 +758,6 @@ let coerce_to_id = function
 
 (* Used in correctness and interface *)
 
-
-let names_of_cases_indtype =
-  let add_var ids = function CRef (Ident (_,id)) -> id::ids | _ -> ids in
-  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)
-    (* assume the ntn is applicative and does not instantiate the head !! *)
-    | CAppExpl (_,_,l) -> List.fold_left add_var [] l
-    | CDelimiters(_,_,c) -> vars_of c
-    | _ -> [] in
-  vars_of
-
 let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e
 
 let map_binders f g e bl =
@@ -696,7 +776,7 @@ let map_local_binders f g e bl =
   let (e,rbl) = List.fold_left h (e,[]) bl in
   (e, List.rev rbl)
 
-let map_constr_expr_with_binders f g e = function
+let map_constr_expr_with_binders g f e = function
   | CArrow (loc,a,b) -> CArrow (loc,f e a,f e b)
   | CAppExpl (loc,r,l) -> CAppExpl (loc,r,List.map (f e) l) 
   | CApp (loc,(p,a),l) -> 
@@ -714,18 +794,9 @@ let map_constr_expr_with_binders f g e = function
   | CCases (loc,rtnpo,a,bl) ->
       (* TODO: apply g on the binding variables in pat... *)
       let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
-      let e' = 
-	List.fold_right
-	  (fun (tm,(na,indnal)) e ->
-	    option_fold_right
-	      (fun t ->
-		let ids = names_of_cases_indtype t in
-		List.fold_right g ids)
-            indnal (option_fold_right (name_fold g) na e))
-	  a e
-      in
-      CCases (loc,option_map (f e') rtnpo,
-         List.map (fun (tm,x) -> (f e tm,x)) a,bl)
+      let ids = ids_of_cases_tomatch a in
+      let po = option_map (f (List.fold_right g ids e)) rtnpo in
+      CCases (loc, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl)
   | CLetTuple (loc,nal,(ona,po),b,c) ->
       let e' = List.fold_right (name_fold g) nal e in
       let e'' = option_fold_right (name_fold g) ona e in
@@ -753,8 +824,8 @@ let map_constr_expr_with_binders f g e = function
 let rec replace_vars_constr_expr l = function
   | CRef (Ident (loc,id)) as x ->
       (try CRef (Ident (loc,List.assoc id l)) with Not_found -> x)
-  | c -> map_constr_expr_with_binders replace_vars_constr_expr 
-      (fun id l -> List.remove_assoc id l) l c
+  | c -> map_constr_expr_with_binders List.remove_assoc 
+           replace_vars_constr_expr l c
 
 (**********************************************************************)
 (* Concrete syntax for modules and modules types *)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 51853089..131e4170 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: topconstr.mli 9032 2006-07-07 16:30:34Z herbelin $ i*)
+(*i $Id: topconstr.mli 9226 2006-10-09 16:11:01Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -35,7 +35,7 @@ type aconstr =
   | ALetIn of name * aconstr * aconstr
   | ACases of aconstr option *
       (aconstr * (name * (inductive * int * name list) option)) list *
-      (identifier list * cases_pattern list * aconstr) list
+      (cases_pattern list * aconstr) list
   | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
   | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
   | ASort of rawsort
@@ -43,30 +43,50 @@ type aconstr =
   | APatVar of patvar
   | ACast of aconstr * cast_type * aconstr
 
+(**********************************************************************)
+(* Translate a rawconstr into a notation given the list of variables  *)
+(* bound by the notation; also interpret recursive patterns           *) 
+
+val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr
+
+(* Name of the special identifier used to encode recursive notations  *)
+val ldots_var : identifier
+
+(* Equality of rawconstr (warning: only partially implemented) *)
+val eq_rawconstr : rawconstr -> rawconstr -> bool
+
+(**********************************************************************)
+(* Re-interpret a notation as a rawconstr, taking care of binders     *)
+
 val rawconstr_of_aconstr_with_binders : loc -> 
-  (identifier -> 'a -> identifier * 'a) ->
+  ('a -> identifier -> 'a * identifier) ->
   ('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr
 
 val rawconstr_of_aconstr : loc -> aconstr -> rawconstr
 
-val subst_aconstr : substitution -> Names.identifier list -> aconstr -> aconstr
+(**********************************************************************)
+(* Substitution of kernel names, avoiding a list of bound identifiers *)
 
-val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr
+val subst_aconstr : substitution -> identifier list -> aconstr -> aconstr
 
-val eq_rawconstr : rawconstr -> rawconstr -> bool
+(**********************************************************************)
+(* [match_aconstr metas] matches a rawconstr against an aconstr with  *)
+(* metavariables in [metas]; raise [No_match] if the matching fails   *)
 
-(* [match_aconstr metas] match a rawconstr against an aconstr with
-   metavariables in [metas]; it raises [No_match] if the matching fails *)
 exception No_match
 
 type scope_name = string
+
+type tmp_scope_name = scope_name
+
 type interpretation = 
-    (identifier * (scope_name option * scope_name list)) list * aconstr
+    (identifier * (tmp_scope_name option * scope_name list)) list * aconstr
 
 val match_aconstr : rawconstr -> interpretation ->
-      (rawconstr * (scope_name option * scope_name list)) list
+      (rawconstr * (tmp_scope_name option * scope_name list)) list
 
-(*s Concrete syntax for terms *)
+(**********************************************************************)
+(*s Concrete syntax for terms                                         *)
 
 type notation = string
 
@@ -128,18 +148,21 @@ and local_binder =
   | LocalRawDef of name located * constr_expr
   | LocalRawAssum of name located list * constr_expr
 
+(**********************************************************************)
+(* Utilities on constr_expr                                           *)
 
 val constr_loc : constr_expr -> loc
 
-val cases_pattern_loc : cases_pattern_expr -> loc
+val cases_pattern_expr_loc : cases_pattern_expr -> loc
 
 val replace_vars_constr_expr :
   (identifier * identifier) list -> constr_expr -> constr_expr
 
+val free_vars_of_constr_expr : constr_expr -> Idset.t
 val occur_var_constr_expr : identifier -> constr_expr -> bool
 
 (* Specific function for interning "in indtype" syntax of "match" *)
-val names_of_cases_indtype : constr_expr -> identifier list
+val ids_of_cases_indtype : constr_expr -> identifier list
 
 val mkIdentC : identifier -> constr_expr
 val mkRefC : reference -> constr_expr
@@ -172,10 +195,11 @@ val names_of_local_binders : local_binder list -> name located list
 (* in pattern-matching clauses and in binders of the form [x,y:T(x)] *)
 
 val map_constr_expr_with_binders :
-  ('a -> constr_expr -> constr_expr) ->
-      (identifier -> 'a -> 'a) -> 'a -> constr_expr -> constr_expr
+  (identifier -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) ->
+      'a -> constr_expr -> constr_expr
 
-(* Concrete syntax for modules and modules types *)
+(**********************************************************************)
+(* Concrete syntax for modules and module types                       *)
 
 type with_declaration_ast = 
   | CWith_Module of identifier list located * qualid located
@@ -188,6 +212,3 @@ 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