Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

34 files changed, 721 insertions, 640 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a32aaf45..b0fe83a3 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cases.ml 8693 2006-04-10 12:05:05Z msozeau $ *)
+(* $Id: cases.ml 8875 2006-05-29 19:59:11Z msozeau $ *)
 
 open Util
 open Names
@@ -66,13 +66,10 @@ let error_needs_inversion env x t =
 module type S = sig
   val compile_cases :
     loc ->
-    (type_constraint -> env -> rawconstr -> unsafe_judgment) *    
+    (type_constraint -> env -> rawconstr -> unsafe_judgment) *
       Evd.evar_defs ref ->
     type_constraint -> 
-    env ->
-    rawconstr option *
-      (rawconstr * (name * (loc * inductive * name list) option)) list *
-      (loc * identifier list * cases_pattern list * rawconstr) list ->
+    env -> rawconstr option * tomatch_tuple * cases_clauses ->
     unsafe_judgment
 end
 
@@ -138,14 +135,9 @@ type 'a lifted = int * 'a
 
 let insert_lifted a = (0,a);;
 
-(* The pattern variables for [it] are in [user_ids] and the variables
-   to avoid are in [other_ids]. 
-*)
-
 type rhs =
     { rhs_env    : env;
-      other_ids  : identifier list;
-      user_ids   : identifier list;
+      avoid_ids  : identifier list;
       rhs_lift   : int;
       it         : rawconstr }
 
@@ -321,16 +313,21 @@ let rec find_row_ind = function
   | PatCstr(loc,c,_,_) :: _ -> Some (loc,c)
 
 let inductive_template isevars env tmloc ind =
-  let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let (ntys,_) = splay_prod env (Evd.evars_of !isevars) mip.mind_nf_arity in
+  let arsign = get_full_arity_sign env ind in
   let hole_source = match tmloc with 
     | Some loc -> fun i -> (loc, Evd.TomatchTypeParameter (ind,i))
     | None -> fun _ -> (dummy_loc, Evd.InternalHole) in
-   let (evarl,_) =
+   let (_,evarl,_) =
     List.fold_right
-      (fun (na,ty) (evl,n) ->
-	(e_new_evar isevars env ~src:(hole_source n) (substl evl ty))::evl,n+1)
-      ntys ([],1) in
+      (fun (na,b,ty) (subst,evarl,n) ->
+	match b with
+        | None ->
+	    let ty' = substl subst ty in
+	    let e = e_new_evar isevars env ~src:(hole_source n) ty' in
+	    (e::subst,e::evarl,n+1) 
+	| Some b ->
+	    (b::subst,evarl,n+1))
+      arsign ([],[],1) in
    applist (mkInd ind,List.rev evarl)
 
 let inh_coerce_to_ind isevars env ty tyi =
@@ -349,7 +346,7 @@ let unify_tomatch_with_patterns isevars env typ tm =
 
 let find_tomatch_tycon isevars env loc = function
   (* Try first if some 'in I ...' is present and can be used as a constraint *)
-  | Some (_,ind,_),_ 
+  | Some (_,ind,_,_),_ 
   (* Otherwise try to get constraints from (the 1st) constructor in clauses *)
   | None, Some (_,(ind,_)) ->
       mk_tycon (inductive_template isevars env loc ind)
@@ -434,7 +431,7 @@ let mkDeclTomatch na = function
 
 let map_tomatch_type f = function
   | IsInd (t,ind) -> IsInd (f t,map_inductive_type f ind)
-  | NotInd (c,t) -> NotInd (option_app f c, f t)
+  | NotInd (c,t) -> NotInd (option_map f c, f t)
 
 let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth)
 let lift_tomatch_type n = liftn_tomatch_type n 1
@@ -701,7 +698,7 @@ let get_names env sign eqns =
   (* Otherwise, we take names from the parameters of the constructor but
      avoiding conflicts with user ids *)
   let allvars =
-    List.fold_left (fun l (_,eqn) -> list_union l eqn.rhs.other_ids) [] eqns in
+    List.fold_left (fun l (_,eqn) -> list_union l eqn.rhs.avoid_ids) [] eqns in
   let names4,_ =
     List.fold_left2
       (fun (l,avoid) d na ->
@@ -793,7 +790,7 @@ let prepare_unif_pb typ cs =
   let typ' =
     if noccur_between_without_evar 1 n typ then lift (-n) typ
     else (* TODO4-1 *)
-      error "Inference of annotation not yet implemented in this case" in
+      error "Unable to infer return clause of this pattern-matching problem" in
   let args = extended_rel_list (-n) cs.cs_args in
   let ci = applist (mkConstruct cs.cs_cstr, cs.cs_params@args) in
 
@@ -1172,7 +1169,7 @@ let rec generalize_problem pb current = function
       let tomatch = regeneralize_index_tomatch (i+1) tomatch in
       { pb with
 	  tomatch = Abstract d :: tomatch;
-          pred = option_app (generalize_predicate current i d) pb'.pred }
+          pred = option_map (generalize_predicate current i d) pb'.pred }
 
 (* No more patterns: typing the right-hand-side of equations *)
 let build_leaf pb =
@@ -1187,7 +1184,7 @@ let build_leaf pb =
 let shift_problem (current,t) pb =
   {pb with
      tomatch = Alias (current,current,NonDepAlias,type_of_tomatch t)::pb.tomatch;
-     pred = option_app (specialize_predicate_var (current,t)) pb.pred;
+     pred = option_map (specialize_predicate_var (current,t)) pb.pred;
      history = push_history_pattern 0 AliasLeaf pb.history;
      mat = List.map remove_current_pattern pb.mat }
 
@@ -1257,7 +1254,7 @@ let build_branch current deps pb eqns const_info =
   { pb with
       env = push_rels sign pb.env;
       tomatch = List.rev_append currents tomatch;
-      pred = option_app (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred;
+      pred = option_map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred;
       history = history;
       mat = List.map (push_rels_eqn_with_names sign) submat }
 
@@ -1329,7 +1326,7 @@ and compile_generalization pb d rest =
     { pb with
        env = push_rel d pb.env;
        tomatch = rest;
-       pred = option_app ungeneralize_predicate pb.pred;
+       pred = option_map ungeneralize_predicate pb.pred;
        mat = List.map (push_rels_eqn [d]) pb.mat } in
   let patstat,j = compile pb in
   patstat, 
@@ -1355,7 +1352,7 @@ and compile_alias pb (deppat,nondeppat,d,t) rest =
     {pb with
        env = newenv;
        tomatch = tomatch;
-       pred = option_app (lift_predicate n) pb.pred;
+       pred = option_map (lift_predicate n) pb.pred;
        history = history;
        mat = mat } in
   let patstat,j = compile pb in
@@ -1368,78 +1365,16 @@ substituer après par les initiaux *)
 (**************************************************************************)
 (* Preparation of the pattern-matching problem                            *)
 
-(* Qu'est-ce qui faut pas faire pour traiter les alias ... *)
-
-(* On ne veut pas ajouter de primitive à Environ et le problème, c'est
-   donc de faire un renommage en se contraignant à parcourir l'env
-   dans le sens croissant. Ici, subst renomme des variables repérées
-   par leur numéro et seen_ids collecte celles dont on sait que les
-   variables de subst annule le scope *)
-let rename_env subst env =
-  let n = ref (rel_context_length (rel_context env)) in
-  let seen_ids = ref [] in
-  process_rel_context
-    (fun (na,c,t as d) env ->
-       let d =
-	 try
-	   let id = List.assoc !n subst in
-	   seen_ids := id :: !seen_ids;
-	   (Name id,c,t)
-	 with Not_found ->
-	   match na with
-	     | Name id when List.mem id !seen_ids -> (Anonymous,c,t)
-	     | _ -> d in
-       decr n;
-       push_rel d env) env
-
-let is_dependent_indtype = function
-  | NotInd _ -> false
-  | IsInd (_, IndType(_,realargs)) -> realargs <> []
-
-let prepare_initial_alias_eqn isdep tomatchl eqn =
-  let (subst, pats) = 
-  List.fold_right2
-    (fun pat (tm,tmtyp) (subst, stripped_pats) ->
-       match alias_of_pat pat with
-	 | Anonymous -> (subst, pat::stripped_pats)
-	 | Name idpat ->
-	     match kind_of_term tm with
-	       | Rel n when not (is_dependent_indtype tmtyp) & not isdep
-		   -> (n, idpat)::subst, (unalias_pat pat::stripped_pats)
-	       | _ -> (subst, pat::stripped_pats))
-    eqn.patterns tomatchl ([], []) in
-  let env = rename_env subst eqn.rhs.rhs_env in
-  { eqn with patterns = pats; rhs = { eqn.rhs with rhs_env = env } }
-
-let prepare_initial_aliases isdep tomatchl mat = mat
-(*  List.map (prepare_initial_alias_eqn isdep tomatchl) mat*)
-
-(*
-let prepare_initial_alias lpat tomatchl rhs =
-  List.fold_right2
-    (fun pat tm (stripped_pats, rhs) ->
-       match alias_of_pat pat with
-	 | Anonymous -> (pat::stripped_pats, rhs)
-	 | Name _ as na ->
-	     match tm with
-	       | RVar _ -> 
-		   (unalias_pat pat::stripped_pats, 
-		    RLetIn (dummy_loc, na, tm, rhs))
-	       | _ -> (pat::stripped_pats, rhs))
-    lpat tomatchl ([], rhs)
-*)
 (* builds the matrix of equations testing that each eqn has n patterns
  * and linearizing the _ patterns.
  * Syntactic correctness has already been done in astterm *)
 let matx_of_eqns env tomatchl eqns =
   let build_eqn (loc,ids,lpat,rhs) =
-(*    let initial_lpat,initial_rhs = prepare_initial_alias lpat tomatchl rhs in*)
     let initial_lpat,initial_rhs = lpat,rhs in
     let initial_rhs = rhs in
     let rhs =
       { rhs_env = env;
-	other_ids = ids@(ids_of_named_context (named_context env));
-	user_ids = ids;
+	avoid_ids = ids@(ids_of_named_context (named_context env));
 	rhs_lift = 0;
 	it = initial_rhs } in
     { dependencies = [];
@@ -1547,7 +1482,7 @@ let set_arity_signature dep n arsign tomatchl pred x =
   in
   decomp_block [] pred (tomatchl,arsign)
 
-let prepare_predicate_from_tycon loc dep env isevars tomatchs c =
+let prepare_predicate_from_tycon loc dep env isevars tomatchs sign c =
   let cook (n, l, env, signs) = function
     | c,IsInd (_,IndType(indf,realargs)) ->
 	let indf' = lift_inductive_family n indf in
@@ -1605,8 +1540,8 @@ let extract_arity_signature env0 tomatchl tmsign =
     match tm with
       | NotInd (bo,typ) -> 
 	  (match t with
-	    | None -> [na,option_app (lift n) bo,lift n typ]
-	    | Some (loc,_,_) -> 
+	    | None -> [na,option_map (lift n) bo,lift n typ]
+	    | Some (loc,_,_,_) -> 
  	    user_err_loc (loc,"",
 	    str "Unexpected type annotation for a term of non inductive type"))
       | IsInd (_,IndType(indf,realargs)) ->
@@ -1615,18 +1550,12 @@ let extract_arity_signature env0 tomatchl tmsign =
 	  let nrealargs = List.length realargs in
 	  let realnal =
 	    match t with
-	      | Some (loc,ind',nal) ->
-		  let nparams = List.length params in
+	      | Some (loc,ind',nparams,realnal) ->
 		  if ind <> ind' then
 		    user_err_loc (loc,"",str "Wrong inductive type");
-		  let nindargs = nparams + nrealargs in
-		  (* Normally done at interning time *)
-		  if List.length nal <> nindargs then
-		    error_wrong_numarg_inductive_loc loc env0 ind' nindargs;
-		  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");
+		  if List.length params <> nparams
+		    or nrealargs <> List.length realnal then
+		      anomaly "Ill-formed 'in' clause in cases";
 		  List.rev realnal
 	      | None -> list_tabulate (fun _ -> Anonymous) nrealargs in
 	  let arsign = fst (get_arity env0 indf') in
@@ -1665,7 +1594,7 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
       (match tycon with
        | Some (None, t) ->
 	   let names,pred = 
-	     prepare_predicate_from_tycon loc false env isevars tomatchs t 
+	     prepare_predicate_from_tycon loc false env isevars tomatchs sign t 
 	   in Some (build_initial_predicate false names pred)
        | _ -> None)
 
@@ -1677,8 +1606,9 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
       let allnames = List.rev (List.map (List.map pi1) arsign) in
       let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in
       let _ = 
-	option_app (fun tycon -> 
-		      isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val tycon)
+	option_map (fun tycon -> 
+		      isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val 
+		      (lift_tycon_type (List.length arsign) tycon))
 	  tycon
       in
       let predccl = (j_nf_isevar !isevars predcclj).uj_val in      
@@ -1701,9 +1631,6 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
   let tmsign = List.map snd tomatchl in
   let pred = prepare_predicate loc typing_fun isevars env tomatchs tmsign tycon predopt in
     
-  (* We deal with initial aliases *)
-  let matx = prepare_initial_aliases (known_dependent pred) tomatchs matx in 
-    
   (* We push the initial terms to match and push their alias to rhs' envs *)
   (* names of aliases will be recovered from patterns (hence Anonymous here) *)
   let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 5919c42a..9e902126 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cases.mli 8654 2006-03-22 15:36:58Z msozeau $ i*)
+(*i $Id: cases.mli 8741 2006-04-26 22:30:32Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -41,13 +41,9 @@ val error_wrong_numarg_inductive_loc : loc -> env -> inductive -> int -> 'a
 module type S = sig
   val compile_cases :
     loc ->
-    (type_constraint -> env -> rawconstr -> unsafe_judgment) *    
-      evar_defs ref ->
+    (type_constraint -> env -> rawconstr -> unsafe_judgment) * evar_defs ref ->
     type_constraint -> 
-    env ->
-    rawconstr option *
-      (rawconstr * (name * (loc * inductive * name list) option)) list *
-      (loc * identifier list * cases_pattern list * rawconstr) list ->
+    env -> rawconstr option * tomatch_tuple * cases_clauses ->
     unsafe_judgment
 end
 
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 33166ba8..2a01e901 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cbv.ml 7639 2005-12-02 10:01:15Z gregoire $ *)
+(* $Id: cbv.ml 8802 2006-05-10 20:47:28Z barras $ *)
 
 open Util
 open Pp
@@ -45,10 +45,10 @@ open Esubst
  *)
 type cbv_value =
   | VAL of int * constr
-  | LAM of name * constr * constr * cbv_value subs
-  | FIXP of fixpoint * cbv_value subs * cbv_value list
-  | COFIXP of cofixpoint * cbv_value subs * cbv_value list
-  | CONSTR of constructor * cbv_value list
+  | LAM of int * (name * constr) list * constr * cbv_value subs
+  | FIXP of fixpoint * cbv_value subs * cbv_value array
+  | COFIXP of cofixpoint * cbv_value subs * cbv_value array
+  | CONSTR of constructor * cbv_value array
 
 (* les vars pourraient etre des constr,
    cela permet de retarder les lift: utile ?? *) 
@@ -58,14 +58,15 @@ type cbv_value =
  *)
 let rec shift_value n = function
   | VAL (k,v) -> VAL ((k+n),v)
-  | LAM (x,a,b,s) -> LAM (x,a,b,subs_shft (n,s))
+  | LAM (nlams,ctxt,b,s) -> LAM (nlams,ctxt,b,subs_shft (n,s))
   | FIXP (fix,s,args) ->
-      FIXP (fix,subs_shft (n,s), List.map (shift_value n) args)
+      FIXP (fix,subs_shft (n,s), Array.map (shift_value n) args)
   | COFIXP (cofix,s,args) ->
-      COFIXP (cofix,subs_shft (n,s), List.map (shift_value n) args)
+      COFIXP (cofix,subs_shft (n,s), Array.map (shift_value n) args)
   | CONSTR (c,args) ->
-      CONSTR (c, List.map (shift_value n) args)
-	
+      CONSTR (c, Array.map (shift_value n) args)
+let shift_value n v =
+  if n = 0 then v else shift_value n v
 
 (* Contracts a fixpoint: given a fixpoint and a bindings,
  * returns the corresponding fixpoint body, and the bindings in which
@@ -74,22 +75,14 @@ let rec shift_value n = function
  *    -> (S. [S]F0 . [S]F1 ... . [S]Fn-1, Ti)
  *)
 let contract_fixp env ((reci,i),(_,_,bds as bodies)) =
-  let make_body j = FIXP(((reci,j),bodies), env, []) in
+  let make_body j = FIXP(((reci,j),bodies), env, [||]) in
   let n = Array.length bds in
-  let rec subst_bodies_from_i i subs =
-    if i=n then subs
-    else subst_bodies_from_i (i+1) (subs_cons (make_body i, subs))
-  in       
-  subst_bodies_from_i 0 env, bds.(i)
+  subs_cons(Array.init n make_body, env), bds.(i)
 
 let contract_cofixp env (i,(_,_,bds as bodies)) =
-  let make_body j = COFIXP((j,bodies), env, []) in
+  let make_body j = COFIXP((j,bodies), env, [||]) in
   let n = Array.length bds in
-  let rec subst_bodies_from_i i subs =
-    if i=n then subs
-    else subst_bodies_from_i (i+1) (subs_cons (make_body i, subs))
-  in       
-  subst_bodies_from_i 0 env, bds.(i)
+  subs_cons(Array.init n make_body, env), bds.(i)
 
 let make_constr_ref n = function
   | RelKey p -> mkRel (n+p)
@@ -99,9 +92,11 @@ let make_constr_ref n = function
 
 (* type of terms with a hole. This hole can appear only under App or Case.
  *   TOP means the term is considered without context
- *   APP(l,stk) means the term is applied to l, and then we have the context st
+ *   APP(v,stk) means the term is applied to v, and then the context stk
+ *      (v.0 is the first argument).
  *      this corresponds to the application stack of the KAM.
- *      The members of l are values: we evaluate arguments before the function.
+ *      The members of l are values: we evaluate arguments before
+        calling the function.
  *   CASE(t,br,pat,S,stk) means the term is in a case (which is himself in stk
  *      t is the type of the case and br are the branches, all of them under
  *      the subs S, pat is information on the patterns of the Case
@@ -114,15 +109,15 @@ let make_constr_ref n = function
 
 type cbv_stack =
   | TOP
-  | APP of cbv_value list * cbv_stack
+  | APP of cbv_value array * cbv_stack
   | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
 
 (* Adds an application list. Collapse APPs! *)
 let stack_app appl stack =
-  match (appl, stack) with
-    | ([], _)            -> stack
-    | (_, APP(args,stk)) -> APP(appl@args,stk)
-    | _                  -> APP(appl, stack)
+  if Array.length appl = 0 then stack else
+    match stack with
+    | APP(args,stk) -> APP(Array.append appl args,stk)
+    | _             -> APP(appl, stack)
 
 
 open RedFlags
@@ -137,23 +132,21 @@ let red_set_ref flags = function
  *)
 let strip_appl head stack =
   match head with
-    | FIXP (fix,env,app) -> (FIXP(fix,env,[]), stack_app app stack)
-    | COFIXP (cofix,env,app) -> (COFIXP(cofix,env,[]), stack_app app stack)
-    | CONSTR (c,app) -> (CONSTR(c,[]), stack_app app stack)
+    | FIXP (fix,env,app) -> (FIXP(fix,env,[||]), stack_app app stack)
+    | COFIXP (cofix,env,app) -> (COFIXP(cofix,env,[||]), stack_app app stack)
+    | CONSTR (c,app) -> (CONSTR(c,[||]), stack_app app stack)
     | _ -> (head, stack)
 
 
-(* Tests if fixpoint reduction is possible. A reduction function is given as
-   argument *)
-let rec check_app_constr = function
-  | ([], _) -> false
-  | ((CONSTR _)::_, 0) -> true
-  | (_::l, n) -> check_app_constr (l,(pred n))
-	
+(* Tests if fixpoint reduction is possible. *)
 let fixp_reducible flgs ((reci,i),_) stk =
   if red_set flgs fIOTA then
-    match stk with               (* !!! for Acc_rec: reci.(i) = -2 *)
-      | APP(appl,_) -> reci.(i) >=0 & check_app_constr (appl, reci.(i))
+    match stk with
+      | APP(appl,_) ->
+          Array.length appl > reci.(i) &&
+          (match appl.(reci.(i)) with
+              CONSTR _ -> true
+            | _ -> false)
       | _ -> false
   else 
     false
@@ -166,6 +159,7 @@ let cofixp_reducible flgs _ stk =
   else 
     false
 
+
 (* The main recursive functions
  *
  * Go under applications and cases (pushed in the stack), expand head
@@ -184,7 +178,7 @@ let rec norm_head info env t stack =
   | App (head,args) -> (* Applied terms are normalized immediately;
                         they could be computed when getting out of the stack *)
       let nargs = Array.map (cbv_stack_term info TOP env) args in
-      norm_head info env head (stack_app (Array.to_list nargs) stack)
+      norm_head info env head (stack_app nargs stack)
   | Case (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack))
   | Cast (ct,_,_) -> norm_head info env ct stack
 
@@ -212,7 +206,7 @@ let rec norm_head info env t stack =
           or red_set (info_flags info) fDELTA
           *)
         then 
-	  subs_cons (cbv_stack_term info TOP env b,env)
+	  subs_cons ([|cbv_stack_term info TOP env b|],env)
 	else
 	  subs_lift env in
       if zeta then
@@ -225,10 +219,12 @@ let rec norm_head info env t stack =
 	(VAL(0,normt), stack) (* Considérer une coupure commutative ? *)
 
   (* non-neutral cases *)
-  | Lambda (x,a,b) -> (LAM(x,a,b,env), stack)
-  | Fix fix -> (FIXP(fix,env,[]), stack)
-  | CoFix cofix -> (COFIXP(cofix,env,[]), stack)
-  | Construct c -> (CONSTR(c, []), stack)
+  | Lambda _ ->
+      let ctxt,b = decompose_lam t in
+      (LAM(List.length ctxt, List.rev ctxt,b,env), stack)
+  | Fix fix -> (FIXP(fix,env,[||]), stack)
+  | CoFix cofix -> (COFIXP(cofix,env,[||]), stack)
+  | Construct c -> (CONSTR(c, [||]), stack)
 
   (* neutral cases *)
   | (Sort _ | Meta _ | Ind _|Evar _) -> (VAL(0, t), stack)
@@ -253,10 +249,18 @@ and norm_head_ref k info env stack normt =
 and cbv_stack_term info stack env t =
   match norm_head info env t stack with
     (* a lambda meets an application -> BETA *)
-    | (LAM (x,a,b,env), APP (arg::args, stk))
+    | (LAM (nlams,ctxt,b,env), APP (args, stk))
       when red_set (info_flags info) fBETA ->
-        let subs = subs_cons (arg,env) in
-          cbv_stack_term info (stack_app args stk) subs b
+        let nargs = Array.length args in
+        if nargs == nlams then
+          cbv_stack_term info stk (subs_cons(args,env)) b
+        else if nlams < nargs then
+          let env' = subs_cons(Array.sub args 0 nlams, env) in
+          let eargs = Array.sub args nlams (nargs-nlams) in
+          cbv_stack_term info (APP(eargs,stk)) env' b
+        else
+          let ctxt' = list_skipn nargs ctxt in
+          LAM(nlams-nargs,ctxt', b, subs_cons(args,env))
 
     (* a Fix applied enough -> IOTA *)
     | (FIXP(fix,env,_), stk)
@@ -273,8 +277,9 @@ and cbv_stack_term info stack env t =
     (* constructor in a Case -> IOTA *)
     | (CONSTR((sp,n),_), APP(args,CASE(_,br,ci,env,stk)))
             when red_set (info_flags info) fIOTA ->
-	let real_args = list_skipn ci.ci_npar args in
-        cbv_stack_term info (stack_app real_args stk) env br.(n-1)
+	let cargs =
+          Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in
+        cbv_stack_term info (stack_app cargs stk) env br.(n-1)
          
     (* constructor of arity 0 in a Case -> IOTA *)
     | (CONSTR((_,n),_), CASE(_,br,_,env,stk))
@@ -287,6 +292,9 @@ and cbv_stack_term info stack env t =
     | (COFIXP(cofix,env,_), APP(appl,TOP)) -> COFIXP(cofix,env,appl) 
     | (CONSTR(c,_), APP(appl,TOP)) -> CONSTR(c,appl)
 
+    (* absurd cases (ill-typed) *)
+    | (LAM _, CASE _) -> assert false
+
     (* definitely a value *)
     | (head,stk) -> VAL(0,apply_stack info (cbv_norm_value info head) stk)
 
@@ -298,7 +306,7 @@ and cbv_stack_term info stack env t =
 and apply_stack info t = function
   | TOP -> t
   | APP (args,st) ->
-      apply_stack info (applistc t (List.map (cbv_norm_value info) args)) st
+      apply_stack info (mkApp(t,Array.map (cbv_norm_value info) args)) st
   | CASE (ty,br,ci,env,st) ->
       apply_stack info
         (mkCase (ci, cbv_norm_term info env ty, t,
@@ -314,28 +322,28 @@ and cbv_norm_term info env t =
 (* reduction of a cbv_value to a constr *)
 and cbv_norm_value info = function (* reduction under binders *)
   | VAL (n,v) -> lift n v
-  | LAM (x,a,b,env) ->
-      mkLambda (x, cbv_norm_term info env a,
-		cbv_norm_term info (subs_lift env) b)
+  | LAM (n,ctxt,b,env) ->
+      let nctxt =
+        list_map_i (fun i (x,ty) ->
+          (x,cbv_norm_term info (subs_liftn i env) ty)) 0 ctxt in
+      compose_lam (List.rev nctxt) (cbv_norm_term info (subs_liftn n env) b)
   | FIXP ((lij,(names,lty,bds)),env,args) ->
-      applistc
+      mkApp
         (mkFix (lij,
 		(names,
                  Array.map (cbv_norm_term info env) lty,
 		 Array.map (cbv_norm_term info 
-			      (subs_liftn (Array.length lty) env)) bds)))
-        (List.map (cbv_norm_value info) args)
+			      (subs_liftn (Array.length lty) env)) bds)),
+         Array.map (cbv_norm_value info) args)
   | COFIXP ((j,(names,lty,bds)),env,args) ->
-      applistc
+      mkApp
         (mkCoFix (j,
 		  (names,Array.map (cbv_norm_term info env) lty,
 		   Array.map (cbv_norm_term info 
-				(subs_liftn (Array.length lty) env)) bds)))
-        (List.map (cbv_norm_value info) args)
+				(subs_liftn (Array.length lty) env)) bds)),
+         Array.map (cbv_norm_value info) args)
   | CONSTR (c,args) ->
-      applistc
-        (mkConstruct c)
-        (List.map (cbv_norm_value info) args)
+      mkApp(mkConstruct c, Array.map (cbv_norm_value info) args)
 
 (* with profiling *)
 let cbv_norm infos constr =
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index dfdf12dd..8c969e2c 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cbv.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: cbv.mli 8799 2006-05-09 21:15:07Z barras $ i*)
 
 (*i*)
 open Names
@@ -29,19 +29,19 @@ val cbv_norm         : cbv_infos -> constr -> constr
 (*i This is for cbv debug *)
 type cbv_value =
   | VAL of int * constr
-  | LAM of name * constr * constr * cbv_value subs
-  | FIXP of fixpoint * cbv_value subs * cbv_value list
-  | COFIXP of cofixpoint * cbv_value subs * cbv_value list
-  | CONSTR of constructor * cbv_value list
+  | LAM of int * (name * constr) list * constr * cbv_value subs
+  | FIXP of fixpoint * cbv_value subs * cbv_value array
+  | COFIXP of cofixpoint * cbv_value subs * cbv_value array
+  | CONSTR of constructor * cbv_value array
 
 val shift_value : int -> cbv_value -> cbv_value
 
 type cbv_stack =
   | TOP
-  | APP of cbv_value list * cbv_stack
+  | APP of cbv_value array * cbv_stack
   | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
 
-val stack_app : cbv_value list -> cbv_stack -> cbv_stack
+val stack_app : cbv_value array -> cbv_stack -> cbv_stack
 val strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack
 
 (* recursive functions... *)
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 0b88b14b..6113ec2d 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: clenv.ml 8688 2006-04-07 15:08:12Z msozeau $ *)
+(* $Id: clenv.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
 
 open Pp
 open Util
@@ -84,10 +84,10 @@ let clenv_environments evd bound c =
 	  let dep = dependent (mkRel 1) c2 in
 	  let na' = if dep then na else Anonymous in
 	  let e' = meta_declare mv c1 ~name:na' e in
-	  clrec (e', (mkMeta mv)::metas) (option_app ((+) (-1)) n)
+	  clrec (e', (mkMeta mv)::metas) (option_map ((+) (-1)) n)
 	    (if dep then (subst1 (mkMeta mv) c2) else c2)
       | (n, LetIn (na,b,_,c)) ->
-	  clrec (e,metas) (option_app ((+) (-1)) n) (subst1 b c)
+	  clrec (e,metas) (option_map ((+) (-1)) n) (subst1 b c)
       | (n, _) -> (e, List.rev metas, c)
   in 
   clrec (evd,[]) bound c
@@ -100,10 +100,10 @@ let clenv_environments_evars env evd bound c =
       | (n, Prod (na,c1,c2)) ->
           let e',constr = Evarutil.new_evar e env c1 in
 	  let dep = dependent (mkRel 1) c2 in
-	  clrec (e', constr::ts) (option_app ((+) (-1)) n)
+	  clrec (e', constr::ts) (option_map ((+) (-1)) n)
 	    (if dep then (subst1 constr c2) else c2)
       | (n, LetIn (na,b,_,c)) ->
-	  clrec (e,ts) (option_app ((+) (-1)) n) (subst1 b c)
+	  clrec (e,ts) (option_map ((+) (-1)) n) (subst1 b c)
       | (n, _) -> (e, List.rev ts, c)
   in 
   clrec (evd,[]) bound c
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index e01dac47..d0ee913f 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: coercion.ml 8695 2006-04-10 16:33:52Z msozeau $ *)
+(* $Id: coercion.ml 8875 2006-05-29 19:59:11Z msozeau $ *)
 
 open Util
 open Names
@@ -35,6 +35,12 @@ module type S = sig
      type a sort; it fails if no coercion is applicable *)
   val inh_coerce_to_sort : loc ->
     env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment
+
+  (* [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
+     inserts a coercion into [j], if needed, in such a way it gets as
+     type its base type (the notion depends on the coercion system) *)
+  val inh_coerce_to_base : loc ->
+    env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
     
   (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type 
      [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
@@ -143,6 +149,8 @@ module Default = struct
 	| _ ->
 	    inh_tosort_force loc env isevars j
 
+  let inh_coerce_to_base loc env isevars j = (isevars, j)
+
   let inh_coerce_to_fail env isevars c1 v t =
     let v', t' =
       try 
@@ -168,7 +176,7 @@ module Default = struct
 	   (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
 	      kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with
 		| Prod (_,t1,t2), Prod (name,u1,u2) -> 
-		    let v' = option_app (whd_betadeltaiota env (evars_of isevars)) v in
+		    let v' = option_map (whd_betadeltaiota env (evars_of isevars)) v in
 		    let (evd',b) =
 		      match v' with 
 			  Some v' ->
@@ -184,7 +192,7 @@ module Default = struct
 			     let env1 = push_rel (x,None,v1) env in
 			     let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd'
 						       (Some v2) t2 u2 in
-			       (evd'', option_app (fun v2' -> mkLambda (x, v1, v2')) v2', 
+			       (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2', 
 				mkProd (x, v1, t2'))
 			 | None ->
 			     (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
@@ -201,7 +209,7 @@ module Default = struct
 			     let (evd'', v2', t2') = 
 			       let v2 =
 				 match v with 
-				     Some v -> option_app (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1'
+				     Some v -> option_map (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1'
 				   | None -> None
 			       and evd', t2 =
 				 match v1' with 
@@ -212,7 +220,7 @@ module Default = struct
 			       in
 				 inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
 			     in
-			       (evd'', option_app (fun v2' -> mkLambda (name, u1, v2')) v2',
+			       (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2',
 				mkProd (name, u1, t2')))
 		| _ -> raise NoCoercion))
 	
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index f675beff..42ce27fd 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coercion.mli 8688 2006-04-07 15:08:12Z msozeau $ i*)
+(*i $Id: coercion.mli 8875 2006-05-29 19:59:11Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -33,13 +33,19 @@ module type S = sig
      type a sort; it fails if no coercion is applicable *)
   val inh_coerce_to_sort : loc ->
     env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment
+
+  (* [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
+     inserts a coercion into [j], if needed, in such a way it gets as
+     type its base type (the notion depends on the coercion system) *)
+  val inh_coerce_to_base : loc ->
+    env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
     
   (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type 
      [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
      [j.uj_type] are convertible; it fails if no coercion is applicable *)
   val inh_conv_coerce_to : loc -> 
     env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment
-
+    
   (* [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
      is coercible to an object of type [t'] adding evar constraints if needed;
      it fails if no coercion exists *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 3f2aed34..7a170bcf 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: detyping.ml 8624 2006-03-13 17:38:17Z msozeau $ *)
+(* $Id: detyping.ml 8875 2006-05-29 19:59:11Z msozeau $ *)
 
 open Pp
 open Util
@@ -277,6 +277,25 @@ let extract_nondep_branches test c b n =
       | _ -> assert false in
   if test c n then Some (strip n b) else None
 
+let it_destRLambda_or_LetIn_names n c =
+  let rec aux n nal c =
+    if n=0 then (List.rev nal,c) else match c with
+      | RLambda (_,na,_,c) -> aux (n-1) (na::nal) c
+      | RLetIn (_,na,_,c) -> aux (n-1) (na::nal) c
+      | _ ->
+          (* eta-expansion *)
+	  let rec next l =
+	    let x = Nameops.next_ident_away (id_of_string "x") l in
+	    (* Not efficient but unusual and no function to get free rawvars *)
+	    if occur_rawconstr x c then next (x::l) else x in
+	  let x = next [] in 
+	  let a = RVar (dl,x) in
+	  aux (n-1) (Name x :: nal) 
+            (match c with
+              | RApp (loc,p,l) -> RApp (loc,c,l@[a])
+              | _ -> (RApp (dl,c,[a])))
+  in aux n [] c
+
 let detype_case computable detype detype_eqns testdep avoid data p c bl =
   let (indsp,st,nparams,consnargsl,k) = data in
   let synth_type = synthetize_type () in
@@ -286,32 +305,16 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
     then 
       Anonymous, None, None
     else
-      match option_app detype p with
+      match option_map detype p with
         | None -> Anonymous, None, None
         | Some p ->
-            let decompose_lam k c =
-              let rec lamdec_rec l avoid k c =
-                if k = 0 then List.rev l,c else match c with
-                  | RLambda (_,x,t,c) -> 
-                      lamdec_rec (x::l) (name_cons x avoid) (k-1) c
-                  | c -> 
-                      let x = next_ident_away (id_of_string "x") avoid in
-                      lamdec_rec ((Name x)::l) (x::avoid) (k-1)
-                        (let a = RVar (dl,x) in
-                          match c with
-                          | RApp (loc,p,l) -> RApp (loc,p,l@[a])
-                          | _ -> (RApp (dl,c,[a])))
-              in 
-              lamdec_rec [] [] k c in
-            let nl,typ = decompose_lam k p in
+            let nl,typ = it_destRLambda_or_LetIn_names k p in
 	    let n,typ = match typ with 
               | RLambda (_,x,t,c) -> x, c
 	      | _ -> Anonymous, typ in
 	    let aliastyp =
 	      if List.for_all ((=) Anonymous) nl then None
-	      else 
-		let pars = list_tabulate (fun _ -> Anonymous) nparams in
-		Some (dl,indsp,pars@nl) in
+	      else Some (dl,indsp,nparams,nl) in
             n, aliastyp, Some typ
   in
   let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
@@ -331,22 +334,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
   match tag with
   | LetStyle when aliastyp = None -> 
       let bl' = Array.map detype bl in
-      let rec decomp_lam_force n avoid l p =
-	if n = 0 then (List.rev l,p) else
-          match p with
-            | RLambda (_,na,_,c) -> 
-		decomp_lam_force (n-1) (name_cons na avoid) (na::l) c
-            | RLetIn (_,na,_,c) -> 
-		decomp_lam_force (n-1) (name_cons na avoid) (na::l) c
-            | _ ->
-		let x = Nameops.next_ident_away (id_of_string "x") avoid in
-		decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
-                  (* eta-expansion *)
-                  (let a = RVar (dl,x) in
-                  match p with
-                    | RApp (loc,p,l) -> RApp (loc,p,l@[a])
-                    | _ -> (RApp (dl,p,[a]))) in
-      let (nal,d) = decomp_lam_force consnargsl.(0) avoid [] bl'.(0) in
+      let (nal,d) = it_destRLambda_or_LetIn_names consnargsl.(0) bl'.(0) in
       RLetTuple (dl,nal,(alias,pred),tomatch,d)
   | IfStyle when aliastyp = None ->
       let bl' = Array.map detype bl in
@@ -360,6 +348,10 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
   | _ ->
       RCases (dl,pred,[tomatch,(alias,aliastyp)],eqnl)
 
+let detype_sort = function
+  | Prop c -> RProp c
+  | Type u -> RType (Some u)
+
 (**********************************************************************)
 (* Main detyping function                                             *)
 
@@ -380,10 +372,9 @@ let rec detype isgoal avoid env t =
 	  let _ = Global.lookup_named id in RRef (dl, VarRef id)
 	 with _ ->
 	  RVar (dl, id))
-    | Sort (Prop c) -> RSort (dl,RProp c)
-    | Sort (Type u) -> RSort (dl,RType (Some u))
+    | Sort s -> RSort (dl,detype_sort s)
     | Cast (c1,k,c2) ->
-	RCast(dl,detype isgoal avoid env c1, k,
+	RCast(dl,detype isgoal avoid env c1, CastConv k,
               detype isgoal avoid env c2)
     | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c
     | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c
@@ -421,7 +412,7 @@ and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) =
   let v = array_map3
     (fun c t i -> share_names isgoal (i+1) [] def_avoid def_env c (lift n t))
     bodies tys vn in
-  RRec(dl,RFix (Array.map (fun i -> i, RStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
+  RRec(dl,RFix (Array.map (fun i -> Some i, RStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
@@ -587,9 +578,9 @@ let rec subst_rawconstr subst raw =
         let a' = subst_rawconstr subst a in
         let (n,topt) = x in 
         let topt' = option_smartmap
-          (fun (loc,(sp,i),x as t) ->
+          (fun (loc,(sp,i),x,y as t) ->
             let sp' = subst_kn subst sp in
-            if sp == sp' then t else (loc,(sp',i),x)) topt in
+            if sp == sp' then t else (loc,(sp',i),x,y)) topt in
         if a == a' && topt == topt' then y else (a',(n,topt'))) rl
       and branches' = list_smartmap 
 			(fun (loc,idl,cpl,r as branch) ->
@@ -645,3 +636,18 @@ let rec subst_rawconstr subst raw =
 	  RCast (loc,r1',k,r2')
 
   | RDynamic _ -> raw
+
+(* Utilities to transform kernel cases to simple pattern-matching problem *)
+
+let simple_cases_matrix_of_branches ind brns brs =
+  list_map2_i (fun i n b ->
+      let nal,c = it_destRLambda_or_LetIn_names n b in
+      let mkPatVar na = PatVar (dummy_loc,na) in
+      let p = PatCstr (dummy_loc,(ind,i+1),List.map mkPatVar nal,Anonymous) in
+      let ids = map_succeed Nameops.out_name nal in
+      (dummy_loc,ids,[p],c))
+    0 brns brs
+
+let return_type_of_predicate ind nparams n pred =
+  let nal,p = it_destRLambda_or_LetIn_names (n+1) pred in
+  (List.hd nal, Some (dummy_loc, ind, nparams, List.tl nal)), Some p
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 0b35728c..bbe2fcc9 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: detyping.mli 7881 2006-01-16 14:03:05Z herbelin $ i*)
+(*i $Id: detyping.mli 8831 2006-05-19 09:29:54Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -38,6 +38,8 @@ val detype_case :
   identifier list -> inductive * case_style * int * int array * int ->
     'a option -> 'a -> 'a array -> rawconstr
 
+val detype_sort : sorts -> rawsort
+
 (* look for the index of a named var or a nondep var as it is renamed *)
 val lookup_name_as_renamed  : env -> constr -> identifier -> int option
 val lookup_index_as_renamed : env -> constr -> int -> int option
@@ -47,3 +49,12 @@ val force_wildcard : unit -> bool
 val synthetize_type : unit -> bool
 val force_if : case_info -> bool
 val force_let : case_info -> bool
+
+(* Utilities to transform kernel cases to simple pattern-matching problem *)
+
+val it_destRLambda_or_LetIn_names : int -> rawconstr -> name list * rawconstr
+val simple_cases_matrix_of_branches : 
+  inductive -> int list -> rawconstr list -> cases_clauses
+val return_type_of_predicate :
+  inductive -> int -> int -> rawconstr -> predicate_pattern * rawconstr option
+
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 2b04b693..458f5bd3 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,14 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarconv.ml 8111 2006-03-02 17:23:41Z herbelin $ *)
+(* $Id: evarconv.ml 8793 2006-05-05 17:41:41Z barras $ *)
 
 open Util
 open Names
 open Term
+open Closure
 open Reduction
 open Reductionops
-open Closure
 open Environ
 open Typing
 open Classops
@@ -41,7 +41,7 @@ let eval_flexible_term env c =
   match kind_of_term c with
   | Const c -> constant_opt_value env c
   | Rel n ->
-      (try let (_,v,_) = lookup_rel n env in option_app (lift n) v
+      (try let (_,v,_) = lookup_rel n env in option_map (lift n) v
       with Not_found -> None)
   | Var id ->
       (try let (_,v,_) = lookup_named id env in v with Not_found -> None)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index aeaaefef..506cd03f 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarutil.ml 8695 2006-04-10 16:33:52Z msozeau $ *)
+(* $Id: evarutil.ml 8759 2006-04-28 12:24:14Z herbelin $ *)
 
 open Util
 open Pp
@@ -35,7 +35,7 @@ exception Uninstantiated_evar of existential_key
 
 let rec whd_ise sigma c =
   match kind_of_term c with
-    | Evar (ev,args) when Evd.in_dom sigma ev ->
+    | Evar (ev,args) when Evd.mem sigma ev ->
 	if Evd.is_defined sigma ev then
           whd_ise sigma (existential_value sigma (ev,args))
 	else raise (Uninstantiated_evar ev)
@@ -46,7 +46,7 @@ let rec whd_ise sigma c =
 let whd_castappevar_stack sigma c = 
   let rec whrec (c, l as s) =
     match kind_of_term c with
-      | Evar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> 
+      | Evar (ev,args) when Evd.mem sigma ev & Evd.is_defined sigma ev -> 
 	  whrec (existential_value sigma (ev,args), l)
       | Cast (c,_,_) -> whrec (c, l)
       | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
@@ -93,7 +93,7 @@ let collect_evars emap c =
   let rec collrec acc c =
     match kind_of_term c with
       | Evar (k,_) ->
-	  if Evd.in_dom emap k & not (Evd.is_defined emap k) then k::acc
+	  if Evd.mem emap k & not (Evd.is_defined emap k) then k::acc
 	  else (* No recursion on the evar instantiation *) acc
       | _         ->
 	  fold_constr collrec acc c in
@@ -103,13 +103,14 @@ let push_dependent_evars sigma emap =
   Evd.fold (fun ev {evar_concl = ccl} (sigma',emap') ->
     List.fold_left 
       (fun (sigma',emap') ev -> 
-	(Evd.add sigma' ev (Evd.map emap' ev),Evd.rmv emap' ev))
+	(Evd.add sigma' ev (Evd.find emap' ev),Evd.remove emap' ev))
       (sigma',emap') (collect_evars emap' ccl))
     emap (sigma,emap)
     
 (* replaces a mapping of existentials into a mapping of metas.
    Problem if an evar appears in the type of another one (pops anomaly) *)
 let evars_to_metas sigma (emap, c) =
+  let emap = nf_evars emap in
   let sigma',emap' = push_dependent_evars sigma emap in
   let change_exist evar =
     let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in
@@ -117,7 +118,7 @@ let evars_to_metas sigma (emap, c) =
     mkCast (mkMeta n, DEFAULTcast, ty) in
   let rec replace c =
     match kind_of_term c with
-        Evar (k,_ as ev) when Evd.in_dom emap' k -> change_exist ev
+        Evar (k,_ as ev) when Evd.mem emap' k -> change_exist ev
       | _ -> map_constr replace c in
   (sigma', replace c)
 
@@ -209,7 +210,7 @@ let push_rel_context_to_named_context env =
        let id = next_name_away na avoid in
        ((mkVar id)::subst,
         id::avoid,
-	push_named (id,option_app (substl subst) c,
+	push_named (id,option_map (substl subst) c,
                         type_app (substl subst) t)
 	  env))
     (rel_context env) ~init:([],ids_of_named_context (named_context env),env)
@@ -297,7 +298,7 @@ let is_defined_equation env evd (ev,inst) rhs =
   is_pattern inst &&
   not (occur_evar ev rhs) &&
   try
-    let evi = Evd.map (evars_of evd) ev in
+    let evi = Evd.find (evars_of evd) ev in
     let (evd',body) = inverse_instance env evd ev evi inst rhs in
     evar_well_typed_body evd' ev evi body
   with Failure _ -> false
@@ -313,7 +314,7 @@ let is_defined_equation env evd (ev,inst) rhs =
 
 let do_restrict_hyps evd ev args =
   let args = Array.to_list args in
-  let evi = Evd.map (evars_of !evd) ev in
+  let evi = Evd.find (evars_of !evd) ev in
   let env = evar_env evi in
   let hyps = evar_context evi in
   let (sign,ncargs) = list_filter2 (fun _ a -> closed0 a) (hyps,args) in
@@ -395,7 +396,7 @@ let evar_define env (ev,argsv) rhs isevars =
   if occur_evar ev rhs
   then error_occur_check env (evars_of isevars) ev rhs;
   let args = Array.to_list argsv in 
-  let evi = Evd.map (evars_of isevars) ev in
+  let evi = Evd.find (evars_of isevars) ev in
   (* the bindings to invert *)
   let worklist = make_subst (evar_env evi) args in
   let (isevars',body) = real_clean env isevars ev evi worklist rhs in
@@ -502,7 +503,7 @@ let status_changed lev (pbty,t1,t2) =
 
 let solve_refl conv_algo env isevars ev argsv1 argsv2 =
   if argsv1 = argsv2 then (isevars,[]) else
-  let evd = Evd.map (evars_of isevars) ev in
+  let evd = Evd.find (evars_of isevars) ev in
   let hyps = evar_context evd in
   let (isevars',_,rsign) = 
     array_fold_left2
@@ -599,7 +600,7 @@ let mk_valcon c = Some c
    cumulativity now includes Prop and Set in Type...
    It is, but that's not too bad *)
 let define_evar_as_abstraction abs evd (ev,args) =
-  let evi = Evd.map (evars_of evd) ev in
+  let evi = Evd.find (evars_of evd) ev in
   let evenv = evar_env evi in
   let (evd1,dom) = new_evar evd evenv (new_Type()) in
   let nvar =
@@ -679,7 +680,7 @@ let lift_abstr_tycon_type n (abs, t) =
 	  else (Some (init, abs'), t)
 
 let lift_tycon_type n (abs, t) = (abs, lift n t)
-let lift_tycon n = option_app (lift_tycon_type n)
+let lift_tycon n = option_map (lift_tycon_type n)
 
 let pr_tycon_type env (abs, t) =
   match abs with 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index c9f771c9..33f88ebd 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evd.ml 8688 2006-04-07 15:08:12Z msozeau $ *)
+(* $Id: evd.ml 8759 2006-04-28 12:24:14Z herbelin $ *)
 
 open Pp
 open Util
@@ -48,17 +48,16 @@ let empty = Evarmap.empty
 
 let to_list evc = Evarmap.fold (fun ev x acc -> (ev,x)::acc) evc []
 let dom evc = Evarmap.fold (fun ev _ acc -> ev::acc) evc []
-let map evc k = Evarmap.find k evc
-let rmv evc k = Evarmap.remove k evc
-let remap evc k i = Evarmap.add k i evc
-let in_dom evc k = Evarmap.mem k evc
+let find evc k = Evarmap.find k evc
+let remove evc k = Evarmap.remove k evc
+let mem evc k = Evarmap.mem k evc
 let fold = Evarmap.fold
 
 let add evd ev newinfo =  Evarmap.add ev newinfo evd
 
 let define evd ev body = 
   let oldinfo =
-    try map evd ev
+    try find evd ev
     with Not_found -> error "Evd.define: cannot define undeclared evar" in
   let newinfo =
     { evar_concl = oldinfo.evar_concl;
@@ -68,10 +67,10 @@ let define evd ev body =
     | Evar_empty -> Evarmap.add ev newinfo evd
     | _ -> anomaly "Evd.define: cannot define an isevar twice"
     
-let is_evar sigma ev = in_dom sigma ev
+let is_evar sigma ev = mem sigma ev
 
 let is_defined sigma ev =
-  let info = map sigma ev in 
+  let info = find sigma ev in 
   not (info.evar_body = Evar_empty)
 
 let evar_body ev = ev.evar_body
@@ -112,7 +111,7 @@ let instantiate_evar sign c args =
 
 let existential_type sigma (n,args) =
   let info =
-    try map sigma n
+    try find sigma n
     with Not_found ->
       anomaly ("Evar "^(string_of_existential n)^" was not declared") in
   let hyps = evar_context info in
@@ -121,7 +120,7 @@ let existential_type sigma (n,args) =
 exception NotInstantiatedEvar
 
 let existential_value sigma (n,args) =
-  let info = map sigma n in
+  let info = find sigma n in
   let hyps = evar_context info in
   match evar_body info with
     | Evar_defined c ->
@@ -270,10 +269,9 @@ type evar_map = evar_map1 * sort_constraints
 let empty = empty, UniverseMap.empty
 let add (sigma,sm) k v = (add sigma k v, sm)
 let dom (sigma,_) = dom sigma
-let map (sigma,_) = map sigma
-let rmv (sigma,sm) k = (rmv sigma k, sm)
-let remap (sigma,sm) k v = (remap sigma k v, sm)
-let in_dom (sigma,_) = in_dom sigma
+let find (sigma,_) = find sigma
+let remove (sigma,sm) k = (remove sigma k, sm)
+let mem (sigma,_) = mem sigma
 let to_list (sigma,_) = to_list sigma
 let fold f (sigma,_) = fold f sigma
 let define (sigma,sm) k v = (define sigma k v, sm)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 40ecce6e..cbc96b04 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evd.mli 8688 2006-04-07 15:08:12Z msozeau $ i*)
+(*i $Id: evd.mli 8759 2006-04-28 12:24:14Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -43,10 +43,9 @@ val empty : evar_map
 val add : evar_map -> evar -> evar_info -> evar_map
 
 val dom : evar_map -> evar list
-val map : evar_map -> evar -> evar_info
-val rmv : evar_map -> evar -> evar_map
-val remap : evar_map -> evar -> evar_info -> evar_map
-val in_dom : evar_map -> evar -> bool
+val find : evar_map -> evar -> evar_info
+val remove : evar_map -> evar -> evar_map
+val mem : evar_map -> evar -> bool
 val to_list : evar_map -> (evar * evar_info) list
 val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
 
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index a587dd20..07ca5d83 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indrec.ml 7662 2005-12-17 22:03:35Z herbelin $ *)
+(* $Id: indrec.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
 
 open Pp
 open Util
@@ -48,13 +48,13 @@ let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
    lift_constructor et lift_inductive_family qui ne se contentent pas de 
    lifter les paramètres globaux *)
 
-let mis_make_case_com depopt env sigma (ind,mib,mip) kind =
+let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
   let lnamespar = mib.mind_params_ctxt in
   let dep = match depopt with 
-    | None -> mip.mind_sort <> (Prop Null)
+    | None -> inductive_sort_family mip <> InProp
     | Some d -> d
   in
-  if not (List.exists ((=) kind) mip.mind_kelim) then
+  if not (List.mem kind (elim_sorts specif)) then
     raise
       (RecursionSchemeError
 	 (NotAllowedCaseAnalysis
@@ -431,7 +431,7 @@ let mis_make_indrec env sigma listdepkind mib =
       it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) 
 	lnamesparrec
     else 
-      mis_make_case_com (Some dep) env sigma (indi,mibi,mipi) kind 
+      mis_make_case_com (Some dep) env sigma indi (mibi,mipi) kind 
   in 
       (* Body of mis_make_indrec *)
   list_tabulate make_one_rec nrec
@@ -441,7 +441,7 @@ let mis_make_indrec env sigma listdepkind mib =
 
 let make_case_com depopt env sigma ity kind =
   let (mib,mip) = lookup_mind_specif env ity in 
-  mis_make_case_com depopt env sigma (ity,mib,mip) kind
+  mis_make_case_com depopt env sigma ity (mib,mip) kind
 
 let make_case_dep env   = make_case_com (Some true) env
 let make_case_nodep env = make_case_com (Some false) env 
@@ -504,7 +504,7 @@ let check_arities listdepkind =
   let _ = List.fold_left
     (fun ln ((_,ni),mibi,mipi,dep,kind) -> 
        let id = mipi.mind_typename  in
-       let kelim = mipi.mind_kelim in
+       let kelim = elim_sorts (mibi,mipi) in
        if not (List.exists ((=) kind) kelim) then raise
 	 (RecursionSchemeError (BadInduction (dep,id,new_sort_in_family kind)))
        else if List.mem ni ln then raise
@@ -534,7 +534,7 @@ let build_mutual_indrec env sigma = function
 
 let build_indrec env sigma ind =
   let (mib,mip) = lookup_mind_specif env ind in
-  let kind = family_of_sort mip.mind_sort in
+  let kind = inductive_sort_family mip in
   let dep = kind <> InProp in
   List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] mib)
 
@@ -596,7 +596,7 @@ let lookup_eliminator ind_sp s =
        pr_id id ++ spc () ++
        str "The elimination of the inductive definition " ++
        pr_id id ++ spc () ++ str "on sort " ++ 
-       spc () ++ print_sort_family s ++
+       spc () ++ pr_sort_family s ++
        str " is probably not allowed")
 
 
@@ -617,6 +617,6 @@ let lookup_eliminator ind_sp s =
            pr_id id ++ spc () ++
 	   str "The elimination of the inductive definition " ++
            pr_id base ++ spc () ++ str "on sort " ++ 
-           spc () ++ print_sort_family s ++
+           spc () ++ pr_sort_family s ++
 	   str " is probably not allowed")
 *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 57d966f1..e0cdeeee 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inductiveops.ml 8653 2006-03-22 09:41:17Z herbelin $ *)
+(* $Id: inductiveops.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
 
 open Util
 open Names
@@ -116,11 +116,15 @@ let constructor_nrealhyps env (ind,j) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   mip.mind_consnrealdecls.(j-1)
 
+let get_full_arity_sign env ind =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  mip.mind_arity_ctxt
+
 (* Length of arity (w/o local defs) *)
 
 let inductive_nargs env ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  mip.mind_nrealargs + rel_context_nhyps mib.mind_params_ctxt
+  mib.mind_nparams, mip.mind_nrealargs
 
 (* Annotation for cases *)
 let make_case_info env ind style pats_source =
@@ -196,10 +200,40 @@ let rec instantiate args c = match kind_of_term c, args with
   | _, [] -> c
   | _ -> anomaly "too short arity"
 
+(* substitution in a signature *)
+
+let substnl_rel_context subst n sign =
+  let rec aux n = function
+  | d::sign -> substnl_decl subst n d :: aux (n+1) sign
+  | [] -> []
+  in List.rev (aux n (List.rev sign))
+
+let substl_rel_context subst = substnl_rel_context subst 0
+
+let rec instantiate_context sign args =
+  let rec aux subst = function
+  | (_,None,_)::sign, a::args -> aux (a::subst) (sign,args)
+  | (_,Some b,_)::sign, args -> aux (substl subst b::subst) (sign,args)
+  | [], [] -> subst
+  | _ -> anomaly "Signature/instance mismatch in inductive family"
+  in aux [] (List.rev sign,args)
+
 let get_arity env (ind,params) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let arity = mip.mind_nf_arity in
-  destArity (instantiate params arity)
+  let parsign =
+    (* Dynamically detect if called with an instance of recursively
+       uniform parameter only or also of non recursively uniform
+       parameters *)
+    let parsign = mib.mind_params_ctxt in
+    let nnonrecparams = mib.mind_nparams - mib.mind_nparams_rec in
+    if List.length params = rel_context_nhyps parsign - nnonrecparams then
+      snd (list_chop nnonrecparams mib.mind_params_ctxt)
+    else
+      parsign in
+  let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in
+  let arsign,_ = list_chop arproperlength mip.mind_arity_ctxt in
+  let subst = instantiate_context parsign params in
+  (substl_rel_context subst arsign, Inductive.inductive_sort_family mip)
 
 (* Functions to build standard types related to inductive *)
 let build_dependent_constructor cs =
@@ -284,12 +318,12 @@ let find_coinductive env sigma c =
 (* find appropriate names for pattern variables. Useful in the Case
    and Inversion (case_then_using et case_nodep_then_using) tactics. *)
 
-let is_predicate_explicitly_dep env pred nodep_ar = 
-  let rec srec env pval nodep_ar =
+let is_predicate_explicitly_dep env pred arsign = 
+  let rec srec env pval arsign =
     let pv' = whd_betadeltaiota env Evd.empty pval in
-    match kind_of_term pv', kind_of_term nodep_ar with
-      | Lambda (na,t,b), Prod (_,_,a') ->
-	  srec (push_rel_assum (na,t) env) b a'
+    match kind_of_term pv', arsign with
+      | Lambda (na,t,b), (_,None,_)::arsign ->
+	  srec (push_rel_assum (na,t) env) b arsign
       | Lambda (na,_,_), _ ->
 
        (* The following code has impact on the introduction names
@@ -317,12 +351,11 @@ let is_predicate_explicitly_dep env pred nodep_ar =
 
       | _ -> anomaly "Non eta-expanded dep-expanded \"match\" predicate"
   in
-  srec env pred nodep_ar
+  srec env pred arsign
 
 let is_elim_predicate_explicitly_dependent env pred indf =
-  let arsign,s = get_arity env indf in
-  let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in
-  is_predicate_explicitly_dep env pred glob_t
+  let arsign,_ = get_arity env indf in
+  is_predicate_explicitly_dep env pred arsign
 
 let set_names env n brty =
   let (ctxt,cl) = decompose_prod_n_assum n brty in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 2993eed3..dcd86716 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -6,13 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: inductiveops.mli 7955 2006-01-30 22:56:15Z herbelin $ i*)
+(*i $Id: inductiveops.mli 8845 2006-05-23 07:41:58Z herbelin $ i*)
 
 open Names
 open Term
 open Declarations
 open Environ
 open Evd
+open Sign
 
 (* The following three functions are similar to the ones defined in
    Inductive, but they expect an env *)
@@ -42,8 +43,7 @@ val dest_ind_type : inductive_type -> inductive_family * constr list
 val map_inductive_type : (constr -> constr) -> inductive_type -> inductive_type
 val liftn_inductive_type : int -> int -> inductive_type -> inductive_type
 val lift_inductive_type  : int -> inductive_type -> inductive_type
-val substnl_ind_type :
-  constr list -> int -> inductive_type -> inductive_type
+val substnl_ind_type : constr list -> int -> inductive_type -> inductive_type
 
 val mkAppliedInd : inductive_type -> constr
 val mis_is_recursive_subset : int list -> wf_paths -> bool
@@ -51,16 +51,22 @@ val mis_is_recursive :
   inductive * mutual_inductive_body * one_inductive_body -> bool
 val mis_nf_constructor_type :
   inductive * mutual_inductive_body * one_inductive_body -> int -> constr
-val mis_constr_nargs : inductive -> int array
 
+(* Extract information from an inductive name *)
+
+val mis_constr_nargs : inductive -> int array
 val mis_constr_nargs_env : env -> inductive -> int array
 
-val mis_constructor_nargs_env : env -> constructor -> int
+(* Return number of expected parameters and of expected real arguments *)
+val inductive_nargs : env -> inductive -> int * int
 
+val mis_constructor_nargs_env : env -> constructor -> int
 val constructor_nrealargs : env -> constructor -> int
 val constructor_nrealhyps : env -> constructor -> int
 
-val inductive_nargs : env -> inductive -> int
+val get_full_arity_sign : env -> inductive -> rel_context
+
+(* Extract information from an inductive family *)
 
 type constructor_summary = {
   cs_cstr : constructor;
@@ -68,17 +74,16 @@ type constructor_summary = {
   cs_nargs : int;
   cs_args : Sign.rel_context;
   cs_concl_realargs : constr array;
-} 
+}
 val lift_constructor : int -> constructor_summary -> constructor_summary
 val get_constructor :
   inductive * mutual_inductive_body * one_inductive_body * constr list ->
   int -> constructor_summary
-val get_arity        : env -> inductive_family -> Sign.arity
+val get_arity        : env -> inductive_family -> rel_context * sorts_family
 val get_constructors : env -> inductive_family -> constructor_summary array
 val build_dependent_constructor : constructor_summary -> constr
 val build_dependent_inductive   : env -> inductive_family -> constr
-val make_arity_signature :
-  env -> bool -> inductive_family -> Sign.rel_context
+val make_arity_signature : env -> bool -> inductive_family -> Sign.rel_context
 val make_arity : env -> bool -> inductive_family -> sorts -> types
 val build_branch_type : env -> bool -> constr -> constructor_summary -> types
 
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 5ee245b5..12c1ea33 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: matching.ml 7970 2006-02-01 15:09:07Z herbelin $ *)
+(* $Id: matching.ml 8827 2006-05-17 15:15:34Z jforest $ *)
 
 (*i*)
 open Util
@@ -17,6 +17,7 @@ open Termops
 open Reductionops
 open Term
 open Rawterm
+open Sign
 open Environ
 open Pattern
 (*i*)
@@ -70,6 +71,11 @@ let memb_metavars m n =
 
 let eq_context ctxt1 ctxt2 = array_for_all2 eq_constr ctxt1 ctxt2
 
+let same_case_structure (_,cs1,ind,_) ci2 br1 br2 =
+  match ind with
+  | Some ind -> ind = ci2.ci_ind
+  | None -> cs1 = ci2.ci_cstr_nargs
+
 let matches_core convert allow_partial_app pat c = 
   let rec sorec stk sigma p t =
     let cT = strip_outer_cast t in
@@ -79,7 +85,7 @@ let matches_core convert allow_partial_app pat c =
 	    List.map
 	      (function
 		 | PRel n -> n
-		 | _ -> error "Only bound indices are currently allowed in second order pattern matching")
+		 | _ -> error "Only bound indices allowed in second order pattern matching")
 	      args in
 	  let frels = Intset.elements (free_rels cT) in
 	  if list_subset frels relargs then
@@ -150,15 +156,27 @@ let matches_core convert allow_partial_app pat c =
 	  if is_conv env evars c cT then sigma
 	  else raise PatternMatchingFailure
 
-      | PCase (_,_,a1,br1), Case (_,_,a2,br2) ->
-	  (* On ne teste pas le prédicat *)
-          if (Array.length br1) = (Array.length br2) then
-  	    array_fold_left2 (sorec stk) (sorec stk sigma a1 a2) br1 br2
+      | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
+	  let ctx,b2 = decompose_lam_n_assum ci.ci_cstr_nargs.(0) b2 in
+	  let ctx',b2' = decompose_lam_n_assum ci.ci_cstr_nargs.(1) b2' in
+	  let n = List.length ctx and n' = List.length ctx' in
+	  if noccur_between 1 n b2 & noccur_between 1 n' b2' then
+	    let s = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx in
+	    let s' = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx' in
+	    let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in
+  	    sorec s' (sorec s (sorec stk sigma a1 a2) b1 b2) b1' b2'
           else
             raise PatternMatchingFailure
-      (* À faire *)
-      |	PFix f0, Fix f1 when f0 = f1 -> sigma
-      |	PCoFix c0, CoFix c1 when c0 = c1 -> sigma
+
+      | PCase (ci1,p1,a1,br1), Case (ci2,p2,a2,br2) ->
+	  if same_case_structure ci1 ci2 br1 br2 then
+  	    array_fold_left2 (sorec stk) 
+	      (sorec stk (sorec stk sigma a1 a2) p1 p2) br1 br2
+          else
+            raise PatternMatchingFailure
+
+      |	PFix c1, Fix _ when eq_constr (mkFix c1) cT -> sigma
+      |	PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> sigma
       | _ -> raise PatternMatchingFailure
 
   in 
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 390b884c..ef97250a 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pattern.ml 7732 2005-12-26 13:51:24Z herbelin $ *)
+(* $Id: pattern.ml 8755 2006-04-27 22:22:15Z herbelin $ *)
 
 open Util
 open Names
@@ -38,8 +38,9 @@ type constr_pattern =
   | PLetIn of name * constr_pattern * constr_pattern
   | PSort of rawsort
   | PMeta of patvar option
-  | PCase of (inductive option * case_style)
-      * constr_pattern option * constr_pattern * constr_pattern array
+  | PIf of constr_pattern * constr_pattern * constr_pattern
+  | PCase of (case_style * int array * inductive option * (int * int) option)
+      * constr_pattern * constr_pattern * constr_pattern array
   | PFix of fixpoint
   | PCoFix of cofixpoint
 
@@ -49,9 +50,10 @@ let rec occur_meta_pattern = function
   | PLambda (na,t,c)  -> (occur_meta_pattern t) or (occur_meta_pattern c)
   | PProd (na,t,c)  -> (occur_meta_pattern t) or (occur_meta_pattern c)
   | PLetIn (na,t,c)  -> (occur_meta_pattern t) or (occur_meta_pattern c)
-  | PCase(_,None,c,br)   ->
-      (occur_meta_pattern c) or (array_exists occur_meta_pattern br)
-  | PCase(_,Some p,c,br) ->
+  | PIf (c,c1,c2)  ->
+      (occur_meta_pattern c) or
+      (occur_meta_pattern c1) or (occur_meta_pattern c2)
+  | PCase(_,p,c,br) ->
       (occur_meta_pattern p) or
       (occur_meta_pattern c) or (array_exists occur_meta_pattern br)
   | PMeta _ | PSoApp _ -> true
@@ -70,6 +72,7 @@ let rec head_pattern_bound t =
     | PProd (_,_,b)  -> head_pattern_bound b 
     | PLetIn (_,_,b) -> head_pattern_bound b 
     | PApp (c,args)  -> head_pattern_bound c
+    | PIf (c,_,_)  -> head_pattern_bound c
     | PCase (_,p,c,br) -> head_pattern_bound c
     | PRef r         -> r
     | PVar id        -> VarRef id
@@ -103,28 +106,43 @@ let rec pattern_of_constr t =
     | Construct sp -> PRef (ConstructRef sp)
     | Evar (n,ctxt) -> PEvar (n,Array.map pattern_of_constr ctxt)
     | Case (ci,p,a,br) ->
-	PCase ((Some ci.ci_ind,ci.ci_pp_info.style),
-	       Some (pattern_of_constr p),pattern_of_constr a,
+	let cip = ci.ci_pp_info in
+	let no = Some (ci.ci_npar,cip.ind_nargs) in
+	PCase ((cip.style,ci.ci_cstr_nargs,Some ci.ci_ind,no),
+	       pattern_of_constr p,pattern_of_constr a,
 	       Array.map pattern_of_constr br)
     | Fix f -> PFix f
     | CoFix f -> PCoFix f
 
 (* To process patterns, we need a translation without typing at all. *)
 
-let rec inst lvar = function
-  | PVar id as x -> (try List.assoc id lvar with Not_found -> x)
-  | PApp (p,pl) -> PApp (inst lvar p, Array.map (inst lvar) pl)
-  | PSoApp (n,pl) -> PSoApp (n, List.map (inst lvar) pl)
-  | PLambda (n,a,b) -> PLambda (n,inst lvar a,inst lvar b)
-  | PProd (n,a,b) -> PProd (n,inst lvar a,inst lvar b)
-  | PLetIn (n,a,b) -> PLetIn (n,inst lvar a,inst lvar b)
-  | PCase (ci,po,p,pl) ->
-      PCase (ci,option_app (inst lvar) po,inst lvar p,Array.map (inst lvar) pl)
+let map_pattern_with_binders g f l = function
+  | PApp (p,pl) -> PApp (f l p, Array.map (f l) pl)
+  | PSoApp (n,pl) -> PSoApp (n, List.map (f l) pl)
+  | PLambda (n,a,b) -> PLambda (n,f l a,f (g l) b)
+  | PProd (n,a,b) -> PProd (n,f l a,f (g l) b)
+  | PLetIn (n,a,b) -> PLetIn (n,f l a,f (g l) b)
+  | PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2)
+  | PCase (ci,po,p,pl) -> PCase (ci,f l po,f l p,Array.map (f l) pl)
   (* Non recursive *)
-  | (PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _ as x) -> x 
+  | (PVar _ | PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _
   (* Bound to terms *)
-  | (PFix _ | PCoFix _) ->
-      error ("Not instantiable pattern")
+  | PFix _ | PCoFix _ as x) -> x
+
+let map_pattern f = map_pattern_with_binders (fun () -> ()) (fun () -> f) ()
+
+let rec instantiate_pattern lvar = function
+  | PVar id as x -> (try List.assoc id lvar with Not_found -> x)
+  | (PFix _ | PCoFix _) -> error ("Not instantiable pattern")
+  | c -> map_pattern (instantiate_pattern lvar) c
+
+let rec liftn_pattern k n = function
+  | PRel i as x -> if i >= n then PRel (i+k) else x
+  | PFix x -> PFix (destFix (liftn k n (mkFix x)))
+  | PCoFix x -> PCoFix (destCoFix (liftn k n (mkCoFix x)))
+  | c -> map_pattern_with_binders succ (liftn_pattern k) n c
+
+let lift_pattern k = liftn_pattern k 1
 
 let rec subst_pattern subst pat = match pat with
   | PRef ref ->
@@ -160,12 +178,20 @@ let rec subst_pattern subst pat = match pat with
 	  PLetIn (name,c1',c2')
   | PSort _ 
   | PMeta _ -> pat
-  | PCase (cs,typ, c, branches) -> 
-      let typ' = option_smartmap (subst_pattern subst) typ in 
+  | PIf (c,c1,c2) ->
+      let c' = subst_pattern subst c in
+      let c1' = subst_pattern subst c1 in
+      let c2' = subst_pattern subst c2 in
+	if c' == c && c1' == c1 && c2' == c2 then pat else
+	  PIf (c',c1',c2')
+  | PCase ((a,b,ind,n as cs),typ,c,branches) ->
+      let ind' = option_smartmap (Inductiveops.subst_inductive subst) ind in
+      let typ' = subst_pattern subst typ in 
       let c' = subst_pattern subst c in
       let branches' = array_smartmap (subst_pattern subst) branches in
+      let cs' = if ind == ind' then cs else (a,b,ind',n) in
 	if typ' == typ && c' == c && branches' == branches then pat else
-	  PCase(cs,typ', c', branches') 
+	  PCase(cs',typ', c', branches') 
   | PFix fixpoint ->
       let cstr = mkFix fixpoint in
       let fixpoint' = destFix (subst_mps subst cstr) in
@@ -177,8 +203,8 @@ let rec subst_pattern subst pat = match pat with
 	if cofixpoint' == cofixpoint then pat else
 	  PCoFix cofixpoint'
 
-
-let instantiate_pattern = inst
+let mkPLambda na b = PLambda(na,PMeta None,b)
+let rev_it_mkPLambda = List.fold_right mkPLambda 
 
 let rec pat_of_raw metas vars = function
   | RVar (_,id) ->
@@ -212,17 +238,30 @@ let rec pat_of_raw metas vars = function
         Pp.warning "Cast not taken into account in constr pattern";
       pat_of_raw metas vars c
   | RIf (_,c,(_,None),b1,b2) ->
-      PCase ((None,IfStyle),None, pat_of_raw metas vars c,
-             [|pat_of_raw metas vars b1; pat_of_raw metas vars b2|])
-  | RCases (loc,None,[c,_],brs) ->
-      let sp =
+      PIf (pat_of_raw metas vars c,
+           pat_of_raw metas vars b1,pat_of_raw metas vars b2)
+  | RLetTuple (loc,nal,(_,None),b,c) ->
+      let mkRLambda c na = RLambda (loc,na,RHole (loc,Evd.InternalHole),c) in
+      let c = List.fold_left mkRLambda c nal in
+      PCase ((LetStyle,[|1|],None,None),PMeta None,pat_of_raw metas vars b,
+             [|pat_of_raw metas vars c|])
+  | RCases (loc,p,[c,(na,indnames)],brs) ->
+      let pred,ind_nargs, ind = match p,indnames with
+	| Some p, Some (_,ind,n,nal) ->
+	    rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p)),
+	    Some (n,List.length nal),Some ind
+	| _ -> PMeta None, None, None in
+      let ind = match ind with Some _ -> ind | None ->
 	match brs with
 	  | (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind
 	  | _ -> None in
-      PCase ((sp,Term.RegularStyle),None,
-             pat_of_raw metas vars c,
-             Array.init (List.length brs)
-	       (pat_of_raw_branch loc metas vars sp brs))
+      let cbrs =
+	Array.init (List.length brs) (pat_of_raw_branch loc metas vars ind brs)
+      in
+      let cstr_nargs,brs = (Array.map fst cbrs, Array.map snd cbrs) in
+      PCase ((RegularStyle,cstr_nargs,ind,ind_nargs), pred,
+             pat_of_raw metas vars c, brs)
+             
   | r ->
       let loc = loc_of_rawconstr r in
       user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Pattern not supported")
@@ -230,12 +269,12 @@ let rec pat_of_raw metas vars = function
 and pat_of_raw_branch loc metas vars ind brs i =
   let bri = List.filter
     (function
-        (_,_,[PatCstr(_,c,lv,_)],_) -> snd c = i+1
+        (_,_,[PatCstr(_,c,lv,Anonymous)],_) -> snd c = i+1
       | (loc,_,_,_) ->
           user_err_loc (loc,"pattern_of_rawconstr",
                         Pp.str "Not supported pattern")) brs in
   match bri with
-      [(_,_,[PatCstr(_,(indsp,_),lv,_)],br)] ->
+    | [(_,_,[PatCstr(_,(indsp,_),lv,_)],br)] ->
 	if ind <> None & ind <> Some indsp then
           user_err_loc (loc,"pattern_of_rawconstr",
             Pp.str "All constructors must be in the same inductive type");
@@ -246,8 +285,7 @@ and pat_of_raw_branch loc metas vars ind brs i =
                   user_err_loc (loc,"pattern_of_rawconstr",
                                 Pp.str "Not supported pattern")) lv in
         let vars' = List.rev lna @ vars in 
-        List.fold_right (fun na b -> PLambda(na,PMeta None,b)) lna
-          (pat_of_raw metas vars' br)
+	List.length lv, rev_it_mkPLambda lna (pat_of_raw metas vars' br)
     | _ -> user_err_loc (loc,"pattern_of_rawconstr",
                          str "No unique branch for " ++ int (i+1) ++
                          str"-th constructor")
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 25a57ed2..1637fc5f 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pattern.mli 7732 2005-12-26 13:51:24Z herbelin $ i*)
+(*i $Id: pattern.mli 8755 2006-04-27 22:22:15Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -39,8 +39,9 @@ type constr_pattern =
   | PLetIn of name * constr_pattern * constr_pattern
   | PSort of rawsort
   | PMeta of patvar option
-  | PCase of (inductive option * case_style)
-      * constr_pattern option * constr_pattern * constr_pattern array
+  | PIf of constr_pattern * constr_pattern * constr_pattern
+  | PCase of (case_style * int array * inductive option * (int * int) option)
+      * constr_pattern * constr_pattern * constr_pattern array
   | PFix of fixpoint
   | PCoFix of cofixpoint
 
@@ -76,3 +77,5 @@ val pattern_of_rawconstr : rawconstr ->
 
 val instantiate_pattern :
   (identifier * constr_pattern) list -> constr_pattern -> constr_pattern
+
+val lift_pattern : int -> constr_pattern -> constr_pattern
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 48295c92..f5a81659 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pretype_errors.ml 8688 2006-04-07 15:08:12Z msozeau $ *)
+(* $Id: pretype_errors.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
 
 open Util
 open Stdpp
@@ -59,7 +59,7 @@ let env_ise sigma env =
   Sign.fold_rel_context
     (fun (na,b,ty) e ->
       push_rel
-        (na, option_app (nf_evar sigma) b, nf_evar sigma ty)
+        (na, option_map (nf_evar sigma) b, nf_evar sigma ty)
         e)
     ctxt
     ~init:env0
@@ -75,7 +75,7 @@ let contract env lc =
 	  env
       | _ -> 
 	  let t' = substl !l t in
-	  let c' = option_app (substl !l) c in
+	  let c' = option_map (substl !l) c in
 	  let na' = named_hd env t' na in
 	  l := (mkRel 1) :: List.map (lift 1) !l;
 	  push_rel (na',c',t') env in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2d1e297f..ca797f97 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pretyping.ml 8695 2006-04-10 16:33:52Z msozeau $ *)
+(* $Id: pretyping.ml 8875 2006-05-29 19:59:11Z msozeau $ *)
 
 open Pp
 open Util
@@ -273,7 +273,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     | REvar (loc, ev, instopt) ->
 	(* Ne faudrait-il pas s'assurer que hyps est bien un
 	   sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
-	let hyps = evar_context (Evd.map (evars_of !isevars) ev) in
+	let hyps = evar_context (Evd.find (evars_of !isevars) ev) in
 	let args = match instopt with
           | None -> instance_from_named_context hyps
           | Some inst -> failwith "Evar subtitutions not implemented" in
@@ -329,34 +329,43 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		 { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
 		   uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
             ctxtv vdef in
-	  evar_type_fixpoint loc env isevars names ftys vdefj;
-	  let fixj =
-	    match fixkind with
-	      | RFix (vn,i) ->
-		  let fix = ((Array.map fst vn, i),(names,ftys,Array.map j_val vdefj)) in
-		    (try check_fix env fix with e -> Stdpp.raise_with_loc loc e);
-		    make_judge (mkFix fix) ftys.(i)
-	      | RCoFix i -> 
-		  let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
-		    (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
-		    make_judge (mkCoFix cofix) ftys.(i) in
-	    inh_conv_coerce_to_tycon loc env isevars fixj tycon
+	evar_type_fixpoint loc env isevars names ftys vdefj;
+	let fixj = match fixkind with
+	  | RFix (vn,i) ->
+	      let guard_indexes = Array.mapi 
+		(fun i (n,_) -> match n with 
+		   | Some n -> n 
+		   | None -> 
+		       (* Recursive argument was not given by the user : We
+			  check that there is only one inductive argument *)
+		       let ctx = ctxtv.(i) in 
+		       let isIndApp t = 
+			 isInd (fst (decompose_app (strip_head_cast t))) in
+			 (* This could be more precise (e.g. do some delta) *)
+		       let lb = List.rev_map (fun (_,_,t) -> isIndApp t) ctx in
+		       try (list_unique_index true lb) - 1
+		       with Not_found -> 
+			 Util.user_err_loc
+			   (loc,"pretype",
+			    Pp.str "cannot guess decreasing argument of fix"))
+		vn 
+	      in
+	      let fix = ((guard_indexes, i),(names,ftys,Array.map j_val vdefj)) in
+	      (try check_fix env fix with e -> Stdpp.raise_with_loc loc e);
+	      make_judge (mkFix fix) ftys.(i)
+	  | RCoFix i -> 
+	      let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
+	      (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
+	      make_judge (mkCoFix cofix) ftys.(i) in
+	inh_conv_coerce_to_tycon loc env isevars fixj tycon
 
     | RSort (loc,s) ->
 	inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon
 
     | RApp (loc,f,args) -> 
-	let length = List.length args in	 
-	let ftycon = 
-	  match tycon with
-	      None -> None
-	    | Some (None, ty) -> mk_abstr_tycon length ty
-	    | Some (Some (init, cur), ty) ->
-		Some (Some (length + init, length + cur), ty)
-	in
 	let fj = pretype empty_tycon env isevars lvar f in
  	let floc = loc_of_rawconstr f in
-	let rec apply_rec env n resj tycon = function
+	let rec apply_rec env n resj = function
 	  | [] -> resj
 	  | c::rest ->
 	      let argloc = loc_of_rawconstr c in
@@ -367,38 +376,22 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		      let hj = pretype (mk_tycon c1) env isevars lvar c in
 		      let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
 		      let typ' = nf_isevar !isevars typ in
-		      let tycon = 
-			option_app 
-			  (fun (abs, ty) ->
-			     match abs with
-				 None ->
-				   isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
-				     (abs, ty);
-				   (abs, ty)
-			       | Some (init, cur) ->
-				   isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' 
-				     (abs, ty);
-				   (Some (init, pred cur), ty))
-			  tycon
-		      in 
 			apply_rec env (n+1) 
 			  { uj_val = nf_isevar !isevars value;
-			    uj_type = nf_isevar !isevars typ' }
-			  (option_app (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest
-
+			    uj_type = typ' }
+			  rest
 		  | _ ->
 		      let hj = pretype empty_tycon env isevars lvar c in
 			error_cant_apply_not_functional_loc 
 			  (join_loc floc argloc) env (evars_of !isevars)
 	      		  resj [hj]
 	in
-	let ftycon = option_app (lift_abstr_tycon_type (-1)) ftycon in
-	let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in
+	let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj args) in
 	let resj =
 	  match kind_of_term resj.uj_val with
 	  | App (f,args) when isInd f ->
 	      let sigma = evars_of !isevars in
-	      let t = Retyping.type_of_applied_inductive env sigma (destInd f) args in
+	      let t = Retyping.type_of_inductive_knowing_parameters env sigma (destInd f) args in
 	      let s = snd (splay_arity env sigma t) in
 	      on_judgment_type (set_inductive_level env s) resj
 		(* Rem: no need to send sigma: no head evar, it's an arity *)
@@ -573,12 +566,19 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  tycon env (* loc *) (po,tml,eqns)
 
     | RCast(loc,c,k,t) ->
-	let tj = pretype_type empty_valcon env isevars lvar t in
-	let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in
-	  (* User Casts are for helping pretyping, experimentally not to be kept*)
-	  (* ... except for Correctness *)
-	let v = mkCast (cj.uj_val, k, tj.utj_val) in
-	let cj = { uj_val = v; uj_type = tj.utj_val } in
+	let cj =
+	  match k with
+	      CastCoerce ->
+		let cj = pretype empty_tycon env isevars lvar c in
+		  evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj
+	    | CastConv k ->
+		let tj = pretype_type empty_valcon env isevars lvar t in
+		let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in
+		  (* User Casts are for helping pretyping, experimentally not to be kept*)
+		  (* ... except for Correctness *)
+		let v = mkCast (cj.uj_val, k, tj.utj_val) in
+		  { uj_val = v; uj_type = tj.utj_val }
+	in
 	  inh_conv_coerce_to_tycon loc env isevars cj tycon
 
     | RDynamic (loc,d) ->
@@ -640,8 +640,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let rec proc_rec c =
       match kind_of_term c with
 	| Evar (ev,args) ->
-            assert (Evd.in_dom sigma ev);
-	    if not (Evd.in_dom initial_sigma ev) then
+            assert (Evd.mem sigma ev);
+	    if not (Evd.mem initial_sigma ev) then
               let (loc,k) = evar_source ev !isevars in
 		error_unsolvable_implicit loc env sigma k
 	| _ -> iter_constr proc_rec c
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 5d177326..e61bf2c3 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: rawterm.ml 8624 2006-03-13 17:38:17Z msozeau $ *)
+(* $Id: rawterm.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
 
 (*i*)
 open Util
@@ -47,6 +47,10 @@ type 'a bindings =
 
 type 'a with_bindings = 'a * 'a bindings
 
+type cast_type =
+  | CastConv of cast_kind
+  | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *)
+
 type rawconstr = 
   | RRef of (loc * global_reference)
   | RVar of (loc * identifier)
@@ -56,9 +60,7 @@ type rawconstr =
   | RLambda of loc * name * rawconstr * rawconstr
   | RProd of loc * name * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
-  | RCases of loc * rawconstr option *
-      (rawconstr * (name * (loc * inductive * name list) option)) list * 
-      (loc * identifier list * cases_pattern list * rawconstr) list
+  | RCases of loc * rawconstr option * tomatch_tuple * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
   | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
@@ -66,19 +68,29 @@ type rawconstr =
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
   | RHole of (loc * hole_kind)
-  | RCast of loc * rawconstr * cast_kind * rawconstr
+  | RCast of loc * rawconstr * cast_type * rawconstr
   | RDynamic of loc * Dyn.t
 
 and rawdecl = name * rawconstr option * rawconstr
 
 and fix_recursion_order = RStructRec | RWfRec of rawconstr
 
-and fix_kind = RFix of ((int * fix_recursion_order) array * int) | RCoFix of int
+and fix_kind =
+  | RFix of ((int option * fix_recursion_order) array * int)
+  | RCoFix of int
+
+and predicate_pattern =
+    name * (loc * inductive * int * name list) option
+
+and tomatch_tuple = (rawconstr * predicate_pattern) list
+
+and cases_clauses =
+    (loc * identifier list * cases_pattern list * rawconstr) list
 
 let cases_predicate_names tml =
   List.flatten (List.map (function
     | (tm,(na,None)) -> [na]
-    | (tm,(na,Some (_,_,nal))) -> na::nal) tml)
+    | (tm,(na,Some (_,_,_,nal))) -> na::nal) tml)
 
 (*i - if PRec (_, names, arities, bodies) is in env then arities are
    typed in env too and bodies are typed in env enriched by the
@@ -89,7 +101,7 @@ let cases_predicate_names tml =
 
    - boolean in POldCase means it is recursive
 i*)
-let map_rawdecl f (na,obd,ty) = (na,option_app f obd,f ty)
+let map_rawdecl f (na,obd,ty) = (na,option_map f obd,f ty)
 
 let map_rawconstr f = function
   | RVar (loc,id) -> RVar (loc,id)
@@ -98,13 +110,13 @@ let map_rawconstr f = function
   | RProd (loc,na,ty,c) -> RProd (loc,na,f ty,f c)
   | RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c)
   | RCases (loc,rtntypopt,tml,pl) ->
-      RCases (loc,option_app f rtntypopt,
+      RCases (loc,option_map f rtntypopt,
         List.map (fun (tm,x) -> (f tm,x)) tml,
         List.map (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl)
   | RLetTuple (loc,nal,(na,po),b,c) ->
-      RLetTuple (loc,nal,(na,option_app f po),f b,f c)
+      RLetTuple (loc,nal,(na,option_map f po),f b,f c)
   | RIf (loc,c,(na,po),b1,b2) ->
-      RIf (loc,f c,(na,option_app f po),f b1,f b2)
+      RIf (loc,f c,(na,option_map f po),f b1,f b2)
   | RRec (loc,fk,idl,bl,tyl,bv) ->
       RRec (loc,fk,idl,Array.map (List.map (map_rawdecl f)) bl,
             Array.map f tyl,Array.map f bv)
@@ -137,7 +149,7 @@ let map_rawconstr_with_binders_loc loc g f e = function
       let g' id e = snd (g id e) in
       let h (_,idl,p,c) = (loc,idl,p,f (List.fold_right g' idl e) c) in
       RCases
-	(loc,option_app (f e) tyopt,List.map (f e) tml, List.map h pl)
+	(loc,option_map (f e) tyopt,List.map (f e) tml, List.map h pl)
   | RRec (_,fk,idl,tyl,bv) ->
       let idl',e' = fold_ident g idl e in
       RRec (loc,fk,idl',Array.map (f e) tyl,Array.map (f e') bv)
@@ -251,22 +263,24 @@ type 'a raw_red_flag = {
 let all_flags =
   {rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []}
 
-type 'a occurrences = int list * 'a
+type 'a or_var = ArgArg of 'a | ArgVar of identifier located
+
+type 'a with_occurrences = int or_var list * 'a
 
 type ('a,'b) red_expr_gen =
   | Red of bool
   | Hnf
-  | Simpl of 'a occurrences option
+  | Simpl of 'a with_occurrences option
   | Cbv of 'b raw_red_flag
   | Lazy of 'b raw_red_flag
-  | Unfold of 'b occurrences list
+  | Unfold of 'b with_occurrences list
   | Fold of 'a list
-  | Pattern of 'a occurrences list
+  | Pattern of 'a with_occurrences list
   | ExtraRedExpr of string
   | CbvVm
 
 type ('a,'b) may_eval =
   | ConstrTerm of 'a
-  | ConstrEval of ('a, 'b) red_expr_gen * 'a
+  | ConstrEval of ('a,'b) red_expr_gen * 'a
   | ConstrContext of (loc * identifier) * 'a
   | ConstrTypeOf of 'a
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 22317b5f..b29cc7b6 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: rawterm.mli 8624 2006-03-13 17:38:17Z msozeau $ i*)
+(*i $Id: rawterm.mli 8878 2006-05-30 16:44:25Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -44,6 +44,10 @@ type 'a bindings =
 
 type 'a with_bindings = 'a * 'a bindings
 
+type cast_type =
+  | CastConv of cast_kind
+  | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *)
+
 type rawconstr = 
   | RRef of (loc * global_reference)
   | RVar of (loc * identifier)
@@ -53,9 +57,7 @@ type rawconstr =
   | RLambda of loc * name * rawconstr * rawconstr
   | RProd of loc * name * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
-  | RCases of loc * rawconstr option *
-      (rawconstr * (name * (loc * inductive * name list) option)) list * 
-      (loc * identifier list * cases_pattern list * rawconstr) list
+  | RCases of loc * rawconstr option * tomatch_tuple * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
   | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
@@ -63,17 +65,26 @@ type rawconstr =
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
   | RHole of (loc * Evd.hole_kind)
-  | RCast of loc * rawconstr * cast_kind * rawconstr
+  | RCast of loc * rawconstr * cast_type * rawconstr
   | RDynamic of loc * Dyn.t
 
 and rawdecl = name * rawconstr option * rawconstr
 
 and fix_recursion_order = RStructRec | RWfRec of rawconstr
 
-and fix_kind = RFix of ((int * fix_recursion_order) array * int) | RCoFix of int
+and fix_kind =
+  | RFix of ((int option * fix_recursion_order) array * int)
+  | RCoFix of int
+
+and predicate_pattern =
+    name * (loc * inductive * int * name list) option
+
+and tomatch_tuple = (rawconstr * predicate_pattern) list
 
-val cases_predicate_names : 
-  (rawconstr * (name * (loc * inductive * name list) option)) list -> name list
+and cases_clauses =
+    (loc * identifier list * cases_pattern list * rawconstr) list
+
+val cases_predicate_names : tomatch_tuple -> name list
 
 (*i - if PRec (_, names, arities, bodies) is in env then arities are
    typed in env too and bodies are typed in env enriched by the
@@ -121,22 +132,24 @@ type 'a raw_red_flag = {
 
 val all_flags : 'a raw_red_flag
 
-type 'a occurrences = int list * 'a
+type 'a or_var = ArgArg of 'a | ArgVar of identifier located
+
+type 'a with_occurrences = int or_var list * 'a
 
 type ('a,'b) red_expr_gen =
   | Red of bool
   | Hnf
-  | Simpl of 'a occurrences option
+  | Simpl of 'a with_occurrences option
   | Cbv of 'b raw_red_flag
   | Lazy of 'b raw_red_flag
-  | Unfold of 'b occurrences list
+  | Unfold of 'b with_occurrences list
   | Fold of 'a list
-  | Pattern of 'a occurrences list
+  | Pattern of 'a with_occurrences list
   | ExtraRedExpr of string
   | CbvVm
 
 type ('a,'b) may_eval =
   | ConstrTerm of 'a
-  | ConstrEval of ('a, 'b) red_expr_gen * 'a
+  | ConstrEval of ('a,'b) red_expr_gen * 'a
   | ConstrContext of (loc * identifier) * 'a
   | ConstrTypeOf of 'a
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 87997d99..5d38f52c 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: recordops.ml 8642 2006-03-17 10:09:02Z notin $ *)
+(* $Id: recordops.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
 
 open Util
 open Pp
@@ -67,7 +67,7 @@ let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) =
 
 let discharge_structure (_,(ind,id,kl,projs)) =
   Some (Lib.discharge_inductive ind, id, kl,
-        List.map (option_app Lib.discharge_con) projs)
+        List.map (option_map Lib.discharge_con) projs)
 
 let (inStruc,outStruc) =
   declare_object {(default_object "STRUCTURE") with 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index b590f743..82cc1b7d 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: reductionops.ml 8708 2006-04-14 08:13:02Z jforest $ *)
+(* $Id: reductionops.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
 
 open Pp
 open Util
@@ -23,6 +23,91 @@ open Reduction
 
 exception Elimconst
 
+
+(**********************************************************************)
+(* The type of (machine) stacks (= lambda-bar-calculus' contexts)     *) 
+
+type 'a stack_member =
+  | Zapp of 'a list
+  | Zcase of case_info * 'a * 'a array
+  | Zfix of 'a * 'a stack
+  | Zshift of int
+  | Zupdate of 'a
+
+and 'a stack = 'a stack_member list
+
+let empty_stack = []
+let append_stack_list = function
+  | ([],s) -> s
+  | (l1, Zapp l :: s) -> Zapp (l1@l) :: s
+  | (l1, s) -> Zapp l1 :: s
+let append_stack v s = append_stack_list (Array.to_list v, s)
+
+(* Collapse the shifts in the stack *)
+let zshift n s =
+  match (n,s) with
+      (0,_) -> s
+    | (_,Zshift(k)::s) -> Zshift(n+k)::s
+    | _ -> Zshift(n)::s
+
+let rec stack_args_size = function
+  | Zapp l::s -> List.length l + stack_args_size s
+  | Zshift(_)::s -> stack_args_size s
+  | Zupdate(_)::s -> stack_args_size s
+  | _ -> 0
+
+(* When used as an argument stack (only Zapp can appear) *)
+let rec decomp_stack = function
+  | Zapp[v]::s -> Some (v, s)
+  | Zapp(v::l)::s -> Some (v, (Zapp l :: s))
+  | Zapp [] :: s -> decomp_stack s
+  | _ -> None
+let rec decomp_stackn = function
+  | Zapp [] :: s -> decomp_stackn s
+  | Zapp l :: s -> (Array.of_list l, s)
+  | _ -> assert false
+let array_of_stack s =
+  let rec stackrec = function
+  | [] -> []
+  | Zapp args :: s -> args :: (stackrec s)
+  | _ -> assert false
+  in Array.of_list (List.concat (stackrec s))
+let rec list_of_stack = function
+  | [] -> []
+  | Zapp args :: s -> args @ (list_of_stack s)
+  | _ -> assert false
+let rec app_stack = function
+  | f, [] -> f
+  | f, (Zapp [] :: s) -> app_stack (f, s)
+  | f, (Zapp args :: s) -> 
+      app_stack (applist (f, args), s)
+  | _ -> assert false
+let rec stack_assign s p c = match s with
+  | Zapp args :: s ->
+      let q = List.length args in 
+      if p >= q then
+	Zapp args :: stack_assign s (p-q) c
+      else
+        (match list_chop p args with
+            (bef, _::aft) -> Zapp (bef@c::aft) :: s
+          | _ -> assert false)
+  | _ -> s
+let rec stack_tail p s =
+  if p = 0 then s else
+    match s with
+      | Zapp args :: s ->
+	  let q = List.length args in
+	  if p >= q then stack_tail (p-q) s
+	  else Zapp (list_skipn p args) :: s
+      | _ -> failwith "stack_tail"
+let rec stack_nth s p = match s with
+  | Zapp args :: s ->
+      let q = List.length args in
+      if p >= q then stack_nth s (p-q)
+      else List.nth args p
+  | _ -> raise Not_found
+
+(**************************************************************)
 (* The type of (machine) states (= lambda-bar-calculus' cuts) *) 
 type state = constr * constr stack
 
@@ -428,13 +513,13 @@ let whd_betadeltaiota_nolet env sigma x =
 let rec whd_evar sigma c =
   match kind_of_term c with
     | Evar (ev,args)
-        when Evd.in_dom sigma ev & Evd.is_defined sigma ev ->
+        when Evd.mem sigma ev & Evd.is_defined sigma ev ->
 	whd_evar sigma (Evd.existential_value sigma (ev,args))
     | Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c
     | _ -> collapse_appl c
 
-let nf_evar evd =
-  local_strong (whd_evar evd)
+let nf_evar sigma =
+  local_strong (whd_evar sigma)
 
 (* lazy reduction functions. The infos must be created for each term *)
 let clos_norm_flags flgs env sigma t =
@@ -451,113 +536,49 @@ let nf_betadeltaiota env sigma =
    du type checking :
      (fun x => x + x) M
 *)
-let nf_betaiotaevar_preserving_vm_cast env sigma t = 
-  let push decl (env,subst) = 
-    (Environ.push_rel decl env, Esubst.subs_lift subst) in
-  let cons decl v (env, subst) = (push_rel decl env, Esubst.subs_cons (v,subst)) in
-
-  let app_stack t (f, stack) = 
-    let t' = app_stack (f,stack) in
-    match kind_of_term t, kind_of_term t' with
-      | App(f,args), App(f',args') when f == f' && array_for_all2 (==) args args' -> t
-      | _ -> t'
-  in
-  let rec whrec (env, subst as es) (t, stack as s) =
-    match kind_of_term t with
-      | Rel i -> 
-	  let t' = 
-	    match Esubst.expand_rel i subst with
-	      | Inl (k,e) -> lift k e
-	      | Inr (k,None) -> mkRel k
-	      | Inr (k, Some p) -> lift (k-p) (mkRel p) (*??????? == mkRel k !  Julien *)
-                           (* Est correct ??? *)
-	  in
-	  if t = t' then s else t', stack
-      | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> s
-      | Evar (e,al) -> 
-	  let al' = Array.map (norm es) al in
-	  begin match existential_opt_value sigma (e,al') with
-	    | Some body -> whrec (env,Esubst.ESID 0) (body, stack) (**** ????? ****)
-	    | None ->
-		if array_for_all2 (==) al al' then s else (mkEvar (e, al'), stack)
-	  end
-      | Cast (c,VMcast,t) ->
-	  let c' = norm es c in
-	  let t' = norm es t in 
-	  if c == c' && t == t' then s
-	  else (mkCast(c',VMcast,t'),stack)
-      | Cast (c,DEFAULTcast,_) ->
-	  whrec es (c, stack)
-
-      | Prod (na,t,c) ->
-	  let t' = norm es t in
-	  let c' = norm (push (na, None, t') es) c in
-	  if t==t' && c==c' then s else (mkProd (na, t', c'), stack)
-
-      | Lambda (na,t,c) ->
-          begin match decomp_stack stack with
-            | Some (a,m) -> 
-		begin match kind_of_term a with
-		  | Rel i when not (evaluable_rel i env) ->
-                      whrec (cons (na,None,t) a es) (c, m)
-		  | Var id when  not (evaluable_named id env)->
-                      whrec (cons (na,None,t) a es) (c, m)
-		  | _ -> 
-		      let t' = norm es t in
-		      let c' = norm (push (na, None, t') es) c in
-		      if t == t' && c == c' then s
-		      else mkLambda (na, t', c'), stack
-		end
-            | _ -> 
-		let t' = norm es t in 
-		let c' =  norm (push (na, None, t') es) c  in 
-		if t == t' && c == c' then s 
-		else mkLambda(na,t',c'),stack
-		
-	  end
-      | LetIn (na,b,t,c) ->
-	  let b' = norm es b in
-	  let t' = norm es t in
-	  let c' = norm (push (na, Some b', t') es) c in
-	  if b==b' && t==t' && c==c' then s 
-	  else mkLetIn (na, b', t', c'), stack
-
-      | App (f,cl)  -> 
-          let cl' = Array.map (norm es) cl in
-          whrec es (f, append_stack cl' stack)
-
-      | Case (ci,p,d,lf) ->
-          let (c,cargs) = whrec es (d, empty_stack) in
-          if reducible_mind_case c then
-            whrec es (reduce_mind_case
-                     {mP=p; mconstr=c; mcargs=list_of_stack cargs;
-		      mci=ci; mlf=lf}, stack)
-          else     
-	    let p' = norm es p in
-	    let d' = app_stack d (c,cargs) in 
-	    let lf' = Array.map (norm es) lf in
-	    if p==p' && d==d' && array_for_all2 (==) lf lf' then s 
-	    else (mkCase (ci, p', d', lf'), stack)
-      | Fix (ln,(lna,tl,bl)) ->
-	  let tl' = Array.map (norm es) tl in
-	  let es' =
-            array_fold_left2 (fun es na t -> push (na,None,t) es) es lna tl' in
-	  let bl' = Array.map (norm es') bl in
-	  if array_for_all2 (==) tl tl' && array_for_all2 (==) bl bl'
-	  then s
-	  else (mkFix (ln,(lna,tl',bl')), stack)
-      | CoFix(ln,(lna,tl,bl)) ->
-	  let tl' = Array.map (norm es) tl in
-	  let es' =
-            array_fold_left2 (fun es na t -> push (na,None,t) es) es lna tl in
-	  let bl' = Array.map (norm es') bl in
-	  if array_for_all2 (==) tl tl' && array_for_all2 (==) bl bl'
-	  then s
-	  else (mkCoFix (ln,(lna,tl',bl')), stack)
-
-  and norm es t = app_stack t (whrec es (t,empty_stack)) in
-  norm (env, Esubst.ESID 0) t
-
+let rec whd_betaiotaevar_preserving_vm_cast env sigma t = 	 
+   let rec stacklam_var subst t stack = 	 
+     match (decomp_stack stack,kind_of_term t) with 	 
+     | Some (h,stacktl), Lambda (_,_,c) -> 	 
+         begin match kind_of_term h with 	 
+         | Rel i when not (evaluable_rel i env) -> 	 
+             stacklam_var (h::subst) c stacktl 	 
+         | Var id when  not (evaluable_named id env)-> 	 
+             stacklam_var (h::subst) c stacktl 	 
+         | _ -> whrec (substl subst t, stack) 	 
+         end 	 
+     | _ -> whrec (substl subst t, stack) 	 
+   and whrec (x, stack as s) = 	 
+     match kind_of_term x with 	 
+       | Evar ev -> 	 
+           (match existential_opt_value sigma ev with 	 
+              | Some body -> whrec (body, stack) 	 
+              | None -> s) 	 
+       | Cast (c,VMcast,t) -> 	 
+           let c = app_stack (whrec (c,empty_stack)) in 	 
+           let t = app_stack (whrec (t,empty_stack)) in 	 
+           (mkCast(c,VMcast,t),stack) 	 
+       | Cast (c,DEFAULTcast,_) -> 	 
+           whrec (c, stack) 	 
+       | App (f,cl)  -> whrec (f, append_stack cl stack) 	 
+       | Lambda (na,t,c) -> 	 
+           (match decomp_stack stack with 	 
+            | Some (a,m) -> stacklam_var [a] c m 	 
+            | _ -> s) 	 
+       | Case (ci,p,d,lf) -> 	 
+           let (c,cargs) = whrec (d, empty_stack) in 	 
+           if reducible_mind_case c then 	 
+             whrec (reduce_mind_case 	 
+                      {mP=p; mconstr=c; mcargs=list_of_stack cargs; 	 
+                       mci=ci; mlf=lf}, stack) 	 
+           else 	 
+             (mkCase (ci, p, app_stack (c,cargs), lf), stack) 	 
+       | x -> s 	 
+   in 	 
+   app_stack (whrec (t,empty_stack))
+
+let nf_betaiotaevar_preserving_vm_cast = 
+  strong whd_betaiotaevar_preserving_vm_cast
 
 (* lazy weak head reduction functions *)
 let whd_flags flgs env sigma t =
@@ -825,26 +846,6 @@ let is_arity env sigma c =
   match find_conclusion env sigma c with
     | Sort _ -> true
     | _ -> false
- 
-let info_arity env sigma c =
-  match find_conclusion env sigma c with
-    | Sort (Prop Null) -> false 
-    | Sort (Prop Pos) -> true 
-    | _ -> raise IsType
-    
-let is_info_arity env sigma c =
-  try (info_arity env sigma c) with IsType -> true
-  
-let is_type_arity env sigma c = 
-  match find_conclusion env sigma c with
-    | Sort (Type _) -> true
-    | _ -> false
-
-let is_info_type env sigma t =
-  let s = t.utj_type in
-  (s = Prop Pos) ||
-  (s <> Prop Null && 
-   try info_arity env sigma t.utj_val with IsType -> true)
 
 (*************************************)
 (* Metas *)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index ff55cc0e..78afd22b 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: reductionops.mli 8708 2006-04-14 08:13:02Z jforest $ i*)
+(*i $Id: reductionops.mli 8812 2006-05-13 11:46:02Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -21,6 +21,34 @@ open Closure
 
 exception Elimconst
 
+(************************************************************************)
+(*s A [stack] is a context of arguments, arguments are pushed by
+   [append_stack] one array at a time but popped with [decomp_stack]
+   one by one *)
+
+type 'a stack_member =
+  | Zapp of 'a list
+  | Zcase of case_info * 'a * 'a array
+  | Zfix of 'a * 'a stack
+  | Zshift of int
+  | Zupdate of 'a
+
+and 'a stack = 'a stack_member list
+
+val empty_stack : 'a stack
+val append_stack : 'a array -> 'a stack -> 'a stack
+
+val decomp_stack : 'a stack -> ('a * 'a stack) option
+val list_of_stack : 'a stack -> 'a list
+val array_of_stack : 'a stack -> 'a array
+val stack_assign : 'a stack -> int -> 'a -> 'a stack
+val stack_args_size : 'a stack -> int
+val app_stack : constr * constr stack -> constr
+val stack_tail : int -> 'a stack -> 'a stack
+val stack_nth : 'a stack -> int -> 'a
+
+(************************************************************************)
+
 type state = constr * constr stack
 
 type contextual_reduction_function = env -> evar_map -> constr -> constr
@@ -147,13 +175,6 @@ val reduce_mind_case : constr miota_args -> constr
 
 val find_conclusion : env -> evar_map -> constr -> (constr,constr) kind_of_term
 val is_arity : env ->  evar_map -> constr -> bool
-val is_info_type : env ->  evar_map -> unsafe_type_judgment -> bool
-val is_info_arity : env ->  evar_map -> constr -> bool
-(*i Pour l'extraction
-val is_type_arity : env -> 'a evar_map -> constr -> bool
-val is_info_cast_type : env -> 'a evar_map -> constr -> bool
-val contents_of_cast_type : env -> 'a evar_map -> constr -> contents
-i*)
 
 val whd_programs :  reduction_function
 
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 32da4cea..428a7306 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: retyping.ml 8673 2006-03-29 21:21:52Z herbelin $ *)
+(* $Id: retyping.ml 8871 2006-05-28 16:46:48Z herbelin $ *)
 
 open Util
 open Term
@@ -74,7 +74,7 @@ let typeur sigma metamap =
     | Fix ((_,i),(_,tys,_)) -> tys.(i)
     | CoFix (i,(_,tys,_)) -> tys.(i)
     | App(f,args) when isInd f ->
-	let t = type_of_applied_inductive env (destInd f) args in
+	let t = type_of_inductive_knowing_parameters env (destInd f) args in
         strip_outer_cast (subst_type env sigma t (Array.to_list args))
     | App(f,args) ->
         strip_outer_cast
@@ -98,7 +98,7 @@ let typeur sigma metamap =
 	  | Prop Null, (Type _ as s) -> s
 	  | Type u1, Type u2 -> Type (Univ.sup u1 u2))
     | App(f,args) when isInd f ->
-	let t = type_of_applied_inductive env (destInd f) args in
+	let t = type_of_inductive_knowing_parameters env (destInd f) args in
         sort_of_atomic_type env sigma t args
     | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
     | Lambda _ | Fix _ | Construct _ ->
@@ -117,25 +117,17 @@ let typeur sigma metamap =
         anomaly "sort_of: Not a type (1)"
     | _ -> family_of_sort (decomp_sort env sigma (type_of env t))
 
-  and type_of_applied_inductive env ind args =
-    let specif = lookup_mind_specif env ind in
-    let t = Inductive.type_of_inductive specif in
-    if is_small_inductive specif then
-      (* No polymorphism *)
-      t
-    else
-      (* Retyping constructor with the actual arguments *)
-      let env',llc,ls0 = constructor_instances env specif ind args in
-      let lls = Array.map (Array.map (sort_of env')) llc in
-      let ls = Array.map max_inductive_sort lls in
-      set_inductive_level env (find_inductive_level env specif ind ls0 ls) t
+  and type_of_inductive_knowing_parameters env ind args =
+    let (_,mip) = lookup_mind_specif env ind in
+    let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in
+    Inductive.type_of_inductive_knowing_parameters env mip argtyps
 
-  in type_of, sort_of, sort_family_of, type_of_applied_inductive
+  in type_of, sort_of, sort_family_of, type_of_inductive_knowing_parameters
 
 let get_type_of env sigma c = let f,_,_,_ = typeur sigma [] in f env c
 let get_sort_of env sigma t = let _,f,_,_ = typeur sigma [] in f env t
 let get_sort_family_of env sigma c = let _,_,f,_ = typeur sigma [] in f env c
-let type_of_applied_inductive env sigma ind args =
+let type_of_inductive_knowing_parameters env sigma ind args =
   let _,_,_,f = typeur sigma [] in f env ind args
 
 let get_type_of_with_meta env sigma metamap = 
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 7adec66b..923123c5 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: retyping.mli 8673 2006-03-29 21:21:52Z herbelin $ i*)
+(*i $Id: retyping.mli 8871 2006-05-28 16:46:48Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -34,5 +34,5 @@ val get_assumption_of : env -> evar_map -> constr -> types
 (* Makes an unsafe judgment from a constr *)
 val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment
 
-val type_of_applied_inductive : env -> evar_map -> inductive -> 
+val type_of_inductive_knowing_parameters : env -> evar_map -> inductive -> 
   constr array -> types
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 88af6290..006e14b3 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacred.ml 8003 2006-02-07 22:11:50Z herbelin $ *)
+(* $Id: tacred.ml 8793 2006-05-05 17:41:41Z barras $ *)
 
 open Pp
 open Util
@@ -18,8 +18,8 @@ open Termops
 open Declarations
 open Inductive
 open Environ
-open Reductionops
 open Closure
+open Reductionops
 open Cbv
 open Rawterm
 
@@ -80,7 +80,7 @@ let reference_opt_value sigma env = function
       v
   | EvalRel n ->
       let (_,v,_) = lookup_rel n env in
-      option_app (lift n) v
+      option_map (lift n) v
   | EvalEvar ev -> Evd.existential_opt_value sigma ev
 
 exception NotEvaluable
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index a5468435..691fdf01 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacred.mli 8003 2006-02-07 22:11:50Z herbelin $ i*)
+(*i $Id: tacred.mli 8878 2006-05-30 16:44:25Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -77,5 +77,5 @@ val reduce_to_quantified_ref :
 val reduce_to_atomic_ref :
   env ->  evar_map -> Libnames.global_reference -> types -> types
 
-val contextually : bool -> constr occurrences -> reduction_function
+val contextually : bool -> int list * constr -> reduction_function
   -> reduction_function
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 89de5537..823da969 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: termops.ml 8003 2006-02-07 22:11:50Z herbelin $ *)
+(* $Id: termops.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
 
 open Pp
 open Util
@@ -25,7 +25,7 @@ let print_sort = function
   | Prop Null -> (str "Prop")
   | Type u -> (str "Type(" ++ Univ.pr_uni u ++ str ")")
 
-let print_sort_family = function
+let pr_sort_family = function
   | InSet -> (str "Set")
   | InProp -> (str "Prop")
   | InType -> (str "Type")
@@ -961,7 +961,7 @@ let assums_of_rel_context sign =
 let lift_rel_context n sign =
   let rec liftrec k = function
     | (na,c,t)::sign ->
-	(na,option_app (liftn n k) c,type_app (liftn n k) t)
+	(na,option_map (liftn n k) c,type_app (liftn n k) t)
 	::(liftrec (k-1) sign)
     | [] -> []
   in
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 5f8b5376..49de4838 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: termops.mli 8003 2006-02-07 22:11:50Z herbelin $ i*)
+(*i $Id: termops.mli 8845 2006-05-23 07:41:58Z herbelin $ i*)
 
 open Util
 open Pp
@@ -24,7 +24,7 @@ val refresh_universes : types -> types
 
 (* printers *)
 val print_sort : sorts -> std_ppcmds
-val print_sort_family : sorts_family -> std_ppcmds
+val pr_sort_family : sorts_family -> std_ppcmds
 (* debug printer: do not use to display terms to the casual user... *)
 val set_print_constr : (env -> constr -> std_ppcmds) -> unit
 val print_constr     : constr -> std_ppcmds
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index be922c7d..78902a7d 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: typing.ml 8673 2006-03-29 21:21:52Z herbelin $ *)
+(* $Id: typing.ml 8871 2006-05-28 16:46:48Z herbelin $ *)
 
 open Util
 open Names
@@ -88,14 +88,16 @@ let rec execute env evd cstr =
 	judge_of_type u
 	  
     | App (f,args) ->
-	let j = execute env evd f in
         let jl = execute_array env evd args in
-	let (j,_) = judge_of_apply env j jl in
+	let j =
 	if isInd f then
 	  (* Sort-polymorphism of inductive types *)
-	  adjust_inductive_level env evd (destInd f) args j
+	  judge_of_inductive_knowing_parameters env (destInd f)
+	    (jv_nf_evar (evars_of evd) jl)
 	else
-	  j
+	  execute env evd f
+	in
+	fst (judge_of_apply env j jl)
 	    
     | Lambda (name,c1,c2) -> 
         let j = execute env evd c1 in
@@ -141,25 +143,6 @@ and execute_array env evd = Array.map (execute env evd)
 
 and execute_list env evd = List.map (execute env evd)
 
-and adjust_inductive_level env evd ind args j =
-  let specif = lookup_mind_specif env ind in
-  if is_small_inductive specif then
-    (* No polymorphism *)
-    j
-  else
-    (* Retyping constructor with the actual arguments *)
-    let env',llc,ls0 = constructor_instances env specif ind args in
-    let llj = Array.map (execute_array env' evd) llc in
-    let ls =
-      Array.map (fun lj ->
-	let ls =
-	  Array.map (fun c -> decomp_sort env (evars_of evd) c.uj_type) lj
-	in
-	max_inductive_sort ls) llj
-    in
-    let s = find_inductive_level env specif ind ls0 ls in
-    on_judgment_type (set_inductive_level env s) j
-
 let mcheck env evd c t =
   let sigma = Evd.evars_of evd in
   let j = execute env evd (nf_evar sigma c) in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e51f5e0e..e4bde925 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: unification.ml 7113 2005-06-05 17:13:06Z barras $ *)
+(* $Id: unification.ml 8759 2006-04-28 12:24:14Z herbelin $ *)
 
 open Pp
 open Util
@@ -259,7 +259,7 @@ let w_merge env with_types mod_delta metas evars evd =
             end
 
   and mimick_evar evd mod_delta hdc nargs sp =
-    let ev = Evd.map (evars_of evd) sp in
+    let ev = Evd.find (evars_of evd) sp in
     let sp_env = Global.env_of_context ev.evar_hyps in
     let (evd', c) = applyHead sp_env evd nargs hdc in
     let (mc,ec) =