GROS COMMIT:

 - reduction du noyau (variables existentielles, fonctions auxiliaires
   pour inventer des noms, etc. deplacees hors de kernel/)
 - changement de noms de constructeurs des constr (suppression de "Is" et
   "Mut")


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

39 files changed, 3919 insertions, 636 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 39191f3953..1ecb4ce2dc 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -10,12 +10,14 @@
 
 open Util
 open Names
+open Nameops
 open Term
+open Termops
 open Declarations
-open Inductive
+open Inductiveops
 open Environ
 open Sign
-open Reduction
+open Reductionops
 open Typeops
 open Type_errors
 
@@ -53,14 +55,14 @@ let error_wrong_numarg_constructor_loc loc c n =
 let error_wrong_predicate_arity_loc loc env c n1 n2 =
   raise_pattern_matching_error (loc, env, WrongPredicateArity (c,n1,n2))
 
-let error_needs_inversion k env x t =
+let error_needs_inversion env x t =
   raise (PatternMatchingError (env, NeedsInversion (x,t)))
 
 (*********************************************************************)
 (* A) Typing old cases                                               *)
 (* This was previously in Indrec but creates existential holes       *)
 
-let mkExistential isevars env = new_isevar isevars env (new_Type ()) CCI
+let mkExistential isevars env = new_isevar isevars env (new_Type ())
 
 let norec_branch_scheme env isevars cstr =
   let rec crec env = function
@@ -77,7 +79,7 @@ let rec_branch_scheme env isevars (sp,j) recargs cstr =
 	      | Mrec k when k=j ->
 		  let t = mkExistential isevars env in
 		  mkArrow t
-		    (crec (push_rel_assum (Anonymous,t) env)
+		    (crec (push_rel (Anonymous,None,t) env)
 		       (List.rev (lift_rel_context 1 (List.rev rea)),reca))
               | _ -> crec (push_rel d env) (rea,reca) in
           mkProd (name, body_of_type c, d)
@@ -89,12 +91,13 @@ let rec_branch_scheme env isevars (sp,j) recargs cstr =
   in 
   crec env (List.rev cstr.cs_args,recargs) 
     
-let branch_scheme env isevars isrec (IndFamily (mis,params) as indf) =
-  let cstrs = get_constructors indf in 
+let branch_scheme env isevars isrec ((ind,params) as indf) =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  let cstrs = get_constructors env indf in 
   if isrec then
     array_map2
-      (rec_branch_scheme env isevars (mis_inductive mis))
-      (mis_recarg mis) cstrs
+      (rec_branch_scheme env isevars ind)
+      mip.mind_listrec cstrs
   else 
     Array.map (norec_branch_scheme env isevars) cstrs
 
@@ -104,7 +107,7 @@ let branch_scheme env isevars isrec (IndFamily (mis,params) as indf) =
 let concl_n env sigma = 
   let rec decrec m c = if m = 0 then (nf_evar sigma c) else 
     match kind_of_term (whd_betadeltaiota env sigma c) with
-      | IsProd (n,_,c_0) -> decrec (m-1) c_0
+      | Prod (n,_,c_0) -> decrec (m-1) c_0
       | _                -> failwith "Typing.concl_n"
   in 
   decrec
@@ -123,24 +126,25 @@ let count_rec_arg j =
  * where A'_bar = A_bar[p_bar <- globargs] *)
 
 let build_notdep_pred env sigma indf pred =
-  let arsign,_ = get_arity indf in
+  let arsign,_ = get_arity env indf in
   let nar = List.length arsign in
   it_mkLambda_or_LetIn_name env (lift nar pred) arsign
 
 exception NotInferable of ml_case_error
 
 let rec refresh_types t = match kind_of_term t with
-  | IsSort (Type _) -> new_Type ()
-  | IsProd (na,u,v) -> mkProd (na,u,refresh_types v)
+  | Sort (Type _) -> new_Type ()
+  | Prod (na,u,v) -> mkProd (na,u,refresh_types v)
   | _ -> t
 
 let pred_case_ml_fail env sigma isrec (IndType (indf,realargs)) (i,ft) =
   let pred =
-    let mispec,_ = dest_ind_family indf in
-    let recargs = mis_recarg mispec in
+    let (ind,params) = indf in
+    let (mib,mip) = Inductive.lookup_mind_specif env ind in
+    let recargs = mip.mind_listrec in
     if Array.length recargs = 0 then raise (NotInferable MlCaseAbsurd);
     let recargi = recargs.(i) in
-    let j = mis_index mispec in
+    let j = snd ind in (* index of inductive *)
     let nbrec = if isrec then count_rec_arg j recargi else 0 in
     let nb_arg = List.length (recargs.(i)) + nbrec in
     let pred = refresh_types (concl_n env sigma nb_arg ft) in
@@ -188,7 +192,8 @@ let make_anonymous_patvars =
 (* Environment management *)
 let push_rels vars env = List.fold_right push_rel vars env
 
-let push_rel_defs = List.fold_right push_rel_def
+let push_rel_defs =
+  List.fold_right (fun (x,d,t) e -> push_rel (x,Some d,t) e)
 
 let it_mkSpecialLetIn = 
   List.fold_left
@@ -701,7 +706,7 @@ let build_aliases_context env sigma names allpats pats =
 	  List.map2 (fun l1 l2 -> List.hd l2::l1) newallpats oldallpats in
 	let oldallpats = List.map List.tl oldallpats in
 	let d = (na,pat,t) in
-	insert (push_rel_def d env) (d::sign) (n+1) 
+	insert (push_rel (na,Some pat,t) env) (d::sign) (n+1) 
 	    newallpats oldallpats (pats,names)
     | [], [] -> newallpats, sign, env
     | _ -> anomaly "Inconsistent alias and name lists"
@@ -738,8 +743,8 @@ let insert_aliases env sigma aliases eqns =
 exception Occur
 let noccur_between_without_evar n m term = 
   let rec occur_rec n c = match kind_of_term c with
-    | IsRel p       -> if n<=p && p<n+m then raise Occur
-    | IsEvar (_,cl) -> ()
+    | Rel p       -> if n<=p && p<n+m then raise Occur
+    | Evar (_,cl) -> ()
     | _             -> iter_constr_with_binders succ occur_rec n c
   in 
   try occur_rec n term; true with Occur -> false
@@ -755,7 +760,7 @@ let prepare_unif_pb typ cs =
     else (* TODO4-1 *)
       error "Inference of annotation not yet implemented in this case" in
   let args = extended_rel_list (-n) cs.cs_args in
-  let ci = applist (mkMutConstruct cs.cs_cstr, cs.cs_params@args) in
+  let ci = applist (mkConstruct cs.cs_cstr, cs.cs_params@args) in
 
   (* This is the problem: finding P s.t. cs_args |- (P realargs ci) = p' *)
   (Array.map (lift (-n)) cs.cs_concl_realargs, ci, p')
@@ -837,7 +842,7 @@ let abstract_conclusion typ cs =
   let (sign,p) = decompose_prod_n n typ in
   lam_it p sign
 
-let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) =
+let infer_predicate env isevars typs cstrs ((mis,_) as indf) =
   (* Il faudra substituer les isevars a un certain moment *)
   if Array.length cstrs = 0 then (* "TODO4-3" *)
     error "Inference of annotation for empty inductive types not implemented"
@@ -850,7 +855,7 @@ let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) =
     let eqns = array_map2 prepare_unif_pb typs cstrs in
     (* First strategy: no dependencies at all *)
 (*    let (cclargs,_,typn) = eqns.(mis_nconstr mis -1) in*)
-    let (sign,_) = get_arity indf in
+    let (sign,_) = get_arity env indf in
     let mtyp =
       if array_exists is_Type typs then
 	(* Heuristic to avoid comparison between non-variables algebric univs*)
@@ -861,7 +866,7 @@ let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) =
     if array_for_all (fun (_,_,typ) -> the_conv_x_leq env isevars typ mtyp) eqns
     then
       (* Non dependent case -> turn it into a (dummy) dependent one *)
-      let sign = (Anonymous,None,build_dependent_inductive indf)::sign in
+      let sign = (Anonymous,None,build_dependent_inductive env indf)::sign in
       let pred = it_mkLambda_or_LetIn (lift (List.length sign) mtyp) sign in
       (true,pred) (* true = dependent -- par défaut *)
     else
@@ -870,7 +875,7 @@ let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) =
       let predpred = it_mkLambda_or_LetIn (mkSort s) sign in
       let caseinfo = make_default_case_info mis in
       let brs = array_map2 abstract_conclusion typs cstrs in
-      let predbody = mkMutCase (caseinfo, (nf_betaiota predpred), mkRel 1, brs) in
+      let predbody = mkCase (caseinfo, (nf_betaiota predpred), mkRel 1, brs) in
       let pred = it_mkLambda_or_LetIn (lift (List.length sign) mtyp) sign in
 *)
       (* "TODO4-2" *)
@@ -936,11 +941,11 @@ let abstract_predicate env sigma indf = function
   | (PrProd _ | PrCcl _ | PrNotInd _) ->
       anomaly "abstract_predicate: must be some LetIn"
   | PrLetIn ((_,copt),pred) ->
-      let sign,_ = get_arity indf in
+      let sign,_ = get_arity env indf in
       let dep = copt <> None in
       let sign' =
 	if dep then
-	  (Anonymous,None,build_dependent_inductive indf) :: sign
+	  (Anonymous,None,build_dependent_inductive env indf) :: sign
 	else sign in
       (dep, it_mkLambda_or_LetIn_name env (extract_predicate pred) sign')
 
@@ -1088,7 +1093,7 @@ let build_branch current pb eqns const_info =
       NonDepAlias current
     else
       let params = const_info.cs_params in
-      DepAlias (applist (mkMutConstruct const_info.cs_cstr, params)) in
+      DepAlias (applist (mkConstruct const_info.cs_cstr, params)) in
   let history = 
     push_history_pattern const_info.cs_nargs
       (AliasConstructor (partialci, const_info.cs_cstr))
@@ -1117,7 +1122,7 @@ let build_branch current pb eqns const_info =
      terms is relative to the current context enriched by topushs *)
   let ci =
     applist
-      (mkMutConstruct const_info.cs_cstr, 
+      (mkConstruct const_info.cs_cstr, 
        (List.map (lift const_info.cs_nargs) const_info.cs_params)
        @(extended_rel_list 0 const_info.cs_args)) in
 
@@ -1160,9 +1165,8 @@ and match_current pb (n,tm) =
 	check_all_variables typ pb.mat;
 	compile_aliases (shift_problem current pb)
     | IsInd (_,(IndType(indf,realargs) as indt)) ->
-	let mis,_ = dest_ind_family indf in
-	let mind = mis_inductive mis in
-	let cstrs = get_constructors indf in
+	let mind,_ = dest_ind_family indf in
+	let cstrs = get_constructors pb.env indf in
 	let eqns,onlydflt = group_equations mind current cstrs pb.mat in
 	if (cstrs <> [||] or not (initial_history pb.history)) & onlydflt then
 	  compile_aliases (shift_problem current pb)
@@ -1176,9 +1180,9 @@ and match_current pb (n,tm) =
 	  let (pred,typ,s) =
 	    find_predicate pb.env pb.isevars 
 	      pb.pred brtyps cstrs current indt in
-	  let ci = make_case_info mis None tags in
+	  let ci = make_case_info pb.env mind None tags in
 	  pattern_status tags,
-	  { uj_val = mkMutCase (ci, (*eta_reduce_if_rel*)(nf_betaiota pred),current,brvals);
+	  { uj_val = mkCase (ci, (*eta_reduce_if_rel*)(nf_betaiota pred),current,brvals);
 	    uj_type = typ }
 
 and compile_further pb firstnext rest =
@@ -1238,7 +1242,7 @@ let rename_env subst env =
   let n = ref (rel_context_length (rel_context env)) in
   let seen_ids = ref [] in
   process_rel_context
-    (fun env (na,c,t as d) ->
+    (fun (na,c,t as d) env ->
        let d =
 	 try
 	   let id = List.assoc !n subst in
@@ -1263,7 +1267,7 @@ let prepare_initial_alias_eqn isdep tomatchl eqn =
 	 | Anonymous -> (subst, pat::stripped_pats)
 	 | Name idpat as na ->
 	     match kind_of_term tm with
-	       | IsRel n when not (is_dependent_indtype tmtyp) & not isdep
+	       | 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
@@ -1333,15 +1337,15 @@ let rec find_row_ind = function
 exception NotCoercible
 
 let inh_coerce_to_ind isevars env ty tyi =
-  let (ntys,_) =
-    splay_prod env (evars_of isevars) (mis_arity (Global.lookup_mind_specif tyi)) in
+  let (mib,mip) = Inductive.lookup_mind_specif env tyi in
+  let (ntys,_) = splay_prod env (evars_of isevars) mip.mind_nf_arity in
    let (_,evarl) =
     List.fold_right
       (fun (na,ty) (env,evl) ->
-	 (push_rel_assum (na,ty) env,
-	    (new_isevar isevars env ty CCI)::evl))
+	 (push_rel (na,None,ty) env,
+	    (new_isevar isevars env ty)::evl))
       ntys (env,[]) in
-  let expected_typ = applist (mkMutInd tyi,evarl) in
+  let expected_typ = applist (mkInd tyi,evarl) in
      (* devrait être indifférent d'exiger leq ou pas puisque pour 
         un inductif cela doit être égal *)
   if the_conv_x_leq env isevars expected_typ ty then ty
@@ -1364,7 +1368,7 @@ let coerce_row typing_fun isevars env cstropt tomatch =
 	       error_bad_constructor_loc cloc c mind
 	     with Induc ->
 	       error_case_not_inductive_loc
-		 (loc_of_rawconstr tomatch) CCI env (evars_of isevars) j)
+		 (loc_of_rawconstr tomatch) env (evars_of isevars) j)
       | None -> 
 	  try IsInd (typ,find_rectype env (evars_of isevars) typ)
 	  with Induc -> NotInd (None,typ)
@@ -1384,7 +1388,7 @@ let build_expected_arity env isevars isdep tomatchl =
   let cook n = function
     | _,IsInd (_,IndType(indf,_)) ->
         let indf' = lift_inductive_family n indf in
-	Some (build_dependent_inductive indf', fst (get_arity indf'))
+	Some (build_dependent_inductive env indf', fst (get_arity env indf'))
     | _,NotInd _ -> None
   in
   let rec buildrec n env = function
@@ -1414,7 +1418,7 @@ let build_initial_predicate env sigma isdep pred tomatchl =
     | c,NotInd _ -> None, Some (lift n c) in
   let decomp_lam_force p =
     match kind_of_term p with
-      | IsLambda (_,_,c) -> c
+      | Lambda (_,_,c) -> c
       | _ -> (* eta-expansion *) applist (lift 1 p, [mkRel 1]) in
   let rec strip_and_adjust nargs pred =
     if nargs = 0 then
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index e44bda7d21..3126198f9a 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -13,7 +13,7 @@ open Names
 open Term
 open Evd
 open Environ
-open Inductive
+open Inductiveops
 open Rawterm
 open Evarutil
 (*i*)
@@ -32,7 +32,7 @@ exception PatternMatchingError of env * pattern_matching_error
 (* Used for old cases in pretyping *)
 
 val branch_scheme : 
-  env -> 'a evar_defs -> bool -> inductive_family -> constr array
+  env -> 'a evar_defs -> bool -> inductive * constr list -> constr array
 
 val pred_case_ml_onebranch : loc -> env -> 'c evar_map -> bool ->
   inductive_type -> int * unsafe_judgment -> constr 
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index c4f5b13a42..96af71ce6a 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -137,10 +137,9 @@ let red_allowed flags stack rk =
 open RedFlags
 
 let red_allowed_ref flags stack = function
-  | FarRelBinding _ -> red_allowed flags stack fDELTA
-  | VarBinding id -> red_allowed flags stack (fVAR id)
-  | EvarBinding _ -> red_allowed flags stack fEVAR
-  | ConstBinding sp -> red_allowed flags stack (fCONST sp)
+  | FarRelKey _ -> red_allowed flags stack fDELTA
+  | VarKey id -> red_allowed flags stack (fVAR id)
+  | ConstKey sp -> red_allowed flags stack (fCONST sp)
 
 (* Transfer application lists from a value to the stack
  * useful because fixpoints may be totally applied in several times
@@ -190,7 +189,7 @@ let cofixp_reducible redfun flgs _ stk =
 
 let mindsp_nparams env (sp,i) =
   let mib = lookup_mind sp env in
-  (Declarations.mind_nth_type_packet mib i).Declarations.mind_nparams
+  mib.Declarations.mind_packets.(i).Declarations.mind_nparams
 
 (* The main recursive functions
  *
@@ -207,17 +206,17 @@ let rec norm_head info env t stack =
   (* no reduction under binders *)
   match kind_of_term t with
   (* stack grows (remove casts) *)
-  | IsApp (head,args) -> (* Applied terms are normalized immediately;
+  | 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)
-  | IsMutCase (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack))
-  | IsCast (ct,_) -> norm_head info env ct 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
 
   (* constants, axioms
    * the first pattern is CRUCIAL, n=0 happens very often:
    * when reducing closed terms, n is always 0 *)
-  | IsRel i -> (match expand_rel i env with
+  | Rel i -> (match expand_rel i env with
                 | Inl (0,v) ->
                     reduce_const_body (cbv_norm_more info env) v stack
                 | Inl (n,v) ->
@@ -226,18 +225,14 @@ let rec norm_head info env t stack =
                 | Inr (n,None) ->
 		    (VAL(0, mkRel n), stack)
                 | Inr (n,Some p) ->
-		    norm_head_ref (n-p) info env stack (FarRelBinding p))
+		    norm_head_ref (n-p) info env stack (FarRelKey p))
 
-  | IsVar id -> norm_head_ref 0 info env stack (VarBinding id)
+  | Var id -> norm_head_ref 0 info env stack (VarKey id)
 
-  | IsConst sp ->
-      norm_head_ref 0 info env stack (ConstBinding sp)
+  | Const sp ->
+      norm_head_ref 0 info env stack (ConstKey sp)
 
-  | IsEvar (ev,args) ->
-      let evar = (ev, Array.map (cbv_norm_term info env) args) in
-      norm_head_ref 0 info env stack (EvarBinding evar)
-
-  | IsLetIn (x, b, t, c) ->
+  | LetIn (x, b, t, c) ->
       (* zeta means letin are contracted; delta without zeta means we *)
       (* allow substitution but leave let's in place *)
       let zeta = red_allowed (info_flags info) stack fZETA in
@@ -256,14 +251,14 @@ let rec norm_head info env t stack =
 	(VAL(0,normt), stack) (* Considérer une coupure commutative ? *)
 
   (* non-neutral cases *)
-  | IsLambda (x,a,b) -> (LAM(x,a,b,env), stack)
-  | IsFix fix -> (FIXP(fix,env,[]), stack)
-  | IsCoFix cofix -> (COFIXP(cofix,env,[]), stack)
-  | IsMutConstruct c -> (CONSTR(c, []), stack)
+  | 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)
 
   (* neutral cases *)
-  | (IsSort _ | IsMeta _ | IsMutInd _) -> (VAL(0, t), stack)
-  | IsProd (x,t,c) -> 
+  | (Sort _ | Meta _ | Ind _|Evar _) -> (VAL(0, t), stack)
+  | Prod (x,t,c) -> 
       (VAL(0, mkProd (x, cbv_norm_term info env t,
 		      cbv_norm_term info (subs_lift env) c)),
 	     stack)
@@ -277,11 +272,9 @@ and norm_head_ref k info env stack normt =
   else (VAL(0,make_constr_ref k info normt), stack)
 
 and make_constr_ref n info = function
-  | FarRelBinding p -> mkRel (n+p)
-  | VarBinding id -> mkVar id
-  | EvarBinding (ev,args) ->
-      mkEvar (ev,Array.map (cbv_norm_term info (ESID 0)) args)
-  | ConstBinding cst -> mkConst cst
+  | FarRelKey p -> mkRel (n+p)
+  | VarKey id -> mkVar id
+  | ConstKey cst -> mkConst cst
 
 (* cbv_stack_term performs weak reduction on constr t under the subs
  * env, with context stack, i.e. ([env]t stack).  First computes weak
@@ -311,9 +304,9 @@ and cbv_stack_term info stack env t =
 
     (* constructor in a Case -> IOTA
        (use red_under because we know there is a Case) *)
-    | (CONSTR((sp,n),_), APP(args,CASE(_,br,(arity,_),env,stk)))
+    | (CONSTR((sp,n),_), APP(args,CASE(_,br,ci,env,stk)))
             when red_under (info_flags info) fIOTA ->
-	let real_args = snd (list_chop arity args) in
+	let real_args = snd (list_chop ci.ci_npar args) in
         cbv_stack_term info (stack_app real_args stk) env br.(n-1)
          
     (* constructor of arity 0 in a Case -> IOTA ( "   " )*)
@@ -349,7 +342,7 @@ and apply_stack info t = function
       apply_stack info (applistc t (List.map (cbv_norm_value info) args)) st
   | CASE (ty,br,ci,env,st) ->
       apply_stack info
-        (mkMutCase (ci, cbv_norm_term info env ty, t,
+        (mkCase (ci, cbv_norm_term info env ty, t,
 		    Array.map (cbv_norm_term info env) br))
         st
 
@@ -382,7 +375,7 @@ and cbv_norm_value info = function (* reduction under binders *)
         (List.map (cbv_norm_value info) args)
   | CONSTR (c,args) ->
       applistc
-        (mkMutConstruct c)
+        (mkConstruct c)
         (List.map (cbv_norm_value info) args)
 
 (* with profiling *)
@@ -390,12 +383,11 @@ let cbv_norm infos constr =
   with_stats (lazy (cbv_norm_term infos (ESID 0) constr))
 
 
-type 'a cbv_infos = (cbv_value, 'a) infos
+type cbv_infos = cbv_value infos
 
 (* constant bodies are normalized at the first expansion *)
-let create_cbv_infos flgs env sigma =
+let create_cbv_infos flgs env =
   create
     (fun old_info c -> cbv_stack_term old_info TOP (ESID 0) c)
     flgs
     env
-    sigma
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index d787111370..000ed4e3f7 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -22,9 +22,9 @@ open Esubst
 (*s Call-by-value reduction *)
 
 (* Entry point for cbv normalization of a constr *)
-type 'a cbv_infos
-val create_cbv_infos : flags -> env -> 'a evar_map -> 'a cbv_infos
-val cbv_norm : 'a cbv_infos -> constr -> constr
+type cbv_infos
+val create_cbv_infos : flags -> env -> cbv_infos
+val cbv_norm : cbv_infos -> constr -> constr
 
 (***********************************************************************)
 (*i This is for cbv debug *)
@@ -52,12 +52,12 @@ val reduce_const_body :
   (cbv_value -> cbv_value) -> cbv_value -> cbv_stack -> cbv_value * cbv_stack
 
 (* recursive functions... *)
-val cbv_stack_term : 'a cbv_infos ->
+val cbv_stack_term : cbv_infos ->
   cbv_stack -> cbv_value subs -> constr -> cbv_value
-val cbv_norm_term : 'a cbv_infos -> cbv_value subs -> constr -> constr
-val cbv_norm_more : 'a cbv_infos -> cbv_value subs -> cbv_value -> cbv_value
-val norm_head : 'a cbv_infos ->
+val cbv_norm_term : cbv_infos -> cbv_value subs -> constr -> constr
+val cbv_norm_more : cbv_infos -> cbv_value subs -> cbv_value -> cbv_value
+val norm_head : cbv_infos ->
   cbv_value subs -> constr -> cbv_stack -> cbv_value * cbv_stack
-val apply_stack : 'a cbv_infos -> constr -> cbv_stack -> constr
-val cbv_norm_value : 'a cbv_infos -> cbv_value -> constr
+val apply_stack : cbv_infos -> constr -> cbv_stack -> constr
+val cbv_norm_value : cbv_infos -> cbv_value -> constr
 (* End of cbv debug section i*)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 18bb390990..9df00372c0 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -12,11 +12,13 @@ open Util
 open Pp
 open Options
 open Names
+open Nametab
 open Environ
 open Libobject
 open Library
 open Declare
 open Term
+open Termops
 open Rawterm
 
 (* usage qque peu general: utilise aussi dans record *)
@@ -189,14 +191,14 @@ let _ =
 
 let constructor_at_head t = 
   let rec aux t' = match kind_of_term t' with
-    | IsVar id -> CL_SECVAR (find_section_variable id),0
-    | IsConst sp -> CL_CONST sp,0
-    | IsMutInd ind_sp -> CL_IND ind_sp,0
-    | IsProd (_,_,c) -> CL_FUN,0
-    | IsLetIn (_,_,_,c) -> aux c
-    | IsSort _ -> CL_SORT,0
-    | IsCast (c,_) -> aux (collapse_appl c)
-    | IsApp (f,args) -> let c,_ = aux f in c, Array.length args
+    | Var id -> CL_SECVAR id,0
+    | Const sp -> CL_CONST sp,0
+    | Ind ind_sp -> CL_IND ind_sp,0
+    | Prod (_,_,c) -> CL_FUN,0
+    | LetIn (_,_,_,c) -> aux c
+    | Sort _ -> CL_SORT,0
+    | Cast (c,_) -> aux (collapse_appl c)
+    | App (f,args) -> let c,_ = aux f in c, Array.length args
     |  _ -> raise Not_found
   in 
   aux (collapse_appl t)
@@ -217,7 +219,7 @@ let class_of env sigma t =
   in
   if n = n1 then t,i else raise Not_found
 
-let class_args_of c = snd (decomp_app c)
+let class_args_of c = snd (decompose_app c)
 
 let strength_of_cl = function 
   | CL_CONST sp -> constant_or_parameter_strength sp
@@ -227,9 +229,9 @@ let strength_of_cl = function
 let string_of_class = function
   | CL_FUN -> "FUNCLASS"
   | CL_SORT -> "SORTCLASS" 
-  | CL_CONST sp -> Global.string_of_global (ConstRef sp)
-  | CL_IND sp -> Global.string_of_global (IndRef sp)
-  | CL_SECVAR sp -> Global.string_of_global (VarRef sp)
+  | CL_CONST sp -> string_of_id (id_of_global (Global.env()) (ConstRef sp))
+  | CL_IND sp -> string_of_id (id_of_global (Global.env()) (IndRef sp))
+  | CL_SECVAR sp -> string_of_id (id_of_global (Global.env()) (VarRef sp))
 
 (* coercion_value : int -> unsafe_judgment * bool *)
 
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index c68eba1ddf..eaeb25bc0e 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -10,6 +10,7 @@
 
 (*i*)
 open Names
+open Nametab
 open Term
 open Evd
 open Environ
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 84a6483417..5a540353b2 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -10,7 +10,7 @@
 open Util
 open Names
 open Term
-open Reduction
+open Reductionops
 open Environ
 open Typeops
 open Pretype_errors
@@ -32,7 +32,7 @@ let apply_coercion_args env argl funj =
     | h::restl ->
       (* On devrait pouvoir s'arranger pour qu'on ait pas à faire hnf_constr *)
   	match kind_of_term (whd_betadeltaiota env Evd.empty typ) with
-	  | IsProd (_,c1,c2) -> 
+	  | Prod (_,c1,c2) -> 
               (* Typage garanti par l'appel a app_coercion*)
 	      apply_rec (h::acc) (subst1 h c2) restl
 	  | _ -> anomaly "apply_coercion_args"
@@ -65,8 +65,8 @@ let apply_coercion env p hj typ_cl =
 let inh_app_fun env isevars j = 
   let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in
   match kind_of_term t with
-    | IsProd (_,_,_) -> j
-    | IsEvar ev when not (is_defined_evar isevars ev) ->
+    | Prod (_,_,_) -> j
+    | Evar ev when not (is_defined_evar isevars ev) ->
 	let (sigma',t) = define_evar_as_arrow (evars_of isevars) ev in
 	evars_reset_evd sigma' isevars;
 	{ uj_val = j.uj_val; uj_type = t }
@@ -88,14 +88,14 @@ let inh_tosort_force env isevars j =
 let inh_coerce_to_sort env isevars j =
   let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in
   match kind_of_term typ with
-    | IsSort s -> { utj_val = j.uj_val; utj_type = s }
-    | IsEvar ev when not (is_defined_evar isevars ev) ->
+    | Sort s -> { utj_val = j.uj_val; utj_type = s }
+    | Evar ev when not (is_defined_evar isevars ev) ->
 	let (sigma', s) = define_evar_as_sort (evars_of isevars) ev in
 	evars_reset_evd sigma' isevars;
 	{ utj_val = j.uj_val; utj_type = s }
     | _ ->
         let j1 = inh_tosort_force env isevars j in 
-	type_judgment env (evars_of isevars) j1 
+	type_judgment env (j_nf_evar (evars_of isevars) j1) 
 
 let inh_coerce_to_fail env isevars c1 hj =
   let hj' =
@@ -120,18 +120,19 @@ let rec inh_conv_coerce_to_fail env isevars hj c1 =
     with NoCoercion ->  (* try ... with _ -> ... is BAD *)
       (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
 	     kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with
-	 | IsProd (_,t1,t2), IsProd (name,u1,u2) -> 
+	 | Prod (_,t1,t2), Prod (name,u1,u2) -> 
              let v' = whd_betadeltaiota env (evars_of isevars) v in
              if (match kind_of_term v' with
-                   | IsLambda (_,v1,v2) ->
+                   | Lambda (_,v1,v2) ->
                        the_conv_x env isevars v1 u1 (* leq v1 u1? *)
                    | _  -> false)
              then 
 	       let (x,v1,v2) = destLambda v' in
-               let env1 = push_rel_assum (x,v1) env in
+               let env1 = push_rel (x,None,v1) env in
                let h2 = inh_conv_coerce_to_fail env1 isevars 
 			  {uj_val = v2; uj_type = t2 } u2 in
-               fst (abs_rel env (evars_of isevars) x v1 h2)
+               { uj_val = mkLambda (x, v1, h2.uj_val);
+                 uj_type = mkProd (x, v1, h2.uj_type) }
              else 
                (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
                (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
@@ -139,7 +140,7 @@ let rec inh_conv_coerce_to_fail env isevars hj c1 =
                let name = (match name with 
 			     | Anonymous -> Name (id_of_string "x")
                              | _ -> name) in
-               let env1 = push_rel_assum (name,u1) env in
+               let env1 = push_rel (name,None,u1) env in
                let h1 =
 		 inh_conv_coerce_to_fail env1 isevars
 		   {uj_val = mkRel 1; uj_type = (lift 1 u1) }
@@ -149,7 +150,8 @@ let rec inh_conv_coerce_to_fail env isevars hj c1 =
                            uj_type = subst1 h1.uj_val t2 }
                           u2
 	       in
-	       fst (abs_rel env (evars_of isevars) name u1 h2)
+               { uj_val = mkLambda (name, u1, h2.uj_val);
+                 uj_type = mkProd (name, u1, h2.uj_type) }
 	 | _ -> raise NoCoercion)
 
 (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
@@ -175,7 +177,7 @@ let inh_apply_rel_list apploc env isevars argjl (funloc,funj) tycon =
 	let resj = inh_app_fun env isevars resj in
         let ntyp = whd_betadeltaiota env sigma resj.uj_type in
       	match kind_of_term ntyp with
-          | IsProd (na,c1,c2) ->
+          | Prod (na,c1,c2) ->
               let hj' =
 		try 
 		  inh_conv_coerce_to_fail env isevars hj c1
@@ -185,7 +187,7 @@ let inh_apply_rel_list apploc env isevars argjl (funloc,funj) tycon =
 	      let newresj =
       		{ uj_val = applist (j_val resj, [j_val hj']);
 		  uj_type = subst1 hj'.uj_val c2 } in
-	      apply_rec (push_rel_assum (na,c1) env) (n+1) newresj restjl
+	      apply_rec (push_rel (na,None,c1) env) (n+1) newresj restjl
           | _ ->
               error_cant_apply_not_functional_loc 
 		(Rawterm.join_loc funloc loc) env sigma resj
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 2026bdb21b..405e2e16bf 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -13,87 +13,16 @@ open Util
 open Univ
 open Names
 open Term
+open Declarations
 open Inductive
 open Environ
 open Sign
 open Declare
 open Impargs
 open Rawterm
-
-(* Nouvelle version de renommage des variables (DEC 98) *)
-(* This is the algorithm to display distinct bound variables 
-
-    - Règle 1 : un nom non anonyme, même non affiché, contribue à la liste
-      des noms à éviter 
-    - Règle 2 : c'est la dépendance qui décide si on affiche ou pas
-
-    Exemple : 
-    si bool_ind = (P:bool->Prop)(f:(P true))(f:(P false))(b:bool)(P b), alors
-    il est affiché (P:bool->Prop)(P true)->(P false)->(b:bool)(P b)
-    mais f et f0 contribue à la liste des variables à éviter (en supposant 
-    que les noms f et f0 ne sont pas déjà pris)
-    Intérêt : noms homogènes dans un but avant et après Intro
-*)
-
-type used_idents = identifier list
-
-exception Occur
-
-let occur_rel p env id = 
-  try lookup_name_of_rel p env = Name id
-  with Not_found -> false (* Unbound indice : may happen in debug *)
-
-let occur_id env id0 c =
-  let rec occur n c = match kind_of_term c with
-    | IsVar id when  id=id0 -> raise Occur
-    | IsConst sp when basename sp = id0 -> raise Occur
-    | IsMutInd ind_sp
-	when basename (path_of_inductive_path ind_sp) = id0 -> raise Occur
-    | IsMutConstruct cstr_sp
-	when basename (path_of_constructor_path cstr_sp) = id0 -> raise Occur
-    | IsRel p when p>n & occur_rel (p-n) env id0 -> raise Occur
-    | _ -> iter_constr_with_binders succ occur n c
-  in 
-  try occur 1 c; false
-  with Occur -> true
-
-let next_name_not_occuring name l env_names t =
-  let rec next id =
-    if List.mem id l or occur_id env_names id t then next (lift_ident id)
-    else id
-  in 
-  match name with
-    | Name id   -> next id
-    | Anonymous -> id_of_string "_"
-
-(* Remark: Anonymous var may be dependent in Evar's contexts *)
-let concrete_name l env_names n c =
-  if n = Anonymous & not (dependent (mkRel 1) c) then
-    (None,l)
-  else
-    let fresh_id = next_name_not_occuring n l env_names c in
-    let idopt = if dependent (mkRel 1) c then (Some fresh_id) else None in
-    (idopt, fresh_id::l)
-
-let concrete_let_name l env_names n c =
-  let fresh_id = next_name_not_occuring n l env_names c in
-  (Name fresh_id, fresh_id::l)
-
-    (* Returns the list of global variables and constants in a term *)
-let global_vars_and_consts t =
-  let rec collect acc c =
-    let op, cl = splay_constr c in
-    let acc' = Array.fold_left collect acc cl in
-    match op with
-    | OpVar id -> id::acc'
-    | OpConst sp -> (basename sp)::acc'
-    | OpMutInd ind_sp -> (basename (path_of_inductive_path ind_sp))::acc'
-    | OpMutConstruct csp -> (basename (path_of_constructor_path csp))::acc'
-    | _ -> acc'
-  in
-  list_uniquize (collect [] t)
-    
-let used_of = global_vars_and_consts
+open Nameops
+open Termops
+open Nametab
 
 (****************************************************************************)
 (* Tools for printing of Cases                                              *)
@@ -101,23 +30,20 @@ let used_of = global_vars_and_consts
 let encode_inductive ref =
   let indsp = match ref with
     | IndRef indsp -> indsp
-    | _ -> errorlabstrm "indsp_of_id"
-        [< 'sTR ((Global.string_of_global ref)^" is not an inductive type") >]
-  in
-  let mis = Global.lookup_mind_specif indsp in
-  let constr_lengths = Array.map List.length (mis_recarg mis) in
+    | _ ->
+        let id = basename (Nametab.sp_of_global (Global.env()) ref) in
+        errorlabstrm "indsp_of_id"
+          [< pr_id id; 'sTR" is not an inductive type" >] in
+  let (mib,mip) = Global.lookup_inductive indsp in
+  let constr_lengths = Array.map List.length mip.mind_listrec in
   (indsp,constr_lengths)
 
 let constr_nargs indsp =
-  let mis = Global.lookup_mind_specif indsp in
-  let nparams = mis_nparams mis in
-  Array.map (fun t -> List.length (fst (decompose_prod_assum t)) - nparams)
-    (mis_nf_lc mis)
-
-let sp_of_spi (refsp,tyi) =
-  let mip = Declarations.mind_nth_type_packet (Global.lookup_mind refsp) tyi in
-  let (pa,_,k) = repr_path refsp in 
-  make_path pa mip.Declarations.mind_typename k
+  let (mib,mip) = Global.lookup_inductive indsp in
+  let nparams = mip.mind_nparams in
+  Array.map
+    (fun t -> List.length (fst (decompose_prod_assum t)) - nparams)
+    mip.mind_nf_lc
 
 (* Parameterization of the translation from constr to ast      *)
 
@@ -142,7 +68,8 @@ module PrintingCasesMake =
     let check (_,lc) =
       if not (Test.test lc) then 
 	errorlabstrm "check_encode" [< 'sTR Test.error_message >]
-    let printer (spi,_) = [< 'sTR(string_of_path (sp_of_spi spi)) >]
+    let printer (ind,_) =
+      pr_id (basename (path_of_inductive (Global.env()) ind))
     let key = Goptions.SecondaryTable ("Printing",Test.field)
     let title = Test.title
     let member_message = Test.member_message
@@ -155,13 +82,12 @@ module PrintingCasesIf =
     let error_message = "This type cannot be seen as a boolean type"
     let field = "If"
     let title = "Types leading to pretty-printing of Cases using a `if' form: "
-    let member_message id = function
-      | true  -> 
-          "Cases on elements of " ^ (Global.string_of_global id)
-          ^ " are printed using a `if' form"
-      | false -> 
-          "Cases on elements of " ^ (Global.string_of_global id)
-          ^ " are not printed using `if' form"
+    let member_message ref b =
+      let s = string_of_id (basename (sp_of_global (Global.env()) ref)) in
+      if b then
+        "Cases on elements of " ^ s ^ " are printed using a `if' form"
+      else
+        "Cases on elements of " ^ s ^ " are not printed using `if' form"
   end)
 
 module PrintingCasesLet =
@@ -171,21 +97,22 @@ module PrintingCasesLet =
     let field = "Let"
     let title = 
       "Types leading to a pretty-printing of Cases using a `let' form:"
-    let member_message id = function
-      | true  -> 
-          "Cases on elements of " ^ (Global.string_of_global id)
-          ^ " are printed using a `let' form"
-      | false -> 
-          "Cases on elements of " ^ (Global.string_of_global id)
-          ^ " are not printed using a `let' form"
+    let member_message ref b =
+      let s = string_of_id (basename (sp_of_global (Global.env()) ref)) in
+      if b then
+        "Cases on elements of " ^ s ^ " are printed using a `let' form"
+      else
+        "Cases on elements of " ^ s ^ " are not printed using a `let' form"
   end)
 
 module PrintingIf  = Goptions.MakeIdentTable(PrintingCasesIf)
 module PrintingLet = Goptions.MakeIdentTable(PrintingCasesLet)
 
-let force_let (_,(indsp,_,_,_,_)) = 
+let force_let ci =
+  let indsp = ci.ci_ind in
   let lc = constr_nargs indsp in PrintingLet.active (indsp,lc)
-let force_if (_,(indsp,_,_,_,_)) =
+let force_if ci =
+  let indsp = ci.ci_ind in
   let lc = constr_nargs indsp in PrintingIf.active (indsp,lc)
 
 (* Options for printing or not wildcard and synthetisable types *)
@@ -241,68 +168,70 @@ let computable p k =
 
 let lookup_name_as_renamed ctxt t s =
   let rec lookup avoid env_names n c = match kind_of_term c with
-    | IsProd (name,_,c') ->
+    | Prod (name,_,c') ->
 	(match concrete_name avoid env_names name c' with
            | (Some id,avoid') -> 
 	       if id=s then (Some n) 
 	       else lookup avoid' (add_name (Name id) env_names) (n+1) c'
 	   | (None,avoid')    -> lookup avoid' env_names (n+1) (pop c'))
-    | IsLetIn (name,_,_,c') ->
+    | LetIn (name,_,_,c') ->
 	(match concrete_name avoid env_names name c' with
            | (Some id,avoid') -> 
 	       if id=s then (Some n) 
 	       else lookup avoid' (add_name (Name id) env_names) (n+1) c'
 	   | (None,avoid')    -> lookup avoid' env_names (n+1) (pop c'))
-    | IsCast (c,_) -> lookup avoid env_names n c
+    | Cast (c,_) -> lookup avoid env_names n c
     | _ -> None
   in lookup (ids_of_named_context ctxt) empty_names_context 1 t
 
 let lookup_index_as_renamed t n =
   let rec lookup n d c = match kind_of_term c with
-    | IsProd (name,_,c') ->
+    | Prod (name,_,c') ->
 	  (match concrete_name [] empty_names_context name c' with
                (Some _,_) -> lookup n (d+1) c'
              | (None  ,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
-    | IsLetIn (name,_,_,c') ->
+    | LetIn (name,_,_,c') ->
 	  (match concrete_name [] empty_names_context name c' with
              | (Some _,_) -> lookup n (d+1) c'
              | (None  ,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
-    | IsCast (c,_) -> lookup n d c
+    | Cast (c,_) -> lookup n d c
     | _ -> None
   in lookup n 1 t
 
 let rec detype avoid env t =
   match kind_of_term (collapse_appl t) with
-    | IsRel n ->
+    | Rel n ->
       (try match lookup_name_of_rel n env with
 	 | Name id   -> RVar (dummy_loc, id)
 	 | Anonymous -> anomaly "detype: index to an anonymous variable"
        with Not_found ->
 	 let s = "_UNBOUND_REL_"^(string_of_int n)
 	 in RVar (dummy_loc, id_of_string s))
-    | IsMeta n -> RMeta (dummy_loc, n)
-    | IsVar id -> RVar (dummy_loc, id)
-    | IsSort (Prop c) -> RSort (dummy_loc,RProp c)
-    | IsSort (Type u) -> RSort (dummy_loc,RType (Some u))
-    | IsCast (c1,c2) ->
+    | Meta n -> RMeta (dummy_loc, n)
+    | Var id -> RVar (dummy_loc, id)
+    | Sort (Prop c) -> RSort (dummy_loc,RProp c)
+    | Sort (Type u) -> RSort (dummy_loc,RType (Some u))
+    | Cast (c1,c2) ->
 	RCast(dummy_loc,detype avoid env c1,detype avoid env c2)
-    | IsProd (na,ty,c) -> detype_binder BProd avoid env na ty c
-    | IsLambda (na,ty,c) -> detype_binder BLambda avoid env na ty c
-    | IsLetIn (na,b,_,c) -> detype_binder BLetIn avoid env na b c
-    | IsApp (f,args) ->
+    | Prod (na,ty,c) -> detype_binder BProd avoid env na ty c
+    | Lambda (na,ty,c) -> detype_binder BLambda avoid env na ty c
+    | LetIn (na,b,_,c) -> detype_binder BLetIn avoid env na b c
+    | App (f,args) ->
 	RApp (dummy_loc,detype avoid env f,array_map_to_list (detype avoid env) args)
-    | IsConst sp -> RRef (dummy_loc, ConstRef sp)
-    | IsEvar (ev,cl) ->
+    | Const sp -> RRef (dummy_loc, ConstRef sp)
+    | Evar (ev,cl) ->
 	let f = REvar (dummy_loc, ev) in
 	RApp (dummy_loc, f, List.map (detype avoid env) (Array.to_list cl))
-    | IsMutInd ind_sp ->
+    | Ind ind_sp ->
 	RRef (dummy_loc, IndRef ind_sp)
-    | IsMutConstruct cstr_sp ->
+    | Construct cstr_sp ->
 	RRef (dummy_loc, ConstructRef cstr_sp)
-    | IsMutCase (annot,p,c,bl) ->
+    | Case (annot,p,c,bl) ->
 	let synth_type = synthetize_type () in
 	let tomatch = detype avoid env c in
-	let (_,(indsp,considl,k,style,tags)) = annot in
+	let indsp = annot.ci_ind in
+        let considl = annot.ci_pp_info.cnames in
+        let k = annot.ci_pp_info.ind_nargs in
 	let consnargsl = constr_nargs indsp in
 	let pred = 
 	  if synth_type & computable p k & considl <> [||] then
@@ -324,8 +253,8 @@ let rec detype avoid env t =
 	in 
 	RCases (dummy_loc,tag,pred,[tomatch],eqnl)
 	
-    | IsFix (nvn,recdef) -> detype_fix avoid env (RFix nvn) recdef
-    | IsCoFix (n,recdef) -> detype_fix avoid env (RCoFix n) recdef
+    | Fix (nvn,recdef) -> detype_fix avoid env (RFix nvn) recdef
+    | CoFix (n,recdef) -> detype_fix avoid env (RCoFix n) recdef
 
 and detype_fix avoid env fixkind (names,tys,bodies) =
   let lfi = Array.map (fun id -> next_name_away id avoid) names in
@@ -351,15 +280,15 @@ and detype_eqn avoid env constr construct_nargs branch =
        detype avoid env b)
     else
       match kind_of_term b with
-	| IsLambda (x,_,b) -> 
+	| Lambda (x,_,b) -> 
 	    let pat,new_avoid,new_env,new_ids = make_pat x avoid env b ids in
             buildrec new_ids (pat::patlist) new_avoid new_env (n-1) b
 
-	| IsLetIn (x,_,_,b) -> 
+	| LetIn (x,_,_,b) -> 
 	    let pat,new_avoid,new_env,new_ids = make_pat x avoid env b ids in
             buildrec new_ids (pat::patlist) new_avoid new_env (n-1) b
 
-	| IsCast (c,_) ->    (* Oui, il y a parfois des cast *)
+	| Cast (c,_) ->    (* Oui, il y a parfois des cast *)
 	    buildrec ids patlist avoid env n c
 
 	| _ -> (* eta-expansion : n'arrivera plus lorsque tous les
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index f68c0356f5..f787da2ba7 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -14,6 +14,7 @@ open Term
 open Sign
 open Environ
 open Rawterm
+open Termops
 (*i*)
 
 (* [detype avoid env c] turns [c], typed in [env], into a rawconstr. *)
@@ -22,7 +23,8 @@ open Rawterm
 val detype : identifier list -> names_context -> constr -> rawconstr
 
 (* look for the index of a named var or a nondep var as it is renamed *)
-val lookup_name_as_renamed : named_context -> constr -> identifier -> int option
+val lookup_name_as_renamed :
+  named_context -> constr -> identifier -> int option
 val lookup_index_as_renamed : constr -> int -> int option
 
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 2858151c1f..6269dc9413 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -11,7 +11,7 @@
 open Util
 open Names
 open Term
-open Reduction
+open Reductionops
 open Closure
 open Instantiate
 open Environ
@@ -28,22 +28,22 @@ type flex_kind_of_term =
 
 let flex_kind_of_term c =
   match kind_of_term c with
-    | IsConst c -> MaybeFlexible (FConst c)
-    | IsRel n -> MaybeFlexible (FRel n)
-    | IsVar id -> MaybeFlexible (FVar id)
-    | IsEvar ev -> Flexible ev
+    | Const c -> MaybeFlexible (FConst c)
+    | Rel n -> MaybeFlexible (FRel n)
+    | Var id -> MaybeFlexible (FVar id)
+    | Evar ev -> Flexible ev
     | _ -> Rigid c
 
 let eval_flexible_term env = function
   | FConst c -> constant_opt_value env c
-  | FRel n -> option_app (lift n) (lookup_rel_value n env)
-  | FVar id -> lookup_named_value id env
+  | FRel n -> let (_,v,_) = lookup_rel n env in option_app (lift n) v
+  | FVar id -> let (_,v,_) = lookup_named id env in v
 
 let evar_apprec env isevars stack c =
   let rec aux s =
-    let (t,stack as s') = Reduction.apprec env (evars_of isevars) s in
+    let (t,stack as s') = Reductionops.apprec env (evars_of isevars) s in
     match kind_of_term t with
-      | IsEvar (n,_ as ev) when Evd.is_defined (evars_of isevars) n ->
+      | Evar (n,_ as ev) when Evd.is_defined (evars_of isevars) n ->
 	  aux (existential_value (evars_of isevars) ev, stack)
       | _ -> (t, list_of_stack stack)
   in aux (c, append_stack (Array.of_list stack) empty_stack)
@@ -239,25 +239,25 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
     | Rigid c1, Rigid c2 -> match kind_of_term c1, kind_of_term c2 with
 	  
-	| IsCast (c1,_), _ -> evar_eqappr_x env isevars pbty (c1,l1) appr2
+	| Cast (c1,_), _ -> evar_eqappr_x env isevars pbty (c1,l1) appr2
 
-	| _, IsCast (c2,_) -> evar_eqappr_x env isevars pbty appr1 (c2,l2)
+	| _, Cast (c2,_) -> evar_eqappr_x env isevars pbty appr1 (c2,l2)
 
-	| IsSort s1, IsSort s2 when l1=[] & l2=[] -> base_sort_cmp pbty s1 s2
+	| Sort s1, Sort s2 when l1=[] & l2=[] -> base_sort_cmp pbty s1 s2
 
-	| IsLambda (na,c1,c'1), IsLambda (_,c2,c'2) when l1=[] & l2=[] -> 
+	| Lambda (na,c1,c'1), Lambda (_,c2,c'2) when l1=[] & l2=[] -> 
 	    evar_conv_x env isevars CONV c1 c2
 	    & 
 	    (let c = nf_evar (evars_of isevars) c1 in
-             evar_conv_x (push_rel_assum (na,c) env) isevars CONV c'1 c'2)
+             evar_conv_x (push_rel (na,None,c) env) isevars CONV c'1 c'2)
 
-	| IsLetIn (na,b1,t1,c'1), IsLetIn (_,b2,_,c'2) ->
+	| LetIn (na,b1,t1,c'1), LetIn (_,b2,_,c'2) ->
 	    let f1 () =
 	      evar_conv_x env isevars CONV b1 b2
 	      & 
               (let b = nf_evar (evars_of isevars) b1 in
 	       let t = nf_evar (evars_of isevars) t1 in
-               evar_conv_x (push_rel_def (na,b,t) env) isevars pbty c'1 c'2)
+               evar_conv_x (push_rel (na,Some b,t) env) isevars pbty c'1 c'2)
 	      & (List.length l1 = List.length l2)
 	      & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2)
 	    and f2 () =
@@ -267,35 +267,35 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	    in 
 	    ise_try isevars [f1; f2]
 
-	| IsLetIn (_,b1,_,c'1), _ ->(* On fait commuter les args avec le Let *)
+	| LetIn (_,b1,_,c'1), _ ->(* On fait commuter les args avec le Let *)
 	     let appr1 = evar_apprec env isevars l1 (subst1 b1 c'1)
              in evar_eqappr_x env isevars pbty appr1 appr2
 
-	| _, IsLetIn (_,b2,_,c'2) ->
+	| _, LetIn (_,b2,_,c'2) ->
 	    let appr2 = evar_apprec env isevars l2 (subst1 b2 c'2)
             in evar_eqappr_x env isevars pbty appr1 appr2
 
-	| IsProd (n,c1,c'1), IsProd (_,c2,c'2) when l1=[] & l2=[] -> 
+	| Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] -> 
             evar_conv_x env isevars CONV c1 c2
             & 
 	    (let c = nf_evar (evars_of isevars) c1 in
-	     evar_conv_x (push_rel_assum (n,c) env) isevars pbty c'1 c'2)
+	     evar_conv_x (push_rel (n,None,c) env) isevars pbty c'1 c'2)
 
-	| IsMutInd sp1, IsMutInd sp2 ->
+	| Ind sp1, Ind sp2 ->
 	    sp1=sp2
             & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2
              
-	| IsMutConstruct sp1, IsMutConstruct sp2 ->
+	| Construct sp1, Construct sp2 ->
 	    sp1=sp2
             & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2
 
-	| IsMutCase (_,p1,c1,cl1), IsMutCase (_,p2,c2,cl2) ->
+	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
 	    evar_conv_x env isevars CONV p1 p2
 	    & evar_conv_x env isevars CONV c1 c2
 	    & (array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2)
 	    & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
 
-	| IsFix (li1,(_,tys1,bds1 as recdef1)), IsFix (li2,(_,tys2,bds2)) ->
+	| Fix (li1,(_,tys1,bds1 as recdef1)), Fix (li2,(_,tys2,bds2)) ->
 	    li1=li2
 	    & (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2)
 	    & (array_for_all2
@@ -303,7 +303,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 		 bds1 bds2)
 	    & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
 	     
-	| IsCoFix (i1,(_,tys1,bds1 as recdef1)), IsCoFix (i2,(_,tys2,bds2)) ->
+	| CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) ->
 	    i1=i2 
 	    & (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2)
 	    & (array_for_all2
@@ -311,22 +311,22 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 		 bds1 bds2)
 	    & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
 
-	| (IsMeta _ | IsLambda _), _ -> false
-	| _, (IsMeta _ | IsLambda _) -> false
+	| (Meta _ | Lambda _), _ -> false
+	| _, (Meta _ | Lambda _) -> false
 
-	| (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _), _ -> false
-	| _, (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _) -> false
+	| (Ind _ | Construct _ | Sort _ | Prod _), _ -> false
+	| _, (Ind _ | Construct _ | Sort _ | Prod _) -> false
 
-	| (IsApp _ | IsMutCase _ | IsFix _ | IsCoFix _), 
-	  (IsApp _ | IsMutCase _ | IsFix _ | IsCoFix _) -> false
+	| (App _ | Case _ | Fix _ | CoFix _), 
+	  (App _ | Case _ | Fix _ | CoFix _) -> false
 
-	| (IsRel _ | IsVar _ | IsConst _ | IsEvar _), _ -> assert false
-	| _, (IsRel _ | IsVar _ | IsConst _ | IsEvar _) -> assert false
+	| (Rel _ | Var _ | Const _ | Evar _), _ -> assert false
+	| _, (Rel _ | Var _ | Const _ | Evar _) -> assert false
 
 and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) = 
   let ks =
     List.fold_left
-      (fun ks b -> (new_isevar isevars env (substl ks b) CCI) :: ks)
+      (fun ks b -> (new_isevar isevars env (substl ks b)) :: ks)
       [] bs
   in
   if (list_for_all2eq 
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 9b45a50943..06a866f482 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -12,7 +12,7 @@
 open Term
 open Sign
 open Environ
-open Reduction
+open Reductionops
 open Evarutil
 (*i*)
 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index a1432ff88d..533292ec71 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -11,13 +11,15 @@
 open Util
 open Pp
 open Names
+open Nameops
 open Univ
 open Term
+open Termops
 open Sign
 open Environ
 open Evd
 open Instantiate
-open Reduction
+open Reductionops
 open Indrec
 open Pretype_errors
 
@@ -54,7 +56,7 @@ exception Uninstantiated_evar of int
 
 let rec whd_ise sigma c =
   match kind_of_term c with
-    | IsEvar (ev,args) when Evd.in_dom sigma ev ->
+    | Evar (ev,args) when Evd.in_dom sigma ev ->
 	if Evd.is_defined sigma ev then
           whd_ise sigma (existential_value sigma (ev,args))
 	else raise (Uninstantiated_evar ev)
@@ -65,10 +67,10 @@ 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
-      | IsEvar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> 
+      | Evar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> 
 	  whrec (existential_value sigma (ev,args), l)
-      | IsCast (c,_) -> whrec (c, l)
-      | IsApp (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
+      | Cast (c,_) -> whrec (c, l)
+      | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
       | _ -> s
   in 
   whrec (c, [])
@@ -146,12 +148,12 @@ let split_evar_to_arrow sigma (ev,args) =
   let (sigma1,dom) = new_type_var evenv sigma in
   let hyps = evd.evar_hyps in
   let nvar = next_ident_away (id_of_string "x") (ids_of_named_context hyps) in
-  let newenv = push_named_assum (nvar, dom) evenv in
+  let newenv = push_named_decl (nvar, None, dom) evenv in
   let (sigma2,rng) = new_type_var newenv sigma1 in
   let prod = mkProd (named_hd newenv dom Anonymous, dom, subst_var nvar rng) in
   let sigma3 = Evd.define sigma2 ev prod in
-  let dsp = num_of_evar dom in
-  let rsp = num_of_evar rng in
+  let dsp = fst (destEvar dom) in
+  let rsp = fst (destEvar rng) in
   (sigma3, prod,
    (dsp,args), (rsp, array_cons (mkRel 1) (Array.map (lift 1) args)))
 
@@ -188,7 +190,7 @@ let do_restrict_hyps sigma ev args =
       (hyps,([],[])) args 
   in
   let sign' = List.rev rsign in
-  let env' = change_hyps (fun _ -> sign') env in
+  let env' = reset_with_named_context sign' env in
   let instance = make_evar_instance env' in
   let (sigma',nc) = new_isevar_sign env' sigma evd.evar_concl instance in
   let sigma'' = Evd.define sigma' ev nc in
@@ -241,7 +243,7 @@ let is_defined_evar isevars (n,_) = Evd.is_defined isevars.evars n
 
 (* Does k corresponds to an (un)defined existential ? *)
 let ise_undefined isevars c = match kind_of_term c with
-  | IsEvar ev -> not (is_defined_evar isevars ev)
+  | Evar ev -> not (is_defined_evar isevars ev)
   | _ -> false
 
 let need_restriction isevars args = not (array_for_all closed0 args)
@@ -259,10 +261,10 @@ let real_clean isevars ev args rhs =
   let subst = List.map (fun (x,y) -> (y,mkVar x)) (filter_unique args) in
   let rec subs k t =
     match kind_of_term t with
-      | IsRel i ->
+      | Rel i ->
  	 if i<=k then t
  	 else (try List.assoc (mkRel (i-k)) subst with Not_found -> t)
-      | IsEvar (ev,args) ->
+      | Evar (ev,args) ->
 	  let args' = Array.map (subs k) args in
 	  if need_restriction isevars args' then
 	    if Evd.is_defined isevars.evars ev then 
@@ -275,7 +277,7 @@ let real_clean isevars ev args rhs =
 	    end
 	  else
 	    mkEvar (ev,args')
-      | IsVar _ -> (try List.assoc t subst with Not_found -> t)
+      | Var _ -> (try List.assoc t subst with Not_found -> t)
       | _ -> map_constr_with_binders succ subs k t
   in
   let body = subs 0 rhs in
@@ -305,7 +307,22 @@ let make_subst env args =
 (* [new_isevar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
 
-let new_isevar isevars env typ k =
+let push_rel_context_to_named_context env =
+  let sign0 = named_context env in
+  let (subst,_,sign) =
+  Sign.fold_rel_context
+    (fun (na,c,t) (subst,avoid,sign) ->
+       let na = if na = Anonymous then Name(id_of_string"_") else na in
+       let id = next_name_away na avoid in
+       ((mkVar id)::subst,
+        id::avoid,
+	add_named_decl (id,option_app (substl subst) c,
+                        type_app (substl subst) t)
+	  sign))
+    (rel_context env) ([],ids_of_named_context sign0,sign0)
+  in (subst, reset_with_named_context sign env)
+
+let new_isevar isevars env typ =
   let subst,env' = push_rel_context_to_named_context env in
   let typ' = substl subst typ in
   let instance = make_evar_instance_with_rel env in
@@ -331,14 +348,10 @@ let new_isevar isevars env typ k =
  * ?1 would be instantiated by (le y y) but y is not in the scope of ?1
  *)
 
-let keep_rels_and_vars c = match kind_of_term c with
-  | IsVar _ | IsRel _ -> c
-  | _ -> mkImplicit   (* Mettre mkMeta ?? *)
-
 let evar_define isevars (ev,argsv) rhs =
   if occur_evar ev rhs
   then error_occur_check empty_env (evars_of isevars) ev rhs;
-  let args = List.map keep_rels_and_vars (Array.to_list argsv) in 
+  let args = Array.to_list argsv in 
   let evd = ise_map isevars ev in
   (* the substitution to invert *)
   let worklist = make_subst (evar_env evd) args in
@@ -356,17 +369,17 @@ let has_undefined_isevars isevars t =
 
 let head_is_evar isevars = 
   let rec hrec k = match kind_of_term k with
-    | IsEvar (n,_)   -> not (Evd.is_defined isevars.evars n)
-    | IsApp (f,_) -> hrec f
-    | IsCast (c,_) -> hrec c
+    | Evar (n,_)   -> not (Evd.is_defined isevars.evars n)
+    | App (f,_) -> hrec f
+    | Cast (c,_) -> hrec c
     | _ -> false
   in 
   hrec 
 
 let rec is_eliminator c = match kind_of_term c with
-  | IsApp _    -> true
-  | IsMutCase _ -> true
-  | IsCast (c,_) -> is_eliminator c
+  | App _    -> true
+  | Case _ -> true
+  | Cast (c,_) -> is_eliminator c
   | _ -> false
 
 let head_is_embedded_evar isevars c =
@@ -374,10 +387,10 @@ let head_is_embedded_evar isevars c =
 
 let head_evar = 
   let rec hrec c = match kind_of_term c with
-    | IsEvar (ev,_)       -> ev
-    | IsMutCase (_,_,c,_) -> hrec c
-    | IsApp (c,_)        -> hrec c
-    | IsCast (c,_)        -> hrec c
+    | Evar (ev,_)       -> ev
+    | Case (_,_,c,_) -> hrec c
+    | App (c,_)        -> hrec c
+    | Cast (c,_)        -> hrec c
     | _                   -> failwith "headconstant"
   in 
   hrec 
@@ -466,7 +479,7 @@ let solve_refl conv_algo env isevars ev argsv1 argsv2 =
 let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
   let t2 = nf_evar isevars.evars t2 in
   let lsp = match kind_of_term t2 with
-    | IsEvar (n2,args2 as ev2)
+    | Evar (n2,args2 as ev2)
         when not (Evd.is_defined isevars.evars n2) ->
 	if n1 = n2 then
 	  solve_refl conv_algo env isevars n1 args1 args2
@@ -522,8 +535,8 @@ let split_tycon loc env isevars = function
       let sigma = evars_of isevars in
       let t = whd_betadeltaiota env sigma c in
       match kind_of_term t with
-        | IsProd (na,dom,rng) -> Some dom, Some rng
-	| IsEvar (n,_ as ev) when not (Evd.is_defined isevars.evars n) ->
+        | Prod (na,dom,rng) -> Some dom, Some rng
+	| Evar (n,_ as ev) when not (Evd.is_defined isevars.evars n) ->
 	    let (sigma',_,evdom,evrng) = split_evar_to_arrow sigma ev in
 	    evars_reset_evd sigma' isevars;
 	    Some (mkEvar evdom), Some (mkEvar evrng)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 73dae829a1..01a2437b28 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -14,7 +14,7 @@ open Term
 open Sign
 open Evd
 open Environ
-open Reduction
+open Reductionops
 (*i*)
 
 (*s This modules provides useful functions for unification modulo evars *)
@@ -22,14 +22,14 @@ open Reduction
 (* [whd_ise] raise [Uninstantiated_evar] if an evar remains uninstantiated; *)
 (* *[whd_evar]* and *[nf_evar]* leave uninstantiated evar as is *)
 
-val nf_evar : 'a Evd.evar_map -> constr -> constr
-val j_nf_evar : 'a Evd.evar_map -> unsafe_judgment -> unsafe_judgment
+val nf_evar : 'a evar_map -> constr -> constr
+val j_nf_evar : 'a evar_map -> unsafe_judgment -> unsafe_judgment
 val jl_nf_evar :
-  'a Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list
+  'a evar_map -> unsafe_judgment list -> unsafe_judgment list
 val jv_nf_evar :
-  'a Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
+  'a evar_map -> unsafe_judgment array -> unsafe_judgment array
 val tj_nf_evar :
-  'a Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
+  'a evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
 (* Replacing all evars *)
 exception Uninstantiated_evar of int
@@ -55,7 +55,7 @@ val ise_try : 'a evar_defs -> (unit -> bool) list -> bool
 val ise_undefined : 'a evar_defs -> constr -> bool
 val has_undefined_isevars : 'a evar_defs -> constr -> bool
 
-val new_isevar : 'a evar_defs -> env -> constr -> path_kind -> constr
+val new_isevar : 'a evar_defs -> env -> constr -> constr
 
 val is_eliminator : constr -> bool
 val head_is_embedded_evar : 'a evar_defs -> constr -> bool
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
new file mode 100644
index 0000000000..a80f21b521
--- /dev/null
+++ b/pretyping/evd.ml
@@ -0,0 +1,74 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Util
+open Names
+open Term
+open Sign
+
+(* The type of mappings for existential variables *)
+
+type evar = int
+
+type evar_body =
+  | Evar_empty 
+  | Evar_defined of constr
+
+type 'a evar_info = {
+  evar_concl : constr;
+  evar_hyps : named_context;
+  evar_body : evar_body;
+  evar_info : 'a option }
+
+type 'a evar_map = 'a evar_info Intmap.t
+
+let empty = Intmap.empty
+
+let to_list evc = Intmap.fold (fun ev x acc -> (ev,x)::acc) evc []
+let dom evc = Intmap.fold (fun ev _ acc -> ev::acc) evc []
+let map evc k = Intmap.find k evc
+let rmv evc k = Intmap.remove k evc
+let remap evc k i = Intmap.add k i evc
+let in_dom evc k = Intmap.mem k evc
+
+let add evd ev newinfo =  Intmap.add ev newinfo evd
+
+let define evd ev body = 
+  let oldinfo = map evd ev in
+  let newinfo =
+    { evar_concl = oldinfo.evar_concl;
+      evar_hyps = oldinfo.evar_hyps;
+      evar_body = Evar_defined body;
+      evar_info = oldinfo.evar_info } 
+  in
+  match oldinfo.evar_body with
+    | Evar_empty -> Intmap.add ev newinfo evd
+    | _ -> anomaly "cannot define an isevar twice"
+
+(* The list of non-instantiated existential declarations *)
+
+let non_instantiated sigma = 
+  let listev = to_list sigma in
+  List.fold_left 
+    (fun l ((ev,evd) as d) -> 
+       if evd.evar_body = Evar_empty then (d::l) else l)
+    [] listev
+    
+let is_evar sigma ev = in_dom sigma ev
+
+let is_defined sigma ev =
+  let info = map sigma ev in 
+  not (info.evar_body = Evar_empty)
+
+let evar_body ev = ev.evar_body
+
+let id_of_existential ev =
+  id_of_string ("?" ^ string_of_int ev)
+
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
new file mode 100644
index 0000000000..f6192c7e50
--- /dev/null
+++ b/pretyping/evd.mli
@@ -0,0 +1,57 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Names
+open Term
+open Sign
+(*i*)
+
+(* The type of mappings for existential variables.
+   The keys are integers and the associated information is a record
+   containing the type of the evar ([evar_concl]), the context under which 
+   it was introduced ([evar_hyps]) and its definition ([evar_body]). 
+   [evar_info] is used to add any other kind of information. *)
+
+type evar = int
+
+type evar_body =
+  | Evar_empty 
+  | Evar_defined of constr
+
+type 'a evar_info = {
+  evar_concl : constr;
+  evar_hyps : named_context;
+  evar_body : evar_body;
+  evar_info : 'a option }
+
+type 'a evar_map
+
+val empty : 'a evar_map
+
+val add : 'a evar_map -> evar -> 'a evar_info -> 'a evar_map
+
+val dom : 'a evar_map -> evar list
+val map : 'a evar_map -> evar -> 'a evar_info
+val rmv : 'a evar_map -> evar -> 'a evar_map
+val remap : 'a evar_map -> evar -> 'a evar_info -> 'a evar_map
+val in_dom : 'a evar_map -> evar -> bool
+val to_list : 'a evar_map -> (evar * 'a evar_info) list
+
+val define : 'a evar_map -> evar -> constr -> 'a evar_map
+
+val non_instantiated : 'a evar_map -> (evar * 'a evar_info) list
+val is_evar : 'a evar_map -> evar -> bool
+
+val is_defined : 'a evar_map -> evar -> bool
+
+val evar_body : 'a evar_info -> evar_body
+
+val id_of_existential : evar -> identifier
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
new file mode 100644
index 0000000000..3c5e17b09a
--- /dev/null
+++ b/pretyping/indrec.ml
@@ -0,0 +1,583 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Term
+open Termops
+open Declarations
+open Inductive
+open Inductiveops
+open Instantiate
+open Environ
+open Reductionops
+open Typeops
+open Type_errors
+open Indtypes (* pour les erreurs *)
+open Declare
+open Safe_typing
+open Nametab
+
+let make_prod_dep dep env = if dep then prod_name env else mkProd
+let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
+
+(*******************************************)
+(* Building curryfied elimination          *)
+(*******************************************)
+
+(**********************************************************************)
+(* Building case analysis schemes *)
+(* Nouvelle version, plus concise mais plus coûteuse à cause de
+   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 lnamespar = mip.mind_params_ctxt in
+  let nparams = mip.mind_nparams in
+  let dep = match depopt with 
+    | None -> mip.mind_sort <> (Prop Null)
+    | Some d -> d
+  in
+  if not (List.exists ((=) kind) mip.mind_kelim) then
+    raise
+      (InductiveError
+	 (NotAllowedCaseAnalysis
+	    (dep,(new_sort_in_family kind),ind)));
+
+  let nbargsprod = mip.mind_nrealargs + 1 in
+
+  (* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *)
+  (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *)
+  let env' = push_rel_context lnamespar env in
+
+  let indf = (ind, extended_rel_list 0 lnamespar) in
+  let constrs = get_constructors env indf in
+
+  let rec add_branch env k = 
+    if k = Array.length mip.mind_consnames then
+      let nbprod = k+1 in
+      let indf = (ind,extended_rel_list nbprod lnamespar) in
+      let lnamesar,_ = get_arity env indf in
+      let ci = make_default_case_info env ind in
+      it_mkLambda_or_LetIn_name env'
+       	(lambda_create env'
+           (build_dependent_inductive env indf,
+            mkCase (ci,
+		       mkRel (nbprod+nbargsprod),
+		       mkRel 1,
+		       rel_vect nbargsprod k)))
+       	lnamesar
+    else
+      let cs = lift_constructor (k+1) constrs.(k) in
+      let t = build_branch_type env dep (mkRel (k+1)) cs in
+      mkLambda_string "f" t
+	(add_branch (push_rel (Anonymous, None, t) env) (k+1))
+  in
+  let typP = make_arity env' dep indf (new_sort_in_family kind) in
+  it_mkLambda_or_LetIn_name env 
+    (mkLambda_string "P" typP
+       (add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar
+    
+(* check if the type depends recursively on one of the inductive scheme *)
+
+(**********************************************************************)
+(* Building the recursive elimination *)
+
+(*
+ * t is the type of the constructor co and recargs is the information on 
+ * the recursive calls. (It is assumed to be in form given by the user).
+ * build the type of the corresponding branch of the recurrence principle
+ * assuming f has this type, branch_rec gives also the term 
+ *   [x1]..[xk](f xi (F xi) ...) to be put in the corresponding branch of 
+ * the case operation
+ * FPvect gives for each inductive definition if we want an elimination 
+ * on it with which predicate and which recursive function. 
+ *)
+
+let type_rec_branch dep env sigma (vargs,depPvect,decP) tyi cs recargs = 
+  let make_prod = make_prod_dep dep in
+  let nparams = List.length vargs in
+  let process_pos env depK pk =
+    let rec prec env i sign p =
+      let p',largs = whd_betadeltaiota_nolet_stack env sigma p in
+      match kind_of_term p' with
+	| Prod (n,t,c) ->
+	    let d = (n,None,t) in
+	    make_prod env (n,t,prec (push_rel d env) (i+1) (d::sign) c)
+	| LetIn (n,b,t,c) ->
+	    let d = (n,Some b,t) in
+	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::sign) c)
+     	| Ind (_,_) ->
+	    let (_,realargs) = list_chop nparams largs in
+	    let base = applist (lift i pk,realargs) in
+            if depK then 
+	      mkApp (base, [|applist (mkRel (i+1),extended_rel_list 0 sign)|])
+            else 
+	      base
+      	| _ -> assert false 
+    in
+    prec env 0 []
+  in
+  let rec process_constr env i c recargs nhyps li =
+    if nhyps > 0 then match kind_of_term c with 
+      | Prod (n,t,c_0) ->
+          let (optionpos,rest) = 
+	    match recargs with 
+	      | [] -> None,[] 
+	      | Param _ :: rest -> (None,rest)
+	      | Norec :: rest   -> (None,rest)
+	      | Imbr _ :: rest  -> 
+		  warning "Ignoring recursive call"; (None,rest) 
+	      | Mrec j :: rest -> (depPvect.(j),rest)
+	  in 
+          (match optionpos with 
+	     | None -> 
+		 make_prod env
+		   (n,t,
+		    process_constr (push_rel (n,None,t) env) (i+1) c_0 rest
+		      (nhyps-1) (i::li))
+             | Some(dep',p) -> 
+		 let nP = lift (i+1+decP) p in
+		 let t_0 = process_pos env dep' nP (lift 1 t) in 
+		 make_prod_dep (dep or dep') env
+                   (n,t,
+		    mkArrow t_0
+		      (process_constr
+			 (push_rel (n,None,t)
+			    (push_rel (Anonymous,None,t_0) env))
+			 (i+2) (lift 1 c_0) rest (nhyps-1) (i::li))))
+      | LetIn (n,b,t,c_0) ->
+	  mkLetIn (n,b,t,
+		   process_constr
+		     (push_rel (n,Some b,t) env)
+		     (i+1) c_0 recargs (nhyps-1) li)
+      | _ -> assert false
+    else
+      if dep then
+	let realargs = List.map (fun k -> mkRel (i-k)) (List.rev li) in
+        let params = List.map (lift i) vargs in
+        let co = applist (mkConstruct cs.cs_cstr,params@realargs) in
+	mkApp (c, [|co|])
+      else c
+(*
+    let c', largs = whd_stack c in
+    match kind_of_term c' with 
+      | Prod (n,t,c_0) ->
+          let (optionpos,rest) = 
+	    match recargs with 
+	      | [] -> None,[] 
+	      | Param _ :: rest -> (None,rest)
+	      | Norec :: rest   -> (None,rest)
+	      | Imbr _ :: rest  -> 
+		  warning "Ignoring recursive call"; (None,rest) 
+	      | Mrec j :: rest -> (depPvect.(j),rest)
+	  in 
+          (match optionpos with 
+	     | None -> 
+		 make_prod env
+		   (n,t,
+		    process_constr (push_rel (n,None,t) env) (i+1) c_0 rest 
+		      (mkApp (lift 1 co, [|mkRel 1|])))
+             | Some(dep',p) -> 
+		 let nP = lift (i+1+decP) p in
+		 let t_0 = process_pos env dep' nP (lift 1 t) in 
+		 make_prod_dep (dep or dep') env
+                   (n,t,
+		    mkArrow t_0
+		      (process_constr
+			 (push_rel (n,None,t)
+			    (push_rel (Anonymous,None,t_0) env))
+			 (i+2) (lift 1 c_0) rest
+			 (mkApp (lift 2 co, [|mkRel 2|])))))
+      | LetIn (n,b,t,c_0) ->
+	  mkLetIn (n,b,t,
+		   process_constr
+		     (push_rel (n,Some b,t) env)
+		     (i+1) c_0 recargs (lift 1 co))
+
+      | Ind ((_,tyi),_) -> 
+      	  let nP = match depPvect.(tyi) with 
+	    | Some(_,p) -> lift (i+decP) p
+	    | _ -> assert false in
+      	  let (_,realargs) = list_chop nparams largs in
+      	  let base = applist (nP,realargs) in
+          if dep then mkApp (base, [|co|]) else base
+      | _ -> assert false
+*)
+  in
+  let nhyps = List.length cs.cs_args in
+  let nP = match depPvect.(tyi) with 
+    | Some(_,p) -> lift (nhyps+decP) p
+    | _ -> assert false in
+  let base = appvect (nP,cs.cs_concl_realargs) in
+  let c = it_mkProd_or_LetIn base cs.cs_args in
+  process_constr env 0 c recargs nhyps []
+
+let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs = 
+  let process_pos env fk  =
+    let rec prec env i hyps p =
+      let p',largs = whd_betadeltaiota_nolet_stack env sigma p in
+      match kind_of_term p' with
+	| Prod (n,t,c) ->
+	    let d = (n,None,t) in
+	    lambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c)
+	| LetIn (n,b,t,c) ->
+	    let d = (n,Some b,t) in
+	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
+     	| Ind _ -> 
+            let (_,realargs) = list_chop nparams largs
+            and arg = appvect (mkRel (i+1),extended_rel_vect 0 hyps) in 
+            applist(lift i fk,realargs@[arg])
+     	| _ -> assert false
+    in
+    prec env 0 []
+  in
+  (* ici, cstrprods est la liste des produits du constructeur instantié *)
+  let rec process_constr env i f = function
+    | (n,None,t as d)::cprest, recarg::rest -> 
+        let optionpos = 
+	  match recarg with 
+            | Param i -> None
+            | Norec   -> None
+            | Imbr _  -> None
+            | Mrec i  -> fvect.(i)
+	in 
+        (match optionpos with 
+           | None ->
+	       lambda_name env
+		 (n,t,process_constr (push_rel d env) (i+1)
+		    (whd_beta (applist (lift 1 f, [(mkRel 1)])))
+		    (cprest,rest))
+           | Some(_,f_0) -> 
+	       let nF = lift (i+1+decF) f_0 in
+	       let arg = process_pos env nF (lift 1 (body_of_type t)) in 
+               lambda_name env
+		 (n,t,process_constr (push_rel d env) (i+1)
+		    (whd_beta (applist (lift 1 f, [(mkRel 1); arg])))
+		    (cprest,rest)))
+    | (n,Some c,t as d)::cprest, rest ->
+	mkLetIn
+	  (n,c,t,
+	   process_constr (push_rel d env) (i+1) (lift 1 f)
+	     (cprest,rest))
+    | [],[] -> f
+    | _,[] | [],_ -> anomaly "process_constr"
+
+  in
+  process_constr env 0 f (List.rev cstr.cs_args, recargs)
+
+(* Main function *)
+let mis_make_indrec env sigma listdepkind (ind,mib,mip) =
+  let nparams = mip.mind_nparams in
+  let lnamespar = mip.mind_params_ctxt in
+  let nrec = List.length listdepkind in
+  let depPvec =
+    Array.create mib.mind_ntypes (None : (bool * constr) option) in 
+  let _ = 
+    let rec 
+      assign k = function 
+	| [] -> ()
+        | (indi,mibi,mipi,dep,_)::rest -> 
+            (Array.set depPvec (snd indi) (Some(dep,mkRel k));
+             assign (k-1) rest)
+    in 
+    assign nrec listdepkind  
+  in 
+  let recargsvec =
+    Array.map (fun mip -> mip.mind_listrec) mib.mind_packets in
+  let make_one_rec p =
+    let makefix nbconstruct =
+      let rec mrec i ln ltyp ldef = function
+	| (indi,mibi,mipi,dep,_)::rest ->
+	    let tyi = snd indi in
+	    let nctyi =
+              Array.length mipi.mind_consnames in (* nb constructeurs du type *) 
+
+            (* arity in the context P1..P_nrec f1..f_nbconstruct *)
+	    let args = extended_rel_list (nrec+nbconstruct) lnamespar in
+	    let indf = (indi,args) in
+	    let lnames,_ = get_arity env indf in
+
+	    let nar = mipi.mind_nrealargs in
+	    let decf = nar+nrec+nbconstruct+nrec in 
+	    let dect = nar+nrec+nbconstruct in
+	    let vecfi = rel_vect (dect+1-i-nctyi) nctyi in
+
+	    let args = extended_rel_list (decf+1) lnamespar in
+	    let constrs = get_constructors env (indi,args) in
+	    let branches = 
+	      array_map3
+		(make_rec_branch_arg env sigma (nparams,depPvec,nar+1))
+                vecfi constrs recargsvec.(tyi) in
+	    let j = (match depPvec.(tyi) with 
+		       | Some (_,c) when isRel c -> destRel c 
+		       | _ -> assert false) in
+	    let args = extended_rel_list (nrec+nbconstruct) lnamespar in
+	    let indf = (indi,args) in
+	    let deftyi = 
+	      it_mkLambda_or_LetIn_name env
+		(lambda_create env
+		   (build_dependent_inductive env
+                     (lift_inductive_family nrec indf),
+		    mkCase (make_default_case_info env indi,
+			       mkRel (dect+j+1), mkRel 1, branches)))
+		(Termops.lift_rel_context nrec lnames)
+	    in
+	    let ind = build_dependent_inductive env indf in
+	    let typtyi = 
+	      it_mkProd_or_LetIn_name env
+		(prod_create env
+		   (ind,
+		    (if dep then 
+		       let ext_lnames = (Anonymous,None,ind)::lnames in
+		       let args = extended_rel_list 0 ext_lnames in
+		       applist (mkRel (nbconstruct+nar+j+1), args)
+		     else
+		       let args = extended_rel_list 1 lnames in
+		       applist (mkRel (nbconstruct+nar+j+1), args))))
+          	lnames
+	    in 
+	    mrec (i+nctyi) (nar::ln) (typtyi::ltyp) (deftyi::ldef) rest
+        | [] -> 
+	    let fixn = Array.of_list (List.rev ln) in
+            let fixtyi = Array.of_list (List.rev ltyp) in
+            let fixdef = Array.of_list (List.rev ldef) in 
+            let names = Array.create nrec (Name(id_of_string "F")) in
+	    mkFix ((fixn,p),(names,fixtyi,fixdef))
+      in 
+      mrec 0 [] [] [] 
+    in 
+    let rec make_branch env i = function 
+      | (indi,mibi,mipi,dep,_)::rest ->
+          let tyi = snd indi in
+	  let nconstr = Array.length mipi.mind_consnames in
+	  let rec onerec env j = 
+	    if j = nconstr then 
+	      make_branch env (i+j) rest 
+	    else 
+	      let recarg = recargsvec.(tyi).(j) in
+	      let vargs = extended_rel_list (nrec+i+j) lnamespar in
+	      let indf = (indi, vargs) in
+	      let cs = get_constructor (indi,mibi,mipi,vargs) (j+1) in
+	      let p_0 =
+		type_rec_branch dep env sigma (vargs,depPvec,i+j) tyi cs recarg
+	      in 
+	      mkLambda_string "f" p_0
+		(onerec (push_rel (Anonymous,None,p_0) env) (j+1))
+	  in onerec env 0
+      | [] -> 
+	  makefix i listdepkind
+    in 
+    let rec put_arity env i = function 
+      | (indi,_,_,dep,kinds)::rest -> 
+	  let indf = make_ind_family (indi,extended_rel_list i lnamespar) in
+	  let typP = make_arity env dep indf (new_sort_in_family kinds) in
+	  mkLambda_string "P" typP
+	    (put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest)
+      | [] -> 
+	  make_branch env 0 listdepkind 
+    in 
+    let (indi,mibi,mipi,dep,kind) = List.nth listdepkind p in
+    let env' = push_rel_context lnamespar env in
+    if mis_is_recursive_subset
+      (List.map (fun (indi,_,_,_,_) -> snd indi) listdepkind) mipi
+    then 
+      it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) lnamespar
+    else 
+      mis_make_case_com (Some dep) env sigma (indi,mibi,mipi) kind 
+  in 
+  list_tabulate make_one_rec nrec
+
+(**********************************************************************)
+(* This builds elimination predicate for Case tactic *)
+
+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
+
+let make_case_dep env   = make_case_com (Some true) env
+let make_case_nodep env = make_case_com (Some false) env 
+let make_case_gen env   = make_case_com None env
+
+
+(**********************************************************************)
+(* [instanciate_indrec_scheme s rec] replace the sort of the scheme
+   [rec] by [s] *)
+
+let change_sort_arity sort = 
+  let rec drec a = match kind_of_term a with
+    | Cast (c,t) -> drec c 
+    | Prod (n,t,c) -> mkProd (n, t, drec c)
+    | Sort _ -> mkSort sort
+    | _ -> assert false
+  in 
+  drec 
+
+(* [npar] is the number of expected arguments (then excluding letin's) *)
+let instanciate_indrec_scheme sort =
+  let rec drec npar elim =
+    match kind_of_term elim with
+      | Lambda (n,t,c) -> 
+	  if npar = 0 then 
+	    mkLambda (n, change_sort_arity sort t, c)
+	  else 
+	    mkLambda (n, t, drec (npar-1) c)
+      | LetIn (n,b,t,c) -> mkLetIn (n,b,t,drec npar c)
+      | _ -> anomaly "instanciate_indrec_scheme: wrong elimination type"
+  in
+  drec
+
+(**********************************************************************)
+(* Interface to build complex Scheme *)
+
+let check_arities listdepkind = 
+  List.iter 
+    (function (indi,mibi,mipi,dep,kind) -> 
+       let id = mipi.mind_typename  in
+       let kelim = mipi.mind_kelim in
+       if not (List.exists ((=) kind) kelim) then
+	 raise
+	   (InductiveError (BadInduction (dep, id, new_sort_in_family kind))))
+    listdepkind
+
+let build_mutual_indrec env sigma = function 
+  | (mind,mib,mip,dep,s)::lrecspec ->
+      let (sp,tyi) = mind in
+      let listdepkind = 
+    	(mind,mib,mip, dep,s)::
+    	(List.map
+	   (function (mind',mibi',mipi',dep',s') ->
+	      let (sp',_) = mind' in
+	      if sp=sp' then 
+                let (mibi',mipi') = lookup_mind_specif env mind' in
+		(mind',mibi',mipi',dep',s') 
+	      else 
+		raise (InductiveError NotMutualInScheme))
+	   lrecspec)
+      in
+      let _ = check_arities listdepkind in 
+      mis_make_indrec env sigma listdepkind (mind,mib,mip)
+  | _ -> anomaly "build_indrec expects a non empty list of inductive types"
+
+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 dep = kind <> InProp in
+  List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] (ind,mib,mip))
+
+(**********************************************************************)
+(* To handle old Case/Match syntax in Pretyping                       *)
+
+(***********************************)
+(* To interpret the Match operator *)
+
+(* TODO: check that we can drop universe constraints ? *)
+let type_mutind_rec env sigma (IndType (indf,realargs) as indt) pj c = 
+  let p = pj.uj_val in
+  let (ind,params) = dest_ind_family indf in
+  let tyi = snd ind in
+  let (mib,mip) = lookup_mind_specif env ind in
+  if mis_is_recursive_subset [tyi] mip then
+    let (dep,_) = find_case_dep_nparams env (c,pj) indf in 
+    let init_depPvec i = if i = tyi then Some(dep,p) else None in
+    let depPvec = Array.init mib.mind_ntypes init_depPvec in
+    let vargs = Array.of_list params in
+    let constructors = get_constructors env indf in
+    let recargs = mip.mind_listrec in
+    let lft = array_map2 (type_rec_branch dep env sigma (params,depPvec,0) tyi)
+                constructors recargs in
+    (lft,
+     if dep then applist(p,realargs@[c]) 
+     else applist(p,realargs) )
+  else 
+    let (p,ra,_) = type_case_branches env (ind,params@realargs) pj c in
+    (p,ra)
+
+let type_rec_branches recursive env sigma indt pj c =
+  if recursive then 
+    type_mutind_rec env sigma indt pj c
+  else 
+    let IndType((ind,params),rargs) = indt in
+    let (p,ra,_) = type_case_branches env (ind,params@rargs) pj c in
+    (p,ra)
+
+
+(*s Eliminations. *)
+
+let eliminations =
+  [ (InProp,"_ind") ; (InSet,"_rec") ; (InType,"_rect") ]
+
+let elimination_suffix = function
+  | InProp -> "_ind"
+  | InSet  -> "_rec"
+  | InType -> "_rect"
+
+let make_elimination_ident id s = add_suffix id (elimination_suffix s)
+  
+let declare_one_elimination ind =
+  let (mib,mip) = Global.lookup_inductive ind in 
+  let mindstr = string_of_id mip.mind_typename in
+  let declare na c =
+    let _ = Declare.declare_constant (id_of_string na)
+      (ConstantEntry
+        { const_entry_body = c;
+          const_entry_type = None;
+          const_entry_opaque = false }, 
+       NeverDischarge) in
+    Options.if_verbose pPNL [< 'sTR na; 'sTR " is defined" >]
+  in
+  let env = Global.env () in
+  let sigma = Evd.empty in
+  let elim_scheme = build_indrec env sigma ind in
+  let npars = mip.mind_nparams in
+  let make_elim s = instanciate_indrec_scheme s npars elim_scheme in
+  let kelim = mip.mind_kelim in
+  List.iter
+    (fun (sort,suff) -> 
+       if List.mem sort kelim then
+	 declare (mindstr^suff) (make_elim (new_sort_in_family sort)))
+    eliminations
+
+let declare_eliminations sp =
+  let mib = Global.lookup_mind sp in
+(*
+  let ids = ids_of_named_context mib.mind_hyps in
+  if not (list_subset ids (ids_of_named_context (Global.named_context ()))) then    error ("Declarations of elimination scheme outside the section "^
+    "of the inductive definition is not implemented");
+*)
+  if mib.mind_finite then
+    for i = 0 to Array.length mib.mind_packets - 1 do
+      declare_one_elimination (sp,i)
+    done
+
+(* Look up function for the default elimination constant *)
+
+let lookup_eliminator ind_sp s =
+  let env = Global.env() in
+  let path = sp_of_global env (IndRef ind_sp) in
+  let dir, base = repr_path path in
+  let id = add_suffix base (elimination_suffix s) in
+  (* Try first to get an eliminator defined in the same section as the *)
+  (* inductive type *)
+  try construct_absolute_reference (Names.make_path dir id)
+  with Not_found ->
+  (* Then try to get a user-defined eliminator in some other places *)
+  (* using short name (e.g. for "eq_rec") *)
+    try construct_reference env id
+    with Not_found ->
+      errorlabstrm "default_elim"
+	[< 'sTR "Cannot find the elimination combinator :";
+           pr_id id; 'sPC;
+	   'sTR "The elimination of the inductive definition :";
+           pr_id base; 'sPC; 'sTR "on sort "; 
+           'sPC; print_sort (new_sort_in_family s) ;
+	   'sTR " is probably not allowed" >]
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
new file mode 100644
index 0000000000..7e6dd8fa1b
--- /dev/null
+++ b/pretyping/indrec.mli
@@ -0,0 +1,54 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Names
+open Term
+open Declarations
+open Inductiveops
+open Environ
+open Evd
+(*i*)
+
+(* Eliminations. *)
+
+(* These functions build elimination predicate for Case tactic *)
+
+val make_case_dep : env -> 'a evar_map -> inductive -> sorts_family -> constr
+val make_case_nodep : env -> 'a evar_map -> inductive -> sorts_family -> constr
+val make_case_gen : env -> 'a evar_map -> inductive -> sorts_family -> constr
+
+(* This builds an elimination scheme associated (using the own arity
+   of the inductive) *)
+
+val build_indrec : env -> 'a evar_map -> inductive -> constr
+val instanciate_indrec_scheme : sorts -> int -> constr -> constr
+
+(* This builds complex [Scheme] *)
+
+val build_mutual_indrec : 
+  env -> 'a evar_map ->
+    (inductive * mutual_inductive_body * one_inductive_body
+    * bool * sorts_family) list
+    -> constr list
+
+(* These are for old Case/Match typing *)
+
+val type_rec_branches : bool -> env -> 'c evar_map -> inductive_type
+  -> unsafe_judgment -> constr -> constr array * constr
+val make_rec_branch_arg : 
+  env -> 'a evar_map ->
+    int * ('b * constr) option array * int ->
+    constr -> constructor_summary -> recarg list -> constr
+
+(* *)
+val declare_eliminations : mutual_inductive -> unit
+val lookup_eliminator : inductive -> sorts_family -> constr
+val elimination_suffix : sorts_family -> string
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
new file mode 100644
index 0000000000..066df12096
--- /dev/null
+++ b/pretyping/inductiveops.ml
@@ -0,0 +1,393 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Util
+open Names
+open Univ
+open Term
+open Termops
+open Sign
+open Declarations
+open Environ
+open Reductionops
+
+(*
+type inductive_instance = {
+  mis_sp : section_path;
+  mis_mib : mutual_inductive_body;
+  mis_tyi : int;
+  mis_mip : one_inductive_body }
+
+
+let build_mis (sp,tyi) mib =
+  { mis_sp = sp; mis_mib = mib; mis_tyi = tyi;
+    mis_mip = mind_nth_type_packet mib tyi }
+
+let mis_ntypes mis = mis.mis_mib.mind_ntypes
+let mis_nparams mis = mis.mis_mip.mind_nparams
+
+let mis_index mis = mis.mis_tyi
+
+let mis_nconstr mis = Array.length (mis.mis_mip.mind_consnames)
+let mis_nrealargs mis = mis.mis_mip.mind_nrealargs
+let mis_kelim mis = mis.mis_mip.mind_kelim
+let mis_recargs mis =
+  Array.map (fun mip -> mip.mind_listrec) mis.mis_mib.mind_packets
+let mis_recarg mis = mis.mis_mip.mind_listrec
+let mis_typename mis = mis.mis_mip.mind_typename
+let mis_typepath mis =
+  make_path (dirpath mis.mis_sp) mis.mis_mip.mind_typename CCI
+let mis_consnames mis = mis.mis_mip.mind_consnames
+let mis_conspaths mis =
+  let dir = dirpath mis.mis_sp in
+  Array.map (fun id -> make_path dir id CCI) mis.mis_mip.mind_consnames
+let mis_inductive mis = (mis.mis_sp,mis.mis_tyi)
+let mis_finite mis = mis.mis_mip.mind_finite
+
+let mis_typed_nf_lc mis =
+  let sign = mis.mis_mib.mind_hyps in
+  mis.mis_mip.mind_nf_lc
+
+let mis_nf_lc mis = Array.map body_of_type (mis_typed_nf_lc mis)
+
+let mis_user_lc mis = 
+  let sign = mis.mis_mib.mind_hyps in
+  (mind_user_lc mis.mis_mip)
+
+(* gives the vector of constructors and of 
+   types of constructors of an inductive definition 
+   correctly instanciated *)
+
+let mis_type_mconstructs mispec =
+  let specif = Array.map body_of_type (mis_user_lc mispec)
+  and ntypes = mis_ntypes mispec
+  and nconstr = mis_nconstr mispec in
+  let make_Ik k = mkMutInd (mispec.mis_sp,ntypes-k-1) 
+  and make_Ck k =
+     mkMutConstruct ((mispec.mis_sp,mispec.mis_tyi),k+1) in
+  (Array.init nconstr make_Ck, 
+   Array.map (substl (list_tabulate make_Ik ntypes)) specif)
+*)
+let mis_nf_constructor_type (ind,mib,mip) j =
+  let specif = mip.mind_nf_lc
+  and ntypes = mib.mind_ntypes
+  and nconstr = Array.length mip.mind_consnames in
+  let make_Ik k = mkInd ((fst ind),ntypes-k-1) in 
+  if j > nconstr then error "Not enough constructors in the type";
+  substl (list_tabulate make_Ik ntypes) specif.(j-1)
+(*
+let mis_constructor_type i mispec = 
+  let specif = mis_user_lc mispec
+  and ntypes = mis_ntypes mispec
+  and nconstr = mis_nconstr mispec in
+  let make_Ik k = mkMutInd (mispec.mis_sp,ntypes-k-1) in 
+  if i > nconstr then error "Not enough constructors in the type";
+  substl (list_tabulate make_Ik ntypes) specif.(i-1)
+
+let mis_arity mis =
+  let hyps = mis.mis_mib.mind_hyps  in
+  mind_user_arity mis.mis_mip
+
+let mis_nf_arity mis =
+  let hyps = mis.mis_mib.mind_hyps in
+  mis.mis_mip.mind_nf_arity
+
+let mis_params_ctxt mis = mis.mis_mip.mind_params_ctxt
+(*
+  let paramsign,_ =
+    decompose_prod_n_assum mis.mis_mip.mind_nparams
+      (body_of_type (mis_nf_arity mis))
+  in paramsign
+*)
+
+let mis_sort mispec = mispec.mis_mip.mind_sort
+*)
+
+(* [inductive_family] = [inductive_instance] applied to global parameters *)
+type inductive_family = inductive * constr list
+
+type inductive_type = IndType of inductive_family * constr list
+
+let liftn_inductive_family n d (mis,params) =
+  (mis, List.map (liftn n d) params)
+let lift_inductive_family n = liftn_inductive_family n 1
+
+let liftn_inductive_type n d (IndType (indf, realargs)) =
+  IndType (liftn_inductive_family n d indf, List.map (liftn n d) realargs)
+let lift_inductive_type n = liftn_inductive_type n 1
+
+let substnl_ind_family l n (mis,params) =
+  (mis, List.map (substnl l n) params)
+
+let substnl_ind_type l n (IndType (indf,realargs)) =
+  IndType (substnl_ind_family l n indf, List.map (substnl l n) realargs)
+
+let make_ind_family (mis, params) = (mis,params)
+let dest_ind_family (mis,params) = (mis,params)
+
+let make_ind_type (indf, realargs) = IndType (indf,realargs)
+let dest_ind_type (IndType (indf,realargs)) = (indf,realargs)
+
+let mkAppliedInd (IndType ((ind,params), realargs)) =
+  applist (mkInd ind,params@realargs)
+
+let mis_is_recursive_subset listind mip = 
+  let rec one_is_rec rvec = 
+    List.exists
+      (function
+	 | Mrec i       -> List.mem i listind 
+         | Imbr(_,lvec) -> one_is_rec lvec
+         | Norec        -> false
+         | Param _      -> false) rvec
+  in 
+  array_exists one_is_rec mip.mind_listrec
+
+let mis_is_recursive (mib,mip) =
+  mis_is_recursive_subset (interval 0 (mib.mind_ntypes-1)) mip
+
+(* Annotation for cases *)
+let make_case_info env ind style pats_source =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  let print_info =
+    { cnames    = mip.mind_consnames;
+      ind_nargs = mip.mind_nrealargs;
+      style     = style;
+      source    =pats_source } in
+  { ci_ind     = ind;
+    ci_npar    = mip.mind_nparams;
+    ci_pp_info = print_info }
+
+let make_default_case_info env ind =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  make_case_info env ind None
+    (Array.map (fun _ -> RegularPat) mip.mind_consnames)
+
+(*s Useful functions *)
+
+type constructor_summary = {
+  cs_cstr : constructor;
+  cs_params : constr list;
+  cs_nargs : int;
+  cs_args : rel_context;
+  cs_concl_realargs : constr array
+}
+
+let lift_constructor n cs = {
+  cs_cstr = cs.cs_cstr;
+  cs_params = List.map (lift n) cs.cs_params;
+  cs_nargs = cs.cs_nargs;
+  cs_args = lift_rel_context n cs.cs_args;
+  cs_concl_realargs = Array.map (liftn n (cs.cs_nargs+1)) cs.cs_concl_realargs
+}
+
+let instantiate_params t args sign =
+  let rec inst s t = function
+    | ((_,None,_)::ctxt,a::args) ->
+	(match kind_of_term t with
+	   | Prod(_,_,t) -> inst (a::s) t (ctxt,args)
+	   | _ -> anomaly"instantiate_params: type, ctxt and args mismatch")
+    | ((_,(Some b),_)::ctxt,args) -> 
+	(match kind_of_term t with
+	   | LetIn(_,_,_,t) -> inst ((substl s b)::s) t (ctxt,args)
+	   | _ -> anomaly"instantiate_params: type, ctxt and args mismatch")
+    | [], [] -> substl s t
+    | _ -> anomaly"instantiate_params: type, ctxt and args mismatch"
+  in inst [] t (List.rev sign,args)
+(*
+let get_constructor_type (IndFamily (mispec,params)) j =
+  assert (j <= mis_nconstr mispec);
+  let typi = mis_constructor_type j mispec in
+  instantiate_params typi params (mis_params_ctxt mispec)
+
+let get_constructors_types (IndFamily (mispec,params) as indf) =
+  Array.init (mis_nconstr mispec) (fun j -> get_constructor_type indf (j+1))
+*)
+let get_constructor (ind,mib,mip,params) j =
+  assert (j <= Array.length mip.mind_consnames);
+  let typi = mis_nf_constructor_type (ind,mib,mip) j in
+  let typi = instantiate_params typi params mip.mind_params_ctxt in
+  let (args,ccl) = decompose_prod_assum typi in
+  let (_,allargs) = decompose_app ccl in
+  let (_,vargs) = list_chop mip.mind_nparams allargs in
+  { cs_cstr = ith_constructor_of_inductive ind j;
+    cs_params = params;
+    cs_nargs = rel_context_length args;
+    cs_args = args;
+    cs_concl_realargs = Array.of_list vargs }
+
+let get_constructors env (ind,params) =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  Array.init (Array.length mip.mind_consnames)
+    (fun j -> get_constructor (ind,mib,mip,params) (j+1))
+
+let get_arity env (ind,params) =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  let arity = body_of_type mip.mind_nf_arity in
+  destArity (prod_applist arity params)
+
+(* Functions to build standard types related to inductive *)
+let local_rels =
+  let rec relrec acc n = function (* more recent arg in front *)
+    | [] -> acc
+    | (_,None,_)::l -> relrec (mkRel n :: acc) (n+1) l
+    | (_,Some _,_)::l -> relrec acc (n+1) l
+  in relrec [] 1
+
+let build_dependent_constructor cs =
+  applist
+    (mkConstruct cs.cs_cstr,
+     (List.map (lift cs.cs_nargs) cs.cs_params)@(local_rels cs.cs_args))
+
+let build_dependent_inductive env ((ind, params) as indf) =
+  let arsign,_ = get_arity env indf in
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  let nrealargs = mip.mind_nrealargs in
+  applist 
+    (mkInd ind,
+     (List.map (lift nrealargs) params)@(local_rels arsign))
+
+(* builds the arity of an elimination predicate in sort [s] *)
+
+let make_arity env dep indf s =
+  let (arsign,_) = get_arity env indf in
+  if dep then
+    (* We need names everywhere *)
+    it_mkProd_or_LetIn_name env
+      (mkArrow (build_dependent_inductive env indf) (mkSort s)) arsign
+  else
+    (* No need to enforce names *)
+    it_mkProd_or_LetIn (mkSort s) arsign
+
+(* [p] is the predicate and [cs] a constructor summary *)
+let build_branch_type env dep p cs =
+  let base = appvect (lift cs.cs_nargs p, cs.cs_concl_realargs) in
+  if dep then
+    it_mkProd_or_LetIn_name env
+      (applist (base,[build_dependent_constructor cs]))
+      cs.cs_args
+  else
+    it_mkProd_or_LetIn base cs.cs_args
+
+(**************************************************)
+
+exception Induc
+
+let extract_mrectype t =
+  let (t, l) = decompose_app t in
+  match kind_of_term t with
+    | Ind ind -> (ind, l)
+    | _ -> raise Induc
+
+let find_mrectype env sigma c =
+  let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in
+  match kind_of_term t with
+    | Ind ind -> (ind, l)
+    | _ -> raise Induc
+
+let find_rectype env sigma c =
+  let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in
+  match kind_of_term t with
+    | Ind ind ->
+        let (mib,mip) = Inductive.lookup_mind_specif env ind in
+        let (par,rargs) = list_chop mip.mind_nparams l in
+        IndType((ind, par),rargs)
+    | _ -> raise Induc
+
+let find_inductive env sigma c =
+  let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in
+  match kind_of_term t with
+    | Ind ind
+        when (fst (Inductive.lookup_mind_specif env ind)).mind_finite ->
+        (ind, l)
+    | _ -> raise Induc
+
+let find_coinductive env sigma c =
+  let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in
+  match kind_of_term t with
+    | Ind ind
+        when not (fst (Inductive.lookup_mind_specif env ind)).mind_finite ->
+        (ind, l)
+    | _ -> raise Induc
+
+
+(***********************************************)
+(* find appropriate names for pattern variables. Useful in the
+   Case tactic. *)
+
+let is_dep_arity env kelim predty t = 
+  let rec srec (pt,t) =
+    let pt' = whd_betadeltaiota env Evd.empty pt in
+    let t' = whd_betadeltaiota env Evd.empty t in
+    match kind_of_term pt', kind_of_term t' with
+      | Prod (_,a1,a2), Prod (_,a1',a2') -> srec (a2,a2')
+      | Prod (_,a1,a2), _ -> true
+      | _ -> false in 
+  srec (predty,t)
+
+let is_dep env predty (ind,args) =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  let params = fst (list_chop mip.mind_nparams args) in
+  let kelim = mip.mind_kelim in
+  let arsign,s = get_arity env (ind,params) in
+  let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in
+  is_dep_arity env kelim predty glob_t
+
+
+
+let set_names env n brty =
+  let (args,cl) = decompose_prod_n n brty in
+  let ctxt = List.map (fun (x,ty) -> (x,None,ty)) args in
+  it_mkProd_or_LetIn_name env cl ctxt
+
+let set_pattern_names env ind brv =
+  let (_,mip) = Inductive.lookup_mind_specif env ind in
+  let arities =
+    Array.map
+      (fun c -> List.length (fst (decompose_prod c)) - mip.mind_nparams)
+      mip.mind_nf_lc in
+  array_map2 (set_names env) arities brv
+
+
+let type_case_branches_with_names env indspec pj c =
+  let (lbrty,conclty,_) = Inductive.type_case_branches env indspec pj c in
+  if is_dep env pj.uj_type indspec then
+    (set_pattern_names env (fst indspec) lbrty, conclty)
+  else (lbrty, conclty)
+
+(***********************************************)
+(* Guard condition *)
+
+(* A function which checks that a term well typed verifies both
+   syntaxic conditions *)
+
+let control_only_guard env = 
+  let rec control_rec c = match kind_of_term c with
+    | Rel _ | Var _    -> ()
+    | Sort _ | Meta _ -> ()
+    | Ind _       -> ()
+    | Construct _ -> ()
+    | Const _        -> ()
+    | CoFix (_,(_,tys,bds) as cofix) ->
+	Inductive.check_cofix env cofix;
+	Array.iter control_rec tys;
+	Array.iter control_rec bds;
+    | Fix (_,(_,tys,bds) as fix) ->
+	Inductive.check_fix env fix; 
+	Array.iter control_rec tys;
+	Array.iter control_rec bds;
+    | Case(_,p,c,b) ->control_rec p;control_rec c;Array.iter control_rec b
+    | Evar (_,cl)         -> Array.iter control_rec cl
+    | App (_,cl)         -> Array.iter control_rec cl
+    | Cast (c1,c2)       -> control_rec c1; control_rec c2
+    | Prod (_,c1,c2)     -> control_rec c1; control_rec c2
+    | Lambda (_,c1,c2)   -> control_rec c1; control_rec c2
+    | LetIn (_,c1,c2,c3) -> control_rec c1; control_rec c2; control_rec c3
+  in 
+  control_rec 
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
new file mode 100644
index 0000000000..7ca5b8b1bb
--- /dev/null
+++ b/pretyping/inductiveops.mli
@@ -0,0 +1,86 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Names
+open Term
+open Declarations
+open Sign
+open Environ
+open Evd
+
+val mis_nf_constructor_type :
+  (section_path * 'a) * mutual_inductive_body *
+  one_inductive_body -> int -> constr
+
+type inductive_family = inductive * constr list
+and inductive_type = IndType of inductive_family * constr list
+val liftn_inductive_family :
+  int -> int -> 'a * constr list -> 'a * constr list
+val lift_inductive_family :
+  int -> 'a * constr list -> 'a * constr list
+val liftn_inductive_type : int -> int -> inductive_type -> inductive_type
+val lift_inductive_type : int -> inductive_type -> inductive_type
+val substnl_ind_family :
+  constr list -> int -> 'a * constr list -> 'a * constr list
+val substnl_ind_type :
+  constr list -> int -> inductive_type -> inductive_type
+val make_ind_family : 'a * 'b -> 'a * 'b
+val dest_ind_family : 'a * 'b -> 'a * 'b
+val make_ind_type : inductive_family * constr list -> inductive_type
+val dest_ind_type : inductive_type -> inductive_family * constr list
+val mkAppliedInd : inductive_type -> constr
+val mis_is_recursive_subset :
+  int list -> one_inductive_body -> bool
+val mis_is_recursive :
+  mutual_inductive_body * one_inductive_body ->
+  bool
+val make_case_info :
+  env -> inductive ->
+  case_style option -> pattern_source array -> case_info
+val make_default_case_info : env -> inductive -> case_info
+
+type constructor_summary = {
+  cs_cstr : constructor;
+  cs_params : constr list;
+  cs_nargs : int;
+  cs_args : 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_constructors :
+  env -> inductive * constr list -> constructor_summary array
+val get_arity :
+  env -> inductive * constr list -> arity
+val local_rels : rel_context -> constr list
+val build_dependent_constructor : constructor_summary -> constr
+val build_dependent_inductive   : env -> inductive * constr list -> constr
+val make_arity :
+  env -> bool -> inductive * constr list -> sorts -> types
+val build_branch_type :
+  env -> bool -> constr -> constructor_summary -> types
+
+exception Induc
+val extract_mrectype : constr -> inductive * constr list
+val find_mrectype :
+  env -> 'a evar_map -> constr -> inductive * constr list
+val find_rectype :
+  env -> 'a evar_map -> constr -> inductive_type
+val find_inductive :
+  env -> 'a evar_map -> constr -> inductive * constr list
+val find_coinductive :
+  env ->
+  'a evar_map -> constr -> inductive * constr list
+val type_case_branches_with_names :
+  env -> inductive * constr list -> unsafe_judgment -> constr ->
+    types array * types
+val control_only_guard : env -> types -> unit
diff --git a/pretyping/instantiate.ml b/pretyping/instantiate.ml
new file mode 100644
index 0000000000..42a4dbba7b
--- /dev/null
+++ b/pretyping/instantiate.ml
@@ -0,0 +1,65 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Term
+open Sign
+open Evd
+open Declarations
+open Environ
+
+let is_id_inst inst =
+  let is_id (id,c) = match kind_of_term c with
+    | Var id' -> id = id'
+    | _ -> false
+  in
+  List.for_all is_id inst
+
+(* Vérifier que les instances des let-in sont compatibles ?? *)
+let instantiate_sign_including_let sign args =
+  let rec instrec = function
+    | ((id,b,_) :: sign, c::args) -> (id,c) :: (instrec (sign,args))
+    | ([],[])                        -> []
+    | ([],_) | (_,[]) ->
+    anomaly "Signature and its instance do not match"
+  in 
+  instrec (sign,args)
+
+let instantiate_evar sign c args =
+  let inst = instantiate_sign_including_let sign args in
+  if is_id_inst inst then
+    c
+  else
+    replace_vars inst c
+
+(* Existentials. *)
+
+let existential_type sigma (n,args) =
+  let info = Evd.map sigma n in
+  let hyps = info.evar_hyps in
+  instantiate_evar hyps info.evar_concl (Array.to_list args)
+
+exception NotInstantiatedEvar
+
+let existential_value sigma (n,args) =
+  let info = Evd.map sigma n in
+  let hyps = info.evar_hyps in
+  match evar_body info with
+    | Evar_defined c ->
+	instantiate_evar hyps c (Array.to_list args)
+    | Evar_empty ->
+	raise NotInstantiatedEvar
+
+let existential_opt_value sigma ev =
+  try Some (existential_value sigma ev)
+  with NotInstantiatedEvar -> None
+
diff --git a/pretyping/instantiate.mli b/pretyping/instantiate.mli
new file mode 100644
index 0000000000..4f4184769a
--- /dev/null
+++ b/pretyping/instantiate.mli
@@ -0,0 +1,25 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Names
+open Term
+open Evd
+open Sign
+open Environ
+(*i*)
+
+(*s [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
+no body and [Not_found] if it does not exist in [sigma] *)
+
+exception NotInstantiatedEvar
+val existential_value : 'a evar_map -> existential -> constr
+val existential_type : 'a evar_map -> existential -> types
+val existential_opt_value : 'a evar_map -> existential -> constr option
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 253e3e579d..85d38ab4d9 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -10,10 +10,13 @@
 
 open Util
 open Names
+open Nameops
 open Term
-open Reduction
+open Termops
+open Reductionops
 open Rawterm
 open Environ
+open Nametab
 
 type constr_pattern =
   | PRef of global_reference
@@ -57,7 +60,7 @@ let label_of_ref = function
   | ConstRef sp     -> ConstNode sp
   | IndRef sp       -> IndNode sp
   | ConstructRef sp -> CstrNode sp
-  | VarRef sp       -> VarNode (basename sp)
+  | VarRef id       -> VarNode id
 
 let rec head_pattern_bound t =
   match t with
@@ -74,10 +77,10 @@ let rec head_pattern_bound t =
     | PCoFix _ -> anomaly "head_pattern_bound: not a type"
 
 let head_of_constr_reference c = match kind_of_term c with
-  | IsConst sp -> ConstNode sp
-  | IsMutConstruct sp -> CstrNode sp
-  | IsMutInd sp -> IndNode sp
-  | IsVar id -> VarNode id
+  | Const sp -> ConstNode sp
+  | Construct sp -> CstrNode sp
+  | Ind sp -> IndNode sp
+  | Var id -> VarNode id
   | _ -> anomaly "Not a rigid reference"
 
 
@@ -157,29 +160,29 @@ let matches_core convert pat c =
 
       | PMeta None, m -> sigma
 
-      | PRef (VarRef sp1), IsVar v2 when basename sp1 = v2 -> sigma
+      | PRef (VarRef v1), Var v2 when v1 = v2 -> sigma
 
-      | PVar v1, IsVar v2 when v1 = v2 -> sigma
+      | PVar v1, Var v2 when v1 = v2 -> sigma
 
       | PRef ref, _ when Declare.constr_of_reference ref = cT -> sigma
 
-      | PRel n1, IsRel n2 when n1 = n2 -> sigma
+      | PRel n1, Rel n2 when n1 = n2 -> sigma
 
-      | PSort (RProp c1), IsSort (Prop c2) when c1 = c2 -> sigma
+      | PSort (RProp c1), Sort (Prop c2) when c1 = c2 -> sigma
 
-      | PSort (RType _), IsSort (Type _) -> sigma
+      | PSort (RType _), Sort (Type _) -> sigma
 
-      | PApp (c1,arg1), IsApp (c2,arg2) ->
+      | PApp (c1,arg1), App (c2,arg2) ->
         (try array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) arg1 arg2
          with Invalid_argument _ -> raise PatternMatchingFailure)
 
-      | PProd (na1,c1,d1), IsProd(na2,c2,d2) ->
+      | PProd (na1,c1,d1), Prod(na2,c2,d2) ->
 	  sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2
 
-      | PLambda (na1,c1,d1), IsLambda(na2,c2,d2) ->
+      | PLambda (na1,c1,d1), Lambda(na2,c2,d2) ->
 	  sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2
 
-      | PLetIn (na1,c1,d1), IsLetIn(na2,c2,t2,d2) ->
+      | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) ->
 	  sorec ((na2,t2)::stk) (sorec stk sigma c1 c2) d1 d2
 
       | PRef (ConstRef _ as ref), _ when convert <> None ->
@@ -188,15 +191,15 @@ let matches_core convert pat c =
 	  if is_conv env evars c cT then sigma
 	  else raise PatternMatchingFailure
 
-      | PCase (_,a1,br1), IsMutCase (_,_,a2,br2) ->
+      | 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
           else
             raise PatternMatchingFailure
       (* À faire *)
-      |	PFix f0, IsFix f1 when f0 = f1 -> sigma
-      |	PCoFix c0, IsCoFix c1 when c0 = c1 -> sigma
+      |	PFix f0, Fix f1 when f0 = f1 -> sigma
+      |	PCoFix c0, CoFix c1 when c0 = c1 -> sigma
       | _ -> raise PatternMatchingFailure
 
   in 
@@ -223,7 +226,7 @@ let rec try_matches nocc pat = function
 (* Tries to match a subterm of [c] with [pat] *)
 let rec sub_match nocc pat c =
   match kind_of_term c with
-  | IsCast (c1,c2) ->
+  | Cast (c1,c2) ->
     (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
     | PatternMatchingFailure ->
       let (lm,lc) = try_sub_match nocc pat [c1] in
@@ -231,7 +234,7 @@ let rec sub_match nocc pat c =
     | NextOccurrence nocc ->
       let (lm,lc) = try_sub_match (nocc - 1) pat [c1] in
       (lm,mkCast (List.hd lc, c2)))
-  | IsLambda (x,c1,c2) ->
+  | Lambda (x,c1,c2) ->
     (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
     | PatternMatchingFailure ->
       let (lm,lc) = try_sub_match nocc pat [c1;c2] in
@@ -239,7 +242,7 @@ let rec sub_match nocc pat c =
     | NextOccurrence nocc ->
       let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in
       (lm,mkLambda (x,List.hd lc,List.nth lc 1)))
-  | IsProd (x,c1,c2) ->
+  | Prod (x,c1,c2) ->
     (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
     | PatternMatchingFailure ->
       let (lm,lc) = try_sub_match nocc pat [c1;c2] in
@@ -247,7 +250,7 @@ let rec sub_match nocc pat c =
     | NextOccurrence nocc ->
       let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in
       (lm,mkProd (x,List.hd lc,List.nth lc 1)))
-  | IsLetIn (x,c1,t2,c2) ->
+  | LetIn (x,c1,t2,c2) ->
     (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
     | PatternMatchingFailure ->
       let (lm,lc) = try_sub_match nocc pat [c1;t2;c2] in
@@ -255,7 +258,7 @@ let rec sub_match nocc pat c =
     | NextOccurrence nocc ->
       let (lm,lc) = try_sub_match (nocc - 1) pat [c1;t2;c2] in
       (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2)))
-  | IsApp (c1,lc) ->
+  | App (c1,lc) ->
     (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
     | PatternMatchingFailure ->
       let (lm,le) = try_sub_match nocc pat (c1::(Array.to_list lc)) in
@@ -263,16 +266,16 @@ let rec sub_match nocc pat c =
     | NextOccurrence nocc ->
       let (lm,le) = try_sub_match (nocc - 1) pat (c1::(Array.to_list lc)) in
       (lm,mkApp (List.hd le, Array.of_list (List.tl le))))
-  | IsMutCase (ci,hd,c1,lc) ->
+  | Case (ci,hd,c1,lc) ->
     (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
     | PatternMatchingFailure ->
       let (lm,le) = try_sub_match nocc pat (c1::Array.to_list lc) in
-      (lm,mkMutCaseL (ci,hd,List.hd le,List.tl le))
+      (lm,mkCase (ci,hd,List.hd le,Array.of_list (List.tl le)))
     | NextOccurrence nocc ->
       let (lm,le) = try_sub_match (nocc - 1) pat (c1::Array.to_list lc) in
-      (lm,mkMutCaseL (ci,hd,List.hd le,List.tl le)))
-  | IsMutConstruct _ | IsFix _ | IsMutInd _|IsCoFix _ |IsEvar _|IsConst _
-  | IsRel _|IsMeta _|IsVar _|IsSort _ ->
+      (lm,mkCase (ci,hd,List.hd le,Array.of_list (List.tl le))))
+  | Construct _ | Fix _ | Ind _|CoFix _ |Evar _|Const _
+  | Rel _|Meta _|Var _|Sort _ ->
     (try authorized_occ nocc ((matches pat c),mkMeta (-1)) with
     | PatternMatchingFailure -> raise (NextOccurrence nocc)
     | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1)))
@@ -301,25 +304,25 @@ let is_matching_conv env sigma pat n =
 
 let rec pattern_of_constr t =
   match kind_of_term t with
-    | IsRel n  -> PRel n
-    | IsMeta n -> PMeta (Some n)
-    | IsVar id -> PVar id
-    | IsSort (Prop c) -> PSort (RProp c)
-    | IsSort (Type _) -> PSort (RType None)
-    | IsCast (c,_)      -> pattern_of_constr c
-    | IsLetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b)
-    | IsProd (na,c,b)   -> PProd (na,pattern_of_constr c,pattern_of_constr b)
-    | IsLambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b)
-    | IsApp (f,a) -> PApp (pattern_of_constr f,Array.map pattern_of_constr a)
-    | IsConst sp         -> PRef (ConstRef sp)
-    | IsMutInd sp        -> PRef (IndRef sp)
-    | IsMutConstruct sp -> PRef (ConstructRef sp)
-    | IsEvar (n,ctxt) ->
+    | Rel n  -> PRel n
+    | Meta n -> PMeta (Some n)
+    | Var id -> PVar id
+    | Sort (Prop c) -> PSort (RProp c)
+    | Sort (Type _) -> PSort (RType None)
+    | Cast (c,_)      -> pattern_of_constr c
+    | LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b)
+    | Prod (na,c,b)   -> PProd (na,pattern_of_constr c,pattern_of_constr b)
+    | Lambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b)
+    | App (f,a) -> PApp (pattern_of_constr f,Array.map pattern_of_constr a)
+    | Const sp         -> PRef (ConstRef sp)
+    | Ind sp        -> PRef (IndRef sp)
+    | Construct sp -> PRef (ConstructRef sp)
+    | Evar (n,ctxt) ->
 	if ctxt = [||] then PEvar n
 	else PApp (PEvar n, Array.map pattern_of_constr ctxt)
-    | IsMutCase (ci,p,a,br) ->
+    | Case (ci,p,a,br) ->
 	PCase (Some (pattern_of_constr p),pattern_of_constr a,
 	       Array.map pattern_of_constr br)
-    | IsFix f -> PFix f
-    | IsCoFix _ ->
+    | Fix f -> PFix f
+    | CoFix _ ->
 	error "pattern_of_constr: (co)fix currently not supported"
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 42b6808204..4a477b8e5a 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -13,6 +13,7 @@ open Names
 open Sign
 open Term
 open Environ
+open Nametab
 (*i*)
 
 type constr_pattern =
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 2d52ad5fde..fd42ca0ba9 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -12,10 +12,11 @@ open Util
 open Names
 open Sign
 open Term
+open Termops
 open Environ
 open Type_errors
 open Rawterm
-open Inductive
+open Inductiveops
 
 type ml_case_error =
   | MlCaseAbsurd
@@ -35,14 +36,7 @@ type pretype_error =
 
 exception PretypeError of env * pretype_error
 
-(* Replacing defined evars for error messages *)
-let rec whd_evar sigma c =
-  match kind_of_term c with
-    | IsEvar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev ->
-	whd_evar sigma (Instantiate.existential_value sigma (ev,args))
-    | _ -> collapse_appl c
-
-let nf_evar sigma = Reduction.local_strong (whd_evar sigma)
+let nf_evar = Reductionops.nf_evar
 let j_nf_evar sigma j = 
   { uj_val = nf_evar sigma j.uj_val;
     uj_type = nf_evar sigma j.uj_type }
@@ -52,13 +46,22 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} =
   {utj_val=type_app (nf_evar sigma) v;utj_type=t}
 
 let env_ise sigma env =
-  map_context (nf_evar sigma) env
+  let sign = named_context env in
+  let ctxt = rel_context env in
+  let env0 = reset_with_named_context sign env in
+  Sign.fold_rel_context
+    (fun (na,b,ty) e ->
+      push_rel
+        (na, option_app (nf_evar sigma) b, nf_evar sigma ty)
+        e)
+    ctxt
+    env0
 
 (* This simplify the typing context of Cases clauses *)
 (* hope it does not disturb other typing contexts *)
 let contract env lc =
   let l = ref [] in
-  let contract_context env (na,c,t) =
+  let contract_context (na,c,t) env =
     match c with
       | Some c' when isRel c' ->
 	  l := (substl !l c') :: !l;
@@ -81,50 +84,52 @@ let contract3 env a b c = match contract env [a;b;c] with
 let raise_pretype_error (loc,ctx,sigma,te) =
   Stdpp.raise_with_loc loc (PretypeError(env_ise sigma ctx,te))
 
-let raise_located_type_error (loc,k,ctx,sigma,te) =
-  Stdpp.raise_with_loc loc (TypeError(k,env_ise sigma ctx,te))
+let raise_located_type_error (loc,ctx,sigma,te) =
+  Stdpp.raise_with_loc loc (TypeError(env_ise sigma ctx,te))
 
 
 let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty =
   let env, c, actty, expty = contract3 env c actty expty in
+  let j = j_nf_evar sigma {uj_val=c;uj_type=actty} in
   raise_located_type_error
-    (loc, CCI, env, sigma,
-     ActualType (c,nf_evar sigma actty, nf_evar sigma expty))
+    (loc, env, sigma, ActualType (j, nf_evar sigma expty))
 
 let error_cant_apply_not_functional_loc loc env sigma rator randl =
+  let ja = Array.of_list (jl_nf_evar sigma randl) in
   raise_located_type_error
-    (loc, CCI, env, sigma,
-    CantApplyNonFunctional (j_nf_evar sigma rator, jl_nf_evar sigma randl))
+    (loc, env, sigma,
+    CantApplyNonFunctional (j_nf_evar sigma rator, ja))
 
 let error_cant_apply_bad_type_loc loc env sigma (n,c,t) rator randl =
+  let ja = Array.of_list (jl_nf_evar sigma randl) in
   raise_located_type_error
-    (loc, CCI, env, sigma,
+    (loc, env, sigma,
      CantApplyBadType
        ((n,nf_evar sigma c, nf_evar sigma t),
-        j_nf_evar sigma rator, jl_nf_evar sigma randl))
+        j_nf_evar sigma rator, ja))
 
 let error_cant_find_case_type_loc loc env sigma expr =
   raise_pretype_error
     (loc, env, sigma, CantFindCaseType (nf_evar sigma expr))
 
-let error_ill_formed_branch_loc loc k env sigma c i actty expty =
+let error_ill_formed_branch_loc loc env sigma c i actty expty =
   let simp t = Reduction.nf_betaiota (nf_evar sigma t) in
   raise_located_type_error
-    (loc, k, env, sigma,
+    (loc, env, sigma,
      IllFormedBranch (nf_evar sigma c,i,simp actty, simp expty))
 
-let error_number_branches_loc loc k env sigma cj expn =
+let error_number_branches_loc loc env sigma cj expn =
   raise_located_type_error
-    (loc, k, env, sigma,
+    (loc, env, sigma,
      NumberBranches (j_nf_evar sigma cj, expn))
 
-let error_case_not_inductive_loc loc k env sigma cj =
+let error_case_not_inductive_loc loc env sigma cj =
   raise_located_type_error
-    (loc, k, env, sigma, CaseNotInductive (j_nf_evar sigma cj))
+    (loc, env, sigma, CaseNotInductive (j_nf_evar sigma cj))
 
-let error_ill_typed_rec_body_loc loc k env sigma i na jl tys =
+let error_ill_typed_rec_body_loc loc env sigma i na jl tys =
   raise_located_type_error
-    (loc, k, env, sigma,
+    (loc, env, sigma,
      IllTypedRecBody (i,na,jv_nf_evar sigma jl,
                       Array.map (nf_evar sigma) tys))
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 90d90120e7..11bf5b5312 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -15,7 +15,7 @@ open Term
 open Sign
 open Environ
 open Rawterm
-open Inductive
+open Inductiveops
 (*i*)
 
 (*s The type of errors raised by the pretyper *)
@@ -65,18 +65,18 @@ val error_cant_find_case_type_loc :
   loc -> env -> 'a Evd.evar_map -> constr -> 'b
 
 val error_case_not_inductive_loc :
-  loc -> path_kind -> env -> 'a Evd.evar_map -> unsafe_judgment -> 'b
+  loc -> env -> 'a Evd.evar_map -> unsafe_judgment -> 'b
 
 val error_ill_formed_branch_loc : 
-  loc -> path_kind -> env -> 'a Evd.evar_map ->
+  loc -> env -> 'a Evd.evar_map ->
       constr -> int -> constr -> constr -> 'b
 
 val error_number_branches_loc : 
-  loc -> path_kind -> env -> 'a Evd.evar_map ->
+  loc -> env -> 'a Evd.evar_map ->
       unsafe_judgment -> int -> 'b
 
 val error_ill_typed_rec_body_loc :
-  loc -> path_kind -> env -> 'a Evd.evar_map ->
+  loc -> env -> 'a Evd.evar_map ->
       int -> name array -> unsafe_judgment array -> types array -> 'b
 
 (*s Implicit arguments synthesis errors *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c0238dbdae..e717ffe95e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -14,7 +14,8 @@ open Names
 open Sign
 open Evd
 open Term
-open Reduction
+open Termops
+open Reductionops
 open Environ
 open Type_errors
 open Typeops
@@ -31,7 +32,9 @@ open Dyn
 
 (***********************************************************************)
 (* This concerns Cases *)
+open Declarations
 open Inductive
+open Inductiveops
 open Instantiate
 
 let lift_context n l = 
@@ -40,24 +43,27 @@ let lift_context n l =
 
 let transform_rec loc env sigma (pj,c,lf) indt = 
   let p = pj.uj_val in
-  let (indf,realargs) = dest_ind_type indt in
-  let (mispec,params) = dest_ind_family indf in
-  let mI = mkMutInd (mis_inductive mispec) in
-  let recargs = mis_recarg mispec in
-  let tyi = mis_index mispec in
-  if Array.length lf <> mis_nconstr mispec then 
+  let ((ind,params) as indf,realargs) = dest_ind_type indt in
+  let (mib,mip) = lookup_mind_specif env ind in
+  let mI = mkInd ind in
+  let recargs = mip.mind_listrec in
+  let tyi = snd ind in
+  let ci = make_default_case_info env ind in
+  let nconstr = Array.length mip.mind_consnames in
+  if Array.length lf <> nconstr then 
     (let cj = {uj_val=c; uj_type=mkAppliedInd indt} in
-     error_number_branches_loc loc CCI env sigma cj (mis_nconstr mispec));
-  if mis_is_recursive_subset [tyi] mispec then
-    let (dep,_) = find_case_dep_nparams env sigma (c,pj) indf in 
+     error_number_branches_loc loc env sigma cj nconstr);
+  if mis_is_recursive_subset [tyi] mip then
+    let (dep,_) =
+      find_case_dep_nparams env
+        (nf_evar sigma c, j_nf_evar sigma pj) indf in 
     let init_depFvec i = if i = tyi then Some(dep,mkRel 1) else None in
-    let depFvec = Array.init (mis_ntypes mispec) init_depFvec in
+    let depFvec = Array.init mib.mind_ntypes init_depFvec in
     (* build now the fixpoint *)
-    let lnames,_ = get_arity indf in
+    let lnames,_ = get_arity env indf in
     let nar = List.length lnames in
-    let nparams = mis_nparams mispec in
-    let constrs = get_constructors (lift_inductive_family (nar+2) indf) in
-    let ci = make_default_case_info mispec in
+    let nparams = mip.mind_nparams in
+    let constrs = get_constructors env (lift_inductive_family (nar+2) indf) in
     let branches = 
       array_map3
 	(fun f t reca -> 
@@ -72,7 +78,7 @@ let transform_rec loc env sigma (pj,c,lf) indt =
 	(lambda_create env
 	   (applist (mI,List.append (List.map (lift (nar+1)) params)
                        (extended_rel_list 0 lnames)),
-            mkMutCase (ci, lift (nar+2) p, mkRel 1, branches)))
+            mkCase (ci, lift (nar+2) p, mkRel 1, branches)))
         (lift_rel_context 1 lnames) 
     in
     if noccurn 1 deffix then 
@@ -98,8 +104,7 @@ let transform_rec loc env sigma (pj,c,lf) indt =
 	       ([|Name(id_of_string "F")|],[|typPfix|],[|deffix|])) in
       applist (fix,realargs@[c])
   else
-    let ci = make_default_case_info mispec in
-    mkMutCase (ci, p, c, lf)
+    mkCase (ci, p, c, lf)
 
 (***********************************************************************)
 
@@ -125,7 +130,7 @@ let evar_type_fixpoint loc env isevars lna lar vdefj =
         if not (the_conv_x_leq env isevars
 		  (vdefj.(i)).uj_type
 		  (lift lt lar.(i))) then
-          error_ill_typed_rec_body_loc loc CCI env (evars_of isevars)
+          error_ill_typed_rec_body_loc loc env (evars_of isevars)
             i lna vdefj lar
       done
 
@@ -133,7 +138,7 @@ let check_branches_message loc env isevars c (explft,lft) =
   for i = 0 to Array.length explft - 1 do
     if not (the_conv_x_leq env isevars lft.(i) explft.(i)) then 
       let sigma = evars_of isevars in
-      error_ill_formed_branch_loc loc CCI env sigma c i lft.(i) explft.(i)
+      error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
   done
 
 (* coerce to tycon if any *)
@@ -156,7 +161,7 @@ let pretype_id loc env lvar id =
     { uj_val  = mkRel n; uj_type = type_app (lift n) typ }
   with Not_found ->
   try
-    let typ = lookup_id_type id (named_context env) in
+    let (_,_,typ) = lookup_named id env in
     { uj_val  = mkVar id; uj_type = typ }
   with Not_found ->
     error_var_not_found_loc loc id
@@ -190,12 +195,12 @@ let pretype_ref _ isevars env lvar ref =
 
 | RInd (ind_sp,ctxt) ->
     let ind = (ind_sp,Array.map pretype ctxt) in
-    make_judge (mkMutInd ind) (type_of_inductive env (evars_of isevars) ind)
+    make_judge (mkInd ind) (type_of_inductive env (evars_of isevars) ind)
  
 | RConstruct (cstr_sp,ctxt) ->
     let cstr = (cstr_sp,Array.map pretype ctxt) in
     let typ = type_of_constructor env (evars_of isevars) cstr in
-    { uj_val=mkMutConstruct cstr; uj_type=typ }
+    { uj_val=mkConstruct cstr; uj_type=typ }
 *)
 let pretype_sort = function
   | RProp c -> judge_of_prop_contents c
@@ -239,7 +244,7 @@ let rec pretype tycon env isevars lvar lmeta = function
   | RHole loc ->
       if !compter then nbimpl:=!nbimpl+1;
       (match tycon with
-	 | Some ty -> { uj_val = new_isevar isevars env ty CCI; uj_type = ty }
+	 | Some ty -> { uj_val = new_isevar isevars env ty; uj_type = ty }
 	 | None ->
 	     (match loc with
 		  None -> anomaly "There is an implicit argument I cannot solve"
@@ -267,11 +272,11 @@ let rec pretype tycon env isevars lvar lmeta = function
 	match fixkind with
 	  | RFix (vn,i as vni) ->
 	      let fix = (vni,(names,lara,Array.map j_val vdefj)) in
-	      check_fix env (evars_of isevars) fix;
+	      check_fix env fix;
 	      make_judge (mkFix fix) lara.(i)
 	  | RCoFix i -> 
 	      let cofix = (i,(names,lara,Array.map j_val vdefj)) in
-	      check_cofix env (evars_of isevars) cofix;
+	      check_cofix env cofix;
 	      make_judge (mkCoFix cofix) lara.(i) in
       inh_conv_coerce_to_tycon loc env isevars fixj tycon
 
@@ -289,7 +294,7 @@ let rec pretype tycon env isevars lvar lmeta = function
             let resty =
               whd_betadeltaiota env (evars_of isevars) resj.uj_type in
       	    match kind_of_term resty with
-	      | IsProd (na,c1,c2) ->
+	      | Prod (na,c1,c2) ->
 		  let hj = pretype (mk_tycon c1) env isevars lvar lmeta c in
 		  let newresj =
       		    { uj_val = applist (j_val resj, [j_val hj]);
@@ -321,10 +326,9 @@ let rec pretype tycon env isevars lvar lmeta = function
       let (dom,rng) = split_tycon loc env isevars tycon in
       let dom_valcon = valcon_of_tycon dom in
       let j = pretype_type dom_valcon env isevars lvar lmeta c1 in
-      let var = (name,j.utj_val) in
-      let j' = pretype rng (push_rel_assum var env) isevars lvar lmeta c2 
-      in 
-      fst (abs_rel env (evars_of isevars) name j.utj_val j')
+      let var = (name,None,j.utj_val) in
+      let j' = pretype rng (push_rel var env) isevars lvar lmeta c2 in 
+      judge_of_abstraction env name j j'
 
   | RProd(loc,name,c1,c2)        ->
       let j = pretype_type empty_valcon env isevars lvar lmeta c1 in
@@ -332,15 +336,15 @@ let rec pretype tycon env isevars lvar lmeta = function
       let env' = push_rel_assum var env in
       let j' = pretype_type empty_valcon env' isevars lvar lmeta c2 in
       let resj =
-	try fst (gen_rel env (evars_of isevars) name j j')
+	try fst (judge_of_product env name j j')
 	with TypeError _ as e -> Stdpp.raise_with_loc loc e in
       inh_conv_coerce_to_tycon loc env isevars resj tycon
 	
   | RLetIn(loc,name,c1,c2)      ->
       let j = pretype empty_tycon env isevars lvar lmeta c1 in
-      let var = (name,j.uj_val,j.uj_type) in
+      let var = (name,Some j.uj_val,j.uj_type) in
         let tycon = option_app (lift 1) tycon in
-      let j' = pretype tycon (push_rel_def var env) isevars lvar lmeta c2 in
+      let j' = pretype tycon (push_rel var env) isevars lvar lmeta c2 in
       { uj_val = mkLetIn (name, j.uj_val, j.uj_type, j'.uj_val) ;
 	uj_type = type_app (subst1 j.uj_val) j'.uj_type }
       
@@ -349,7 +353,7 @@ let rec pretype tycon env isevars lvar lmeta = function
       let (IndType (indf,realargs) as indt) = 
 	try find_rectype env (evars_of isevars) cj.uj_type
 	with Induc ->
-          error_case_not_inductive_loc loc CCI env (evars_of isevars) cj in
+          error_case_not_inductive_loc loc env (evars_of isevars) cj in
       let pj = match po with
 	| Some p -> pretype empty_tycon env isevars lvar lmeta p
 	| None -> 
@@ -382,8 +386,7 @@ let rec pretype tycon env isevars lvar lmeta = function
 	      findtype 0 in
       let pj = j_nf_evar (evars_of isevars) pj in
 
-      let (dep,_) = find_case_dep_nparams env (evars_of isevars)
-        (cj.uj_val,pj) indf in
+      let (dep,_) = find_case_dep_nparams env (cj.uj_val,pj) indf in
 
       let pj =
 	if dep then pj else
@@ -391,10 +394,10 @@ let rec pretype tycon env isevars lvar lmeta = function
 	  let rec decomp n p =
 	    if n=0 then p else
 	      match kind_of_term p with
-		| IsLambda (_,_,c) -> decomp (n-1) c
+		| Lambda (_,_,c) -> decomp (n-1) c
 		| _ -> decomp (n-1) (applist (lift 1 p, [mkRel 1])) in
 	  let sign,s = decompose_prod_n n pj.uj_type in
-	  let ind = build_dependent_inductive indf in
+	  let ind = build_dependent_inductive env indf in
 	  let s' = mkProd (Anonymous, ind, s) in
 	  let ccl = lift 1 (decomp n pj.uj_val) in
 	  let ccl' = mkLambda (Anonymous, ind, ccl) in
@@ -403,7 +406,7 @@ let rec pretype tycon env isevars lvar lmeta = function
 	Indrec.type_rec_branches
           isrec env (evars_of isevars) indt pj cj.uj_val in
       if Array.length bty <> Array.length lf then
-	error_number_branches_loc loc CCI env (evars_of isevars) 
+	error_number_branches_loc loc env (evars_of isevars) 
 	  cj (Array.length bty)
       else
 	let lfj =
@@ -419,8 +422,8 @@ let rec pretype tycon env isevars lvar lmeta = function
 	    transform_rec loc env (evars_of isevars)(pj,cj.uj_val,lfv) indt
 	  else
 	    let mis,_ = dest_ind_family indf in
-	    let ci = make_default_case_info mis in
-	    mkMutCase (ci, (nf_betaiota pj.uj_val), cj.uj_val,
+	    let ci = make_default_case_info env mis in
+	    mkCase (ci, (nf_betaiota pj.uj_val), cj.uj_val,
                        Array.map (fun j-> j.uj_val) lfj)
 	in
 	{uj_val = v;
@@ -456,7 +459,7 @@ and pretype_type valcon env isevars lvar lmeta = function
 	       utj_type = Retyping.get_sort_of env (evars_of isevars) v }
 	 | None ->
 	     let s = new_Type_sort () in
-	     { utj_val = new_isevar isevars env (mkSort s) CCI; utj_type = s})
+	     { utj_val = new_isevar isevars env (mkSort s); utj_type = s})
   | c ->
       let j = pretype empty_tycon env isevars lvar lmeta c in
       let tj = inh_coerce_to_sort env isevars j in
@@ -490,7 +493,7 @@ let check_evars fail_evar initial_sigma sigma c =
   let metamap = ref [] in
   let rec proc_rec c =
     match kind_of_term c with
-      | IsEvar (ev,args as k) ->
+      | Evar (ev,args as k) ->
           assert (Evd.in_dom sigma ev);
 	  if not (Evd.in_dom initial_sigma ev) then
 	    (if fail_evar then
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index c8c91a945a..d82d7fbc81 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -13,6 +13,7 @@ open Util
 open Names
 open Sign
 open Term
+open Nametab
 (*i*)
 
 (* Untyped intermediate terms, after ASTs and before constr. *)
@@ -27,6 +28,8 @@ type cases_pattern =
 
 type rawsort = RProp of Term.contents | RType of Univ.universe option
 
+type fix_kind = RFix of (int array * int) | RCoFix of int
+
 type binder_kind = BProd | BLambda | BLetIn
 
 type 'ctxt reference =
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 336b3ffa1e..8d5184299f 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -12,6 +12,7 @@
 open Names
 open Sign
 open Term
+open Nametab
 (*i*)
 
 (* Untyped intermediate terms, after ASTs and before constr. *)
@@ -26,6 +27,8 @@ type cases_pattern =
 
 type rawsort = RProp of Term.contents | RType of Univ.universe option
 
+type fix_kind = RFix of (int array * int) | RCoFix of int
+
 type binder_kind = BProd | BLambda | BLetIn
 
 type 'ctxt reference =
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 4c72ca1c0a..6617a7a9be 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -11,7 +11,9 @@
 open Util
 open Pp
 open Names
+open Nametab
 open Term
+open Termops
 open Typeops
 open Libobject
 open Library
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index d3811f413e..a3dd2f2a35 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -10,6 +10,7 @@
 
 (*i*)
 open Names
+open Nametab
 open Term
 open Classops
 open Libobject
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
new file mode 100644
index 0000000000..a34c47c5a4
--- /dev/null
+++ b/pretyping/reductionops.ml
@@ -0,0 +1,886 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Term
+open Termops
+open Univ
+open Evd
+open Declarations
+open Environ
+open Instantiate
+open Closure
+open Esubst
+
+exception Elimconst
+
+(* The type of (machine) states (= lambda-bar-calculus' cuts) *) 
+type state = constr * constr stack
+
+type 'a contextual_reduction_function = env -> 'a evar_map -> constr -> constr
+type 'a reduction_function = 'a contextual_reduction_function
+type local_reduction_function = constr -> constr
+
+type 'a contextual_stack_reduction_function = 
+    env -> 'a evar_map -> constr -> constr * constr list
+type 'a stack_reduction_function = 'a contextual_stack_reduction_function
+type local_stack_reduction_function = constr -> constr * constr list
+
+type 'a contextual_state_reduction_function = 
+    env -> 'a evar_map -> state -> state
+type 'a state_reduction_function = 'a contextual_state_reduction_function
+type local_state_reduction_function = state -> state
+
+(*************************************)
+(*** Reduction Functions Operators ***)
+(*************************************)
+
+let rec whd_state (x, stack as s) =
+  match kind_of_term x with
+    | App (f,cl) -> whd_state (f, append_stack cl stack)
+    | Cast (c,_)  -> whd_state (c, stack)
+    | _             -> s
+
+let appterm_of_stack (f,s) = (f,list_of_stack s)
+
+let whd_stack x = appterm_of_stack (whd_state (x, empty_stack))
+let whd_castapp_stack = whd_stack
+
+let stack_reduction_of_reduction red_fun env sigma s =
+  let t = red_fun env sigma (app_stack s) in
+  whd_stack t
+
+let strong whdfun env sigma t = 
+  let rec strongrec env t =
+    map_constr_with_full_binders push_rel strongrec env (whdfun env sigma t) in
+  strongrec env t
+
+let local_strong whdfun = 
+  let rec strongrec t = map_constr strongrec (whdfun t) in
+  strongrec
+
+let rec strong_prodspine redfun c = 
+  let x = redfun c in
+  match kind_of_term x with
+    | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun b)
+    | _ -> x
+
+(*************************************)
+(*** Reduction using substitutions ***)
+(*************************************)
+
+(* This signature is very similar to Closure.RedFlagsSig except there
+   is eta but no per-constant unfolding *)
+
+module type RedFlagsSig = sig
+  type flags
+  type flag
+  val fbeta : flag
+  val fevar : flag
+  val fdelta : flag
+  val feta : flag
+  val fiota : flag
+  val fzeta : flag
+  val mkflags : flag list -> flags
+  val red_beta : flags -> bool
+  val red_delta : flags -> bool
+  val red_evar : flags -> bool
+  val red_eta : flags -> bool
+  val red_iota : flags -> bool
+  val red_zeta : flags -> bool
+end
+
+(* Naive Implementation 
+module RedFlags = (struct
+  type flag = BETA | DELTA | EVAR | IOTA | ZETA | ETA
+  type flags = flag list
+  let fbeta = BETA 
+  let fdelta = DELTA
+  let fevar = EVAR
+  let fiota = IOTA
+  let fzeta = ZETA
+  let feta = ETA
+  let mkflags l = l
+  let red_beta = List.mem BETA
+  let red_delta = List.mem DELTA
+  let red_evar = List.mem EVAR
+  let red_eta = List.mem ETA
+  let red_iota = List.mem IOTA
+  let red_zeta = List.mem ZETA
+end : RedFlagsSig)
+*)
+
+(* Compact Implementation *)
+module RedFlags = (struct
+  type flag = int
+  type flags = int
+  let fbeta = 1
+  let fdelta = 2
+  let fevar = 4
+  let feta = 8 
+  let fiota = 16
+  let fzeta = 32
+  let mkflags = List.fold_left (lor) 0
+  let red_beta f = f land fbeta <> 0
+  let red_delta f = f land fdelta <> 0
+  let red_evar f = f land fevar <> 0
+  let red_eta f = f land feta <> 0
+  let red_iota f = f land fiota <> 0
+  let red_zeta f = f land fzeta <> 0
+end : RedFlagsSig)
+
+open RedFlags
+
+(* Local *)
+let beta = mkflags [fbeta]
+let evar = mkflags [fevar]
+let betaevar = mkflags [fevar; fbeta]
+let betaiota = mkflags [fiota; fbeta]
+let betaiotazeta = mkflags [fiota; fbeta;fzeta]
+
+(* Contextual *)
+let delta = mkflags [fdelta;fevar]
+let betadelta = mkflags [fbeta;fdelta;fzeta;fevar]
+let betadeltaeta = mkflags [fbeta;fdelta;fzeta;fevar;feta]
+let betadeltaiota = mkflags [fbeta;fdelta;fzeta;fevar;fiota]
+let betadeltaiota_nolet = mkflags [fbeta;fdelta;fevar;fiota]
+let betadeltaiotaeta = mkflags [fbeta;fdelta;fzeta;fevar;fiota;feta]
+let betaiotaevar = mkflags [fbeta;fiota;fevar]
+let betaetalet = mkflags [fbeta;feta;fzeta]
+
+(* Beta Reduction tools *)
+
+let rec stacklam recfun env t stack =
+  match (decomp_stack stack,kind_of_term t) with
+    | Some (h,stacktl), Lambda (_,_,c) -> stacklam recfun (h::env) c stacktl
+    | _ -> recfun (substl env t, stack)
+
+let beta_applist (c,l) =
+  stacklam app_stack [] c (append_stack (Array.of_list l) empty_stack)
+
+(* Iota reduction tools *)
+
+type 'a miota_args = {
+  mP      : constr;     (* the result type *)
+  mconstr : constr;     (* the constructor *)
+  mci     : case_info;  (* special info to re-build pattern *)
+  mcargs  : 'a list;    (* the constructor's arguments *)
+  mlf     : 'a array }  (* the branch code vector *)
+		       
+let reducible_mind_case c = match kind_of_term c with
+  | Construct _ | CoFix _ -> true
+  | _  -> false
+
+let contract_cofix (bodynum,(types,names,bodies as typedbodies)) =
+  let nbodies = Array.length bodies in
+  let make_Fi j = mkCoFix (nbodies-j-1,typedbodies) in
+  substl (list_tabulate make_Fi nbodies) bodies.(bodynum)
+
+let reduce_mind_case mia =
+  match kind_of_term mia.mconstr with
+    | Construct (ind_sp,i as cstr_sp) ->
+(*	let ncargs = (fst mia.mci).(i-1) in*)
+	let real_cargs = snd (list_chop mia.mci.ci_npar mia.mcargs) in
+        applist (mia.mlf.(i-1),real_cargs)
+    | CoFix cofix ->
+	let cofix_def = contract_cofix cofix in
+	mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
+    | _ -> assert false
+
+(* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce
+   Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *)
+
+let contract_fix ((recindices,bodynum),(types,names,bodies as typedbodies)) =
+  let nbodies = Array.length recindices in
+  let make_Fi j = mkFix ((recindices,nbodies-j-1),typedbodies) in
+  substl (list_tabulate make_Fi nbodies) bodies.(bodynum)
+
+let fix_recarg ((recindices,bodynum),_) stack =
+  assert (0 <= bodynum & bodynum < Array.length recindices);
+  let recargnum = Array.get recindices bodynum in
+  try 
+    Some (recargnum, stack_nth stack recargnum)
+  with Not_found ->
+    None
+
+type fix_reduction_result = NotReducible | Reduced of state
+
+let reduce_fix whdfun fix stack =
+  match fix_recarg fix stack with
+    | None -> NotReducible
+    | Some (recargnum,recarg) ->
+        let (recarg'hd,_ as recarg') = whdfun (recarg, empty_stack) in
+        let stack' = stack_assign stack recargnum (app_stack recarg') in
+	(match kind_of_term recarg'hd with
+           | Construct _ -> Reduced (contract_fix fix, stack')
+	   | _ -> NotReducible)
+
+(* Generic reduction function *)
+
+(* Y avait un commentaire pour whd_betadeltaiota :
+
+   NB : Cette fonction alloue peu c'est l'appel 
+     ``let (c,cargs) = whfun (recarg, empty_stack)''
+                              -------------------
+   qui coute cher *)
+
+let rec whd_state_gen flags env sigma = 
+  let rec whrec (x, stack as s) =
+    match kind_of_term x with
+      | Rel n when red_delta flags ->
+	  (match lookup_rel n env with
+	     | (_,Some body,_) -> whrec (lift n body, stack)
+	     | _ -> s)
+      | Var id when red_delta flags ->
+	  (match lookup_named id env with
+	     | (_,Some body,_) -> whrec (body, stack)
+	     | _ -> s)
+      | Evar ev when red_evar flags ->
+	  (match existential_opt_value sigma ev with
+	     | Some body -> whrec (body, stack)
+	     | None -> s)
+      | Const const when red_delta flags ->
+	  (match constant_opt_value env const with
+	     | Some  body -> whrec (body, stack)
+	     | None -> s)
+      | LetIn (_,b,_,c) when red_zeta flags -> stacklam whrec [b] c stack
+      | Cast (c,_) -> whrec (c, stack)
+      | App (f,cl)  -> whrec (f, append_stack cl stack)
+      | Lambda (na,t,c) ->
+          (match decomp_stack stack with
+             | Some (a,m) when red_beta flags -> stacklam whrec [a] c m
+             | None when red_eta flags ->
+		 let env' = push_rel (na,None,t) env in
+		 let whrec' = whd_state_gen flags env' sigma in
+                 (match kind_of_term (app_stack (whrec' (c, empty_stack))) with
+                    | App (f,cl) ->
+			let napp = Array.length cl in
+			if napp > 0 then
+			  let x', l' = whrec' (array_last cl, empty_stack) in
+                          match kind_of_term x', decomp_stack l' with
+                            | Rel 1, None ->
+				let lc = Array.sub cl 0 (napp-1) in
+				let u = if napp=1 then f else appvect (f,lc) in
+				if noccurn 1 u then (pop u,empty_stack) else s
+                            | _ -> s
+			else s
+		    | _ -> s)
+	     | _ -> s)
+
+      | Case (ci,p,d,lf) when red_iota flags ->
+          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)
+            
+      | Fix fix when red_iota flags ->
+	  (match reduce_fix whrec fix stack with
+             | Reduced s' -> whrec s'
+	     | NotReducible -> s)
+
+      | x -> s
+  in 
+  whrec
+
+let local_whd_state_gen flags = 
+  let rec whrec (x, stack as s) =
+    match kind_of_term x with
+      | LetIn (_,b,_,c) when red_zeta flags -> stacklam whrec [b] c stack
+      | Cast (c,_) -> whrec (c, stack)
+      | App (f,cl)  -> whrec (f, append_stack cl stack)
+      | Lambda (_,_,c) ->
+          (match decomp_stack stack with
+             | Some (a,m) when red_beta flags -> stacklam whrec [a] c m
+             | None when red_eta flags ->
+                 (match kind_of_term (app_stack (whrec (c, empty_stack))) with 
+                    | App (f,cl) ->
+			let napp = Array.length cl in
+			if napp > 0 then
+			  let x', l' = whrec (array_last cl, empty_stack) in
+                          match kind_of_term x', decomp_stack l' with
+                            | Rel 1, None ->
+				let lc = Array.sub cl 0 (napp-1) in
+				let u = if napp=1 then f else appvect (f,lc) in
+				if noccurn 1 u then (pop u,empty_stack) else s
+                            | _ -> s
+			else s
+		    | _ -> s)
+	     | _ -> s)
+
+      | Case (ci,p,d,lf) when red_iota flags ->
+          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)
+            
+      | Fix fix when red_iota flags ->
+	  (match reduce_fix whrec fix stack with
+             | Reduced s' -> whrec s'
+	     | NotReducible -> s)
+
+      | x -> s
+  in 
+  whrec
+
+(* 1. Beta Reduction Functions *)
+
+let whd_beta_state = local_whd_state_gen beta
+let whd_beta_stack x = appterm_of_stack (whd_beta_state (x, empty_stack))
+let whd_beta x = app_stack (whd_beta_state (x,empty_stack))
+
+(* Nouveau ! *)
+let whd_betaetalet_state = local_whd_state_gen betaetalet
+let whd_betaetalet_stack x =
+  appterm_of_stack (whd_betaetalet_state (x, empty_stack))
+let whd_betaetalet x = app_stack (whd_betaetalet_state (x,empty_stack))
+
+(* 2. Delta Reduction Functions *)
+
+let whd_delta_state e = whd_state_gen delta e
+let whd_delta_stack env sigma x =
+  appterm_of_stack (whd_delta_state env sigma (x, empty_stack))
+let whd_delta env sigma c =
+  app_stack (whd_delta_state env sigma (c, empty_stack))
+
+let whd_betadelta_state e = whd_state_gen betadelta e
+let whd_betadelta_stack env sigma x =
+  appterm_of_stack (whd_betadelta_state env sigma (x, empty_stack))
+let whd_betadelta env sigma c =
+  app_stack (whd_betadelta_state env sigma (c, empty_stack))
+
+let whd_betaevar_state e = whd_state_gen betaevar e
+let whd_betaevar_stack env sigma c =
+  appterm_of_stack (whd_betaevar_state env sigma (c, empty_stack))
+let whd_betaevar env sigma c =
+  app_stack (whd_betaevar_state env sigma (c, empty_stack))
+
+
+let whd_betadeltaeta_state e = whd_state_gen betadeltaeta e
+let whd_betadeltaeta_stack env sigma x =
+  appterm_of_stack (whd_betadeltaeta_state env sigma (x, empty_stack))
+let whd_betadeltaeta env sigma x = 
+  app_stack (whd_betadeltaeta_state env sigma (x, empty_stack))
+
+(* 3. Iota reduction Functions *)
+
+let whd_betaiota_state = local_whd_state_gen betaiota
+let whd_betaiota_stack x =
+  appterm_of_stack (whd_betaiota_state (x, empty_stack))
+let whd_betaiota x =
+  app_stack (whd_betaiota_state (x, empty_stack))
+
+let whd_betaiotazeta_state = local_whd_state_gen betaiotazeta
+let whd_betaiotazeta_stack x =
+  appterm_of_stack (whd_betaiotazeta_state (x, empty_stack))
+let whd_betaiotazeta x =
+  app_stack (whd_betaiotazeta_state (x, empty_stack))
+
+let whd_betaiotaevar_state e = whd_state_gen betaiotaevar e
+let whd_betaiotaevar_stack env sigma x =
+  appterm_of_stack (whd_betaiotaevar_state env sigma (x, empty_stack))
+let whd_betaiotaevar env sigma x = 
+  app_stack (whd_betaiotaevar_state env sigma (x, empty_stack))
+
+let whd_betadeltaiota_state e = whd_state_gen betadeltaiota e
+let whd_betadeltaiota_stack env sigma x =
+  appterm_of_stack (whd_betadeltaiota_state env sigma (x, empty_stack))
+let whd_betadeltaiota env sigma x = 
+  app_stack (whd_betadeltaiota_state env sigma (x, empty_stack))
+
+let whd_betadeltaiotaeta_state e = whd_state_gen betadeltaiotaeta e
+let whd_betadeltaiotaeta_stack env sigma x =
+  appterm_of_stack (whd_betadeltaiotaeta_state env sigma (x, empty_stack))
+let whd_betadeltaiotaeta env sigma x = 
+  app_stack (whd_betadeltaiotaeta_state env sigma (x, empty_stack))
+
+let whd_betadeltaiota_nolet_state e = whd_state_gen betadeltaiota_nolet e
+let whd_betadeltaiota_nolet_stack env sigma x =
+  appterm_of_stack (whd_betadeltaiota_nolet_state env sigma (x, empty_stack))
+let whd_betadeltaiota_nolet env sigma x = 
+  app_stack (whd_betadeltaiota_nolet_state env sigma (x, empty_stack))
+
+(****************************************************************************)
+(*                   Reduction Functions                                    *)
+(****************************************************************************)
+
+(* Replacing defined evars for error messages *)
+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 ->
+	whd_evar sigma (Instantiate.existential_value sigma (ev,args))
+    | _ -> collapse_appl c
+
+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 =
+  norm_val (create_clos_infos flgs env) (inject (nf_evar sigma t))
+
+let nf_beta = clos_norm_flags Closure.beta empty_env Evd.empty
+let nf_betaiota = clos_norm_flags Closure.betaiota empty_env Evd.empty
+let nf_betadeltaiota env sigma =
+  clos_norm_flags Closure.betadeltaiota env sigma
+
+(* lazy weak head reduction functions *)
+let whd_flags flgs env sigma t =
+  whd_val (create_clos_infos flgs env) (inject (nf_evar sigma t))
+
+(********************************************************************)
+(*                         Conversion                               *)
+(********************************************************************)
+(*
+let fkey = Profile.declare_profile "fhnf";;
+let fhnf info v = Profile.profile2 fkey fhnf info v;;
+
+let fakey = Profile.declare_profile "fhnf_apply";;
+let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;;
+*)
+
+type 'a conversion_function = 
+    env -> 'a evar_map -> constr -> constr -> constraints
+
+(* Conversion utility functions *)
+
+type conversion_test = constraints -> constraints
+
+exception NotConvertible
+
+(* Convertibility of sorts *)
+
+type conv_pb = 
+  | CONV 
+  | CUMUL
+
+let pb_is_equal pb = pb = CONV
+
+let pb_equal = function
+  | CUMUL -> CONV
+  | CONV -> CONV
+
+let sort_cmp pb s0 s1 cuniv =
+  match (s0,s1) with
+    | (Prop c1, Prop c2) -> if c1 = c2 then cuniv else raise NotConvertible
+    | (Prop c1, Type u)  ->
+        (match pb with
+            CUMUL -> cuniv
+          | _ -> raise NotConvertible)
+    | (Type u1, Type u2) ->
+	(match pb with
+           | CONV -> enforce_eq u1 u2 cuniv
+	   | CUMUL -> enforce_geq u2 u1 cuniv)
+    | (_, _) -> raise NotConvertible
+
+let base_sort_cmp pb s0 s1 =
+  match (s0,s1) with
+    | (Prop c1, Prop c2) -> c1 = c2
+    | (Prop c1, Type u)  -> pb = CUMUL
+    | (Type u1, Type u2) -> true
+    | (_, _) -> false
+
+(* Conversion between  [lft1]term1 and [lft2]term2 *)
+let rec ccnv cv_pb infos lft1 lft2 term1 term2 cuniv = 
+  eqappr cv_pb infos (lft1, fhnf infos term1) (lft2, fhnf infos term2) cuniv
+
+(* Conversion between [lft1]([^n1]hd1 v1) and [lft2]([^n2]hd2 v2) *)
+and eqappr cv_pb infos appr1 appr2 cuniv =
+  let (lft1,(n1,hd1,v1)) = appr1
+  and (lft2,(n2,hd2,v2)) = appr2 in
+  let el1 = el_shft n1 lft1
+  and el2 = el_shft n2 lft2 in
+  match (fterm_of hd1, fterm_of hd2) with
+    (* case of leaves *)
+    | (FAtom a1, FAtom a2) ->
+	(match kind_of_term a1, kind_of_term a2 with
+	   | (Sort s1, Sort s2) -> 
+	       if stack_args_size v1 = 0 && stack_args_size v2 = 0
+	       then sort_cmp cv_pb s1 s2 cuniv
+               else raise NotConvertible
+	   | (Meta n, Meta m) ->
+               if n=m
+	       then convert_stacks infos lft1 lft2 v1 v2 cuniv
+               else raise NotConvertible
+	   | _ -> raise NotConvertible)
+
+    (* 2 index known to be bound to no constant *)
+    | (FRel n, FRel m) ->
+        if reloc_rel n el1 = reloc_rel m el2
+        then convert_stacks infos lft1 lft2 v1 v2 cuniv
+        else raise NotConvertible
+
+    (* 2 constants, 2 existentials or 2 local defined vars or 2 defined rels *)
+    | (FFlex fl1, FFlex fl2) ->
+	(try (* try first intensional equality *)
+	  if fl1 = fl2
+          then
+	    convert_stacks infos lft1 lft2 v1 v2 cuniv
+          else raise NotConvertible
+        with NotConvertible ->
+          (* else expand the second occurrence (arbitrary heuristic) *)
+	  match unfold_reference infos fl2 with
+            | Some def2 -> 
+		eqappr cv_pb infos appr1
+                  (lft2, fhnf_apply infos n2 def2 v2) cuniv
+             | None ->
+                 (match unfold_reference infos fl1 with
+                   | Some def1 ->
+                       eqappr cv_pb infos
+			 (lft1, fhnf_apply infos n1 def1 v1) appr2 cuniv
+		   | None -> raise NotConvertible))
+
+    (* only one constant, existential, defined var or defined rel *)
+    | (FFlex fl1, _)      ->
+        (match unfold_reference infos fl1 with
+           | Some def1 -> 
+	       eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1)
+                 appr2 cuniv
+           | None -> raise NotConvertible)
+    | (_, FFlex fl2)      ->
+        (match unfold_reference infos fl2 with
+           | Some def2 -> 
+	       eqappr cv_pb infos appr1
+                 (lft2, fhnf_apply infos n2 def2 v2)
+                 cuniv
+           | None -> raise NotConvertible)
+	
+    (* other constructors *)
+    | (FLambda (_,c1,c2,_,_), FLambda (_,c'1,c'2,_,_)) ->
+        if stack_args_size v1 = 0 && stack_args_size v2 = 0
+        then
+          let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in
+          ccnv CONV infos
+            (el_lift el1) (el_lift el2) c2 c'2 u1
+        else raise NotConvertible
+
+    | (FLetIn _, _) | (_, FLetIn _) ->
+        anomaly "LetIn normally removed by fhnf"
+
+    | (FProd (_,c1,c2,_,_), FProd (_,c'1,c'2,_,_)) ->
+	if stack_args_size v1 = 0 && stack_args_size v2 = 0
+	then (* Luo's system *)
+          let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in
+          ccnv cv_pb infos (el_lift el1) (el_lift el2) c2 c'2 u1
+        else raise NotConvertible
+
+    (* Inductive types:  Ind Construct Case Fix Cofix *)
+
+      (* Les annotations du Case ne servent qu'à l'affichage *)
+
+    | (FCases (_,p1,c1,cl1), FCases (_,p2,c2,cl2)) ->
+        let u1 = ccnv CONV infos el1 el2 p1 p2 cuniv in
+        let u2 = ccnv CONV infos el1 el2 c1 c2 u1 in
+        let u3 = convert_vect infos el1 el2 cl1 cl2 u2 in
+	convert_stacks infos lft1 lft2 v1 v2 u3
+
+     | (FInd op1, FInd op2) ->
+         if op1 = op2
+         then convert_stacks infos lft1 lft2 v1 v2 cuniv
+         else raise NotConvertible
+
+     | (FConstruct op1, FConstruct op2) ->
+         if op1 = op2
+         then convert_stacks infos lft1 lft2 v1 v2 cuniv
+         else raise NotConvertible
+
+     | (FFix (op1,(_,tys1,cl1),_,_), FFix(op2,(_,tys2,cl2),_,_)) ->
+	 if op1 = op2
+	 then
+	   let u1 = convert_vect infos el1 el2 tys1 tys2 cuniv in
+           let n = Array.length cl1 in
+           let u2 =
+             convert_vect infos 
+		 (el_liftn n el1) (el_liftn n el2) cl1 cl2 u1 in
+           convert_stacks infos lft1 lft2 v1 v2 u2
+         else raise NotConvertible
+
+     | (FCoFix (op1,(_,tys1,cl1),_,_), FCoFix(op2,(_,tys2,cl2),_,_)) ->
+         if op1 = op2
+         then
+           let u1 = convert_vect infos el1 el2 tys1 tys2 cuniv in
+	   let n = Array.length cl1 in
+           let u2 =
+	     convert_vect infos
+		 (el_liftn n el1) (el_liftn n el2) cl1 cl2 u1 in
+           convert_stacks infos lft1 lft2 v1 v2 u2
+         else raise NotConvertible
+
+     | _ -> raise NotConvertible
+
+and convert_stacks infos lft1 lft2 stk1 stk2 cuniv =
+  match (decomp_stack stk1, decomp_stack stk2) with
+      (Some(a1,s1), Some(a2,s2)) ->
+        let u1 = ccnv CONV infos lft1 lft2 a1 a2 cuniv in
+        convert_stacks infos lft1 lft2 s1 s2 u1
+    | (None, None) -> cuniv
+    | _ -> raise NotConvertible
+
+and convert_vect infos lft1 lft2 v1 v2 cuniv =
+  let lv1 = Array.length v1 in
+  let lv2 = Array.length v2 in
+  if lv1 = lv2
+  then 
+    let rec fold n univ = 
+      if n >= lv1 then univ
+      else
+        let u1 = ccnv CONV infos lft1 lft2 v1.(n) v2.(n) univ in
+        fold (n+1) u1 in
+    fold 0 cuniv
+  else raise NotConvertible
+
+
+
+let fconv cv_pb env sigma t1 t2 =
+  if eq_constr t1 t2 then 
+    Constraint.empty
+  else
+    let infos = create_clos_infos hnf_flags env in
+    ccnv cv_pb infos ELID ELID
+      (inject (nf_evar sigma t1))
+      (inject (nf_evar sigma t2))
+      Constraint.empty
+
+let conv env = fconv CONV env
+let conv_leq env = fconv CUMUL env 
+
+(*
+let convleqkey = Profile.declare_profile "conv_leq";;
+let conv_leq env sigma t1 t2 =
+  Profile.profile4 convleqkey conv_leq env sigma t1 t2;;
+
+let convkey = Profile.declare_profile "conv";;
+let conv env sigma t1 t2 =
+  Profile.profile4 convleqkey conv env sigma t1 t2;;
+*)
+
+let conv_forall2 f env sigma v1 v2 =
+  array_fold_left2 
+    (fun c x y -> let c' = f env sigma x y in Constraint.union c c')
+    Constraint.empty
+    v1 v2
+
+let conv_forall2_i f env sigma v1 v2 =
+  array_fold_left2_i 
+    (fun i c x y -> let c' = f i env sigma x y in Constraint.union c c')
+    Constraint.empty
+    v1 v2
+
+let test_conversion f env sigma x y =
+  try let _ = f env sigma x y in true with NotConvertible -> false
+
+let is_conv env sigma = test_conversion conv env sigma
+let is_conv_leq env sigma = test_conversion conv_leq env sigma
+let is_fconv = function | CONV -> is_conv | CUMUL -> is_conv_leq
+
+(********************************************************************)
+(*             Special-Purpose Reduction                            *)
+(********************************************************************)
+
+let whd_meta metamap c = match kind_of_term c with
+  | Meta p -> (try List.assoc p metamap with Not_found -> c)
+  | _ -> c
+	
+(* Try to replace all metas. Does not replace metas in the metas' values
+ * Differs from (strong whd_meta). *)
+let plain_instance s c = 
+  let rec irec u = match kind_of_term u with
+    | Meta p -> (try List.assoc p s with Not_found -> u)
+    | Cast (m,_) when isMeta m ->
+	(try List.assoc (destMeta m) s with Not_found -> u)
+    | _ -> map_constr irec u
+  in 
+  if s = [] then c else irec c
+    
+(* Pourquoi ne fait-on pas nf_betaiota si s=[] ? *)
+let instance s c = 
+  if s = [] then c else local_strong whd_betaiota (plain_instance s c)
+
+
+(* pseudo-reduction rule:
+ * [hnf_prod_app env s (Prod(_,B)) N --> B[N]
+ * with an HNF on the first argument to produce a product.
+ * if this does not work, then we use the string S as part of our
+ * error message. *)
+
+let hnf_prod_app env sigma t n =
+  match kind_of_term (whd_betadeltaiota env sigma t) with
+    | Prod (_,_,b) -> subst1 n b
+    | _ -> anomaly "hnf_prod_app: Need a product"
+
+let hnf_prod_appvect env sigma t nl = 
+  Array.fold_left (hnf_prod_app env sigma) t nl
+
+let hnf_prod_applist env sigma t nl = 
+  List.fold_left (hnf_prod_app env sigma) t nl
+				    
+let hnf_lam_app env sigma t n =
+  match kind_of_term (whd_betadeltaiota env sigma t) with
+    | Lambda (_,_,b) -> subst1 n b
+    | _ -> anomaly "hnf_lam_app: Need an abstraction"
+
+let hnf_lam_appvect env sigma t nl = 
+  Array.fold_left (hnf_lam_app env sigma) t nl
+
+let hnf_lam_applist env sigma t nl = 
+  List.fold_left (hnf_lam_app env sigma) t nl
+
+let splay_prod env sigma = 
+  let rec decrec env m c =
+    let t = whd_betadeltaiota env sigma c in
+    match kind_of_term t with
+      | Prod (n,a,c0) ->
+	  decrec (push_rel (n,None,a) env)
+	    ((n,a)::m) c0
+      | _ -> m,t
+  in 
+  decrec env []
+
+let splay_prod_assum env sigma = 
+  let rec prodec_rec env l c =
+    let t = whd_betadeltaiota_nolet env sigma c in
+    match kind_of_term c with
+    | Prod (x,t,c)  ->
+	prodec_rec (push_rel (x,None,t) env)
+	  (Sign.add_rel_decl (x, None, t) l) c
+    | LetIn (x,b,t,c) ->
+	prodec_rec (push_rel (x, Some b, t) env)
+	  (Sign.add_rel_decl (x, Some b, t) l) c
+    | Cast (c,_)    -> prodec_rec env l c
+    | _               -> l,t
+  in
+  prodec_rec env Sign.empty_rel_context
+
+let splay_arity env sigma c =
+  let l, c = splay_prod env sigma c in
+  match kind_of_term c with
+    | Sort s -> l,s
+    | _ -> error "not an arity"
+
+let sort_of_arity env c = snd (splay_arity env Evd.empty c)
+  
+let decomp_n_prod env sigma n = 
+  let rec decrec env m ln c = if m = 0 then (ln,c) else 
+    match kind_of_term (whd_betadeltaiota env sigma c) with
+      | Prod (n,a,c0) ->
+	  decrec (push_rel (n,None,a) env)
+	    (m-1) (Sign.add_rel_decl (n,None,a) ln) c0
+      | _                      -> error "decomp_n_prod: Not enough products"
+  in 
+  decrec env n Sign.empty_rel_context
+
+(* One step of approximation *)
+
+let rec apprec env sigma s =
+  let (t, stack as s) = whd_betaiota_state s in
+  match kind_of_term t with
+    | Case (ci,p,d,lf) ->
+        let (cr,crargs) = whd_betadeltaiota_stack env sigma d in
+        let rslt = mkCase (ci, p, applist (cr,crargs), lf) in
+        if reducible_mind_case cr then 
+	  apprec env sigma (rslt, stack)
+        else 
+	  s
+    | Fix fix ->
+	  (match reduce_fix (whd_betadeltaiota_state env sigma) fix stack with
+             | Reduced s -> apprec env sigma s
+	     | NotReducible -> s)
+    | _ -> s
+
+let hnf env sigma c = apprec env sigma (c, empty_stack)
+
+(* A reduction function like whd_betaiota but which keeps casts
+ * and does not reduce redexes containing existential variables.
+ * Used in Correctness.
+ * Added by JCF, 29/1/98. *)
+
+let whd_programs_stack env sigma = 
+  let rec whrec (x, stack as s) =
+    match kind_of_term x with
+      | App (f,cl) ->
+	  let n = Array.length cl - 1 in
+	  let c = cl.(n) in
+	  if occur_existential c then 
+	    s 
+	  else 
+	    whrec (mkApp (f, Array.sub cl 0 n), append_stack [|c|] stack)
+      | LetIn (_,b,_,c) ->
+	  if occur_existential b then
+	    s
+	  else
+	    stacklam whrec [b] c stack
+      | Lambda (_,_,c) ->
+          (match decomp_stack stack with
+             | None -> s
+             | Some (a,m) -> stacklam whrec [a] c m)
+      | Case (ci,p,d,lf) ->
+	  if occur_existential d then
+	    s
+	  else
+            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)
+      | Fix fix ->
+	  (match reduce_fix whrec fix stack with
+             | Reduced s' -> whrec s'
+	     | NotReducible -> s)
+      | _ -> s
+  in 
+  whrec
+
+let whd_programs env sigma x =
+  app_stack (whd_programs_stack env sigma (x, empty_stack))
+
+exception IsType
+
+let find_conclusion env sigma =
+  let rec decrec env c =
+    let t = whd_betadeltaiota env sigma c in
+    match kind_of_term t with
+      | Prod (x,t,c0) -> decrec (push_rel (x,None,t) env) c0
+      | Lambda (x,t,c0) -> decrec (push_rel (x,None,t) env) c0
+      | t -> t
+  in 
+  decrec env
+
+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)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
new file mode 100644
index 0000000000..20c9910326
--- /dev/null
+++ b/pretyping/reductionops.mli
@@ -0,0 +1,205 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Names
+open Term
+open Univ
+open Evd
+open Environ
+open Closure
+(*i*)
+
+(* Reduction Functions. *)
+
+exception Elimconst
+
+type state = constr * constr stack
+
+type 'a contextual_reduction_function = env -> 'a evar_map -> constr -> constr
+type 'a reduction_function = 'a contextual_reduction_function
+type local_reduction_function = constr -> constr
+
+type 'a contextual_stack_reduction_function = 
+    env -> 'a evar_map -> constr -> constr * constr list
+type 'a stack_reduction_function = 'a contextual_stack_reduction_function
+type local_stack_reduction_function = constr -> constr * constr list
+
+type 'a contextual_state_reduction_function = 
+    env -> 'a evar_map -> state -> state
+type 'a state_reduction_function = 'a contextual_state_reduction_function
+type local_state_reduction_function = state -> state
+
+(* Removes cast and put into applicative form *)
+val whd_stack : local_stack_reduction_function
+
+(* For compatibility: alias for whd\_stack *)
+val whd_castapp_stack : local_stack_reduction_function
+
+(*s Reduction Function Operators *)
+
+val strong : 'a reduction_function -> 'a reduction_function
+val local_strong : local_reduction_function -> local_reduction_function
+val strong_prodspine : local_reduction_function -> local_reduction_function
+(*i
+val stack_reduction_of_reduction : 
+  'a reduction_function -> 'a state_reduction_function
+i*)
+val stacklam : (state -> 'a) -> constr list -> constr -> constr stack -> 'a 
+
+(*s Generic Optimized Reduction Function using Closures *)
+
+val clos_norm_flags : Closure.flags -> 'a reduction_function
+(* Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) 
+val nf_beta : local_reduction_function
+val nf_betaiota : local_reduction_function
+val nf_betadeltaiota : 'a reduction_function
+val nf_evar : 'a evar_map -> constr -> constr
+
+(* Lazy strategy, weak head reduction *)
+val whd_evar : 'a evar_map -> constr -> constr
+val whd_beta : local_reduction_function
+val whd_betaiota : local_reduction_function
+val whd_betaiotazeta : local_reduction_function
+val whd_betadeltaiota : 'a contextual_reduction_function
+val whd_betadeltaiota_nolet : 'a contextual_reduction_function
+val whd_betaetalet : local_reduction_function
+
+val whd_beta_stack : local_stack_reduction_function
+val whd_betaiota_stack : local_stack_reduction_function
+val whd_betaiotazeta_stack : local_stack_reduction_function
+val whd_betadeltaiota_stack : 'a contextual_stack_reduction_function
+val whd_betadeltaiota_nolet_stack : 'a contextual_stack_reduction_function
+val whd_betaetalet_stack : local_stack_reduction_function
+
+val whd_beta_state : local_state_reduction_function
+val whd_betaiota_state : local_state_reduction_function
+val whd_betaiotazeta_state : local_state_reduction_function
+val whd_betadeltaiota_state : 'a contextual_state_reduction_function
+val whd_betadeltaiota_nolet_state : 'a contextual_state_reduction_function
+val whd_betaetalet_state : local_state_reduction_function
+
+(*s Head normal forms *)
+
+val whd_delta_stack : 'a stack_reduction_function
+val whd_delta_state : 'a state_reduction_function
+val whd_delta : 'a reduction_function
+val whd_betadelta_stack : 'a stack_reduction_function
+val whd_betadelta_state : 'a state_reduction_function
+val whd_betadelta : 'a reduction_function
+val whd_betaevar_stack : 'a stack_reduction_function
+val whd_betaevar_state : 'a state_reduction_function
+val whd_betaevar : 'a reduction_function
+val whd_betaiotaevar_stack : 'a stack_reduction_function
+val whd_betaiotaevar_state : 'a state_reduction_function
+val whd_betaiotaevar : 'a reduction_function
+val whd_betadeltaeta_stack : 'a stack_reduction_function
+val whd_betadeltaeta_state : 'a state_reduction_function
+val whd_betadeltaeta : 'a reduction_function
+val whd_betadeltaiotaeta_stack : 'a stack_reduction_function
+val whd_betadeltaiotaeta_state : 'a state_reduction_function
+val whd_betadeltaiotaeta : 'a reduction_function
+
+val beta_applist : constr * constr list -> constr
+
+val hnf_prod_app     : env -> 'a evar_map -> constr -> constr -> constr
+val hnf_prod_appvect : env -> 'a evar_map -> constr -> constr array -> constr
+val hnf_prod_applist : env -> 'a evar_map -> constr -> constr list -> constr
+val hnf_lam_app      : env -> 'a evar_map -> constr -> constr -> constr
+val hnf_lam_appvect  : env -> 'a evar_map -> constr -> constr array -> constr
+val hnf_lam_applist  : env -> 'a evar_map -> constr -> constr list -> constr
+
+val splay_prod : env -> 'a evar_map -> constr -> (name * constr) list * constr
+val splay_arity : env -> 'a evar_map -> constr -> (name * constr) list * sorts
+val sort_of_arity : env -> constr -> sorts
+val decomp_n_prod : 
+  env -> 'a evar_map -> int -> constr -> Sign.rel_context * constr
+val splay_prod_assum :
+  env -> 'a evar_map -> constr -> Sign.rel_context * constr
+
+type 'a miota_args = {
+  mP      : constr;     (* the result type *)
+  mconstr : constr;     (* the constructor *)
+  mci     : case_info;  (* special info to re-build pattern *)
+  mcargs  : 'a list;    (* the constructor's arguments *)
+  mlf     : 'a array }  (* the branch code vector *)
+
+val reducible_mind_case : constr -> bool
+val reduce_mind_case : constr miota_args -> constr
+
+val is_arity : env -> 'a evar_map -> constr -> bool
+val is_info_type : env -> 'a evar_map -> unsafe_type_judgment -> bool
+val is_info_arity : env -> 'a 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 : 'a reduction_function
+
+(* [reduce_fix] contracts a fix redex if it is actually reducible *)
+
+type fix_reduction_result = NotReducible | Reduced of state
+
+val fix_recarg : fixpoint -> constr stack -> (int * constr) option
+val reduce_fix : local_state_reduction_function -> fixpoint
+   -> constr stack -> fix_reduction_result
+
+(*s Conversion Functions (uses closures, lazy strategy) *)
+
+type conversion_test = constraints -> constraints
+
+exception NotConvertible
+
+type conv_pb = 
+  | CONV 
+  | CUMUL
+
+val pb_is_equal : conv_pb -> bool
+val pb_equal : conv_pb -> conv_pb
+
+val sort_cmp : conv_pb -> sorts -> sorts -> conversion_test
+val base_sort_cmp : conv_pb -> sorts -> sorts -> bool
+
+type 'a conversion_function = 
+    env -> 'a evar_map -> constr -> constr -> constraints
+
+(* [fconv] has 2 instances: [conv = fconv CONV] i.e. conversion test, and
+   [conv_leq = fconv CONV_LEQ] i.e. cumulativity test. *)
+
+val conv : 'a conversion_function
+val conv_leq : 'a conversion_function
+
+val conv_forall2 : 
+  'a conversion_function -> env -> 'a evar_map -> constr array 
+    -> constr array -> constraints
+
+val conv_forall2_i : 
+  (int -> 'a conversion_function) -> env -> 'a evar_map
+    -> constr array -> constr array -> constraints
+
+val is_conv : env -> 'a evar_map -> constr -> constr -> bool
+val is_conv_leq : env -> 'a evar_map -> constr -> constr -> bool
+val is_fconv : conv_pb -> env -> 'a evar_map -> constr -> constr -> bool
+
+(*s Special-Purpose Reduction Functions *)
+
+val whd_meta : (int * constr) list -> constr -> constr
+val plain_instance : (int * constr) list -> constr -> constr
+val instance : (int * constr) list -> constr -> constr
+
+(*s Obsolete Reduction Functions *)
+
+(*i
+val hnf : env -> 'a evar_map -> constr -> constr * constr list
+i*)
+val apprec : 'a state_reduction_function
+
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 5ed6e60517..bb6948767b 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -12,23 +12,25 @@ open Util
 open Term
 open Inductive
 open Names
-open Reduction
+open Reductionops
 open Environ
 open Typeops
+open Declarations
+open Instantiate
 
 type metamap = (int * constr) list
 
 let outsort env sigma t =
   match kind_of_term (whd_betadeltaiota env sigma t) with
-    | IsSort s -> s
+    | Sort s -> s
     | _ -> anomaly "Retyping: found a type of type which is not a sort"
 
 let rec subst_type env sigma typ = function
   | [] -> typ
   | h::rest ->
       match kind_of_term (whd_betadeltaiota env sigma typ) with
-        | IsProd (na,c1,c2) -> 
-	    subst_type (push_rel_assum (na,c1) env) sigma (subst1 h c2) rest
+        | Prod (na,c1,c2) -> 
+	    subst_type (push_rel (na,None,c1) env) sigma (subst1 h c2) rest
         | _ -> anomaly "Non-functional construction"
 
 (* Si ft est le type d'un terme f, lequel est appliqué à args, *)
@@ -39,71 +41,74 @@ let rec subst_type env sigma typ = function
 let sort_of_atomic_type env sigma ft args =
   let rec concl_of_arity env ar =
     match kind_of_term (whd_betadeltaiota env sigma ar) with
-      | IsProd (na, t, b) -> concl_of_arity (push_rel_assum (na,t) env) b
-      | IsSort s -> s
+      | Prod (na, t, b) -> concl_of_arity (push_rel (na,None,t) env) b
+      | Sort s -> s
       | _ -> outsort env sigma (subst_type env sigma ft (Array.to_list args))
   in concl_of_arity env ft
 
 let typeur sigma metamap =
   let rec type_of env cstr=
     match kind_of_term cstr with
-    | IsMeta n ->
+    | Meta n ->
           (try strip_outer_cast (List.assoc n metamap)
            with Not_found -> anomaly "type_of: this is not a well-typed term")
-    | IsRel n -> lift n (body_of_type (snd (lookup_rel_type n env)))
-    | IsVar id ->
-      (try body_of_type (snd (lookup_named id env))
-       with Not_found ->
-         anomaly ("type_of: variable "^(string_of_id id)^" unbound"))
-    | IsConst c -> body_of_type (type_of_constant env sigma c)
-    | IsEvar ev -> type_of_existential env sigma ev
-    | IsMutInd ind -> body_of_type (type_of_inductive env sigma ind)
-    | IsMutConstruct cstr -> body_of_type (type_of_constructor env sigma cstr)
-    | IsMutCase (_,p,c,lf) ->
-        let IndType (indf,realargs) =
-          try find_rectype env sigma (type_of env c)
+    | Rel n ->
+        let (_,_,ty) = lookup_rel n env in
+        lift n (body_of_type ty)
+    | Var id ->
+        let (_,_,ty) = lookup_named id env in
+        (try body_of_type ty
+        with Not_found ->
+          anomaly ("type_of: variable "^(string_of_id id)^" unbound"))
+    | Const c ->
+        let cb = lookup_constant c env in
+        body_of_type cb.const_type
+    | Evar ev -> existential_type sigma ev
+    | Ind ind -> body_of_type (type_of_inductive env ind)
+    | Construct cstr -> body_of_type (type_of_constructor env cstr)
+    | Case (_,p,c,lf) ->
+        (* TODO: could avoid computing the type of branches *)
+        let i =
+          try find_rectype env (type_of env c)
           with Induc -> anomaly "type_of: Bad recursive type" in
-	let (aritysign,_) = get_arity indf in
-	let (psign,_) = splay_prod env sigma (type_of env p) in
-        let al =
-	  if List.length psign > List.length aritysign
-	  then realargs@[c] else realargs in
-        whd_betadeltaiota env sigma (applist (p,al))
-    | IsLambda (name,c1,c2) ->
-          mkProd (name, c1, type_of (push_rel_assum (name,c1) env) c2)
-    | IsLetIn (name,b,c1,c2) ->
-         subst1 b (type_of (push_rel_def (name,b,c1) env) c2)
-    | IsFix ((_,i),(_,tys,_)) -> tys.(i)
-    | IsCoFix (i,(_,tys,_)) -> tys.(i)
-    | IsApp(f,args)->
+        let pj = { uj_val = p; uj_type = type_of env p } in
+        let (_,ty,_) = type_case_branches env i pj c in
+        ty
+    | Lambda (name,c1,c2) ->
+          mkProd (name, c1, type_of (push_rel (name,None,c1) env) c2)
+    | LetIn (name,b,c1,c2) ->
+         subst1 b (type_of (push_rel (name,Some b,c1) env) c2)
+    | Fix ((_,i),(_,tys,_)) -> tys.(i)
+    | CoFix (i,(_,tys,_)) -> tys.(i)
+    | App(f,args)->
         strip_outer_cast
           (subst_type env sigma (type_of env f) (Array.to_list args))
-    | IsCast (c,t) -> t
-    | IsSort _ | IsProd (_,_,_) | IsMutInd _ -> mkSort (sort_of env cstr)
+    | Cast (c,t) -> t
+    | Sort _ | Prod (_,_,_) | Ind _ -> mkSort (sort_of env cstr)
 
   and sort_of env t = 
     match kind_of_term t with
-    | IsCast (c,s) when isSort s -> destSort s
-    | IsSort (Prop c) -> type_0
-    | IsSort (Type u) -> Type (fst (Univ.super u))
-    | IsProd (name,t,c2) ->
-        (match (sort_of (push_rel_assum (name,t) env) c2) with
+    | Cast (c,s) when isSort s -> destSort s
+    | Sort (Prop c) -> type_0
+    | Sort (Type u) -> Type (fst (Univ.super u))
+    | Prod (name,t,c2) ->
+        (match (sort_of (push_rel (name,None,t) env) c2) with
 	  | Prop _ as s -> s
 	  | Type u2 as s -> s (*Type Univ.dummy_univ*))
-    | IsApp(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
-    | IsLambda _ | IsFix _ | IsMutConstruct _ ->
+    | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
+    | Lambda _ | Fix _ | Construct _ ->
         anomaly "sort_of: Not a type (1)"
     | _ -> outsort env sigma (type_of env t)
 
   and sort_family_of env t =
     match kind_of_term (whd_betadeltaiota env sigma t) with
-    | IsCast (c,s) when isSort s -> family_of_sort (destSort s)
-    | IsSort (Prop c) -> InType
-    | IsSort (Type u) -> InType
-    | IsProd (name,t,c2) -> sort_family_of (push_rel_assum (name,t) env) c2
-    | IsApp(f,args) -> 
+    | Cast (c,s) when isSort s -> family_of_sort (destSort s)
+    | Sort (Prop c) -> InType
+    | Sort (Type u) -> InType
+    | Prod (name,t,c2) -> sort_family_of (push_rel (name,None,t) env) c2
+    | App(f,args) -> 
        family_of_sort (sort_of_atomic_type env sigma (type_of env f) args)
-    | IsLambda _ | IsFix _ | IsMutConstruct _ ->
+    | Lambda _ | Fix _ | Construct _ ->
         anomaly "sort_of: Not a type (1)"
     | _ -> family_of_sort (outsort env sigma (type_of env t))
 
diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml
index 1b875affa7..381a40ee66 100644
--- a/pretyping/syntax_def.ml
+++ b/pretyping/syntax_def.ml
@@ -14,6 +14,7 @@ open Names
 open Rawterm
 open Libobject
 open Lib
+open Nameops
 
 (* Syntactic definitions. *)
 
@@ -57,7 +58,7 @@ let (in_syntax_constant, out_syntax_constant) =
   declare_object ("SYNTAXCONSTANT", od)
 
 let declare_syntactic_definition id c =
-  let _ = add_leaf id CCI (in_syntax_constant c) in ()
+  let _ = add_leaf id (in_syntax_constant c) in ()
 
 let search_syntactic_definition sp = Spmap.find sp !syntax_table
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 7d1564a8c0..854a61b268 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -11,10 +11,12 @@
 open Pp
 open Util
 open Names
+open Nameops
 open Term
+open Termops
 open Inductive
 open Environ
-open Reduction
+open Reductionops
 open Closure
 open Instantiate
 open Cbv
@@ -22,16 +24,46 @@ open Cbv
 exception Elimconst
 exception Redelimination
 
-let check_transparency env ref =
-  match ref with
-      EvalConst sp -> Opaque.is_evaluable env (EvalConstRef sp)
-    | EvalVar id -> Opaque.is_evaluable env (EvalVarRef id)
-    | _ -> false
-
-let isEvalRef env x =
-  Instantiate.isEvalRef x &
-  let ref = Instantiate.destEvalRef x in
-  check_transparency env ref
+type evaluable_reference =
+  | EvalConst of constant
+  | EvalVar of identifier
+  | EvalRel of int
+  | EvalEvar of existential
+
+let mkEvalRef = function
+  | EvalConst cst -> mkConst cst
+  | EvalVar id -> mkVar id
+  | EvalRel n -> mkRel n
+  | EvalEvar ev -> mkEvar ev
+
+let isEvalRef env c = match kind_of_term c with
+  | Const sp -> Opaque.is_evaluable env (EvalConstRef sp)
+  | Var id -> Opaque.is_evaluable env (EvalVarRef id)
+  | Rel _ | Evar _ -> true
+  | _ -> false
+
+let destEvalRef c = match kind_of_term c with
+  | Const cst ->  EvalConst cst
+  | Var id  -> EvalVar id
+  | Rel n -> EvalRel n
+  | Evar ev -> EvalEvar ev
+  | _ -> anomaly "Not an evaluable reference"
+
+let reference_opt_value sigma env = function
+  | EvalConst cst -> constant_opt_value env cst
+  | EvalVar id ->
+      let (_,v,_) = lookup_named id env in
+      v
+  | EvalRel n ->
+      let (_,v,_) = lookup_rel n env in
+      option_app (lift n) v
+  | EvalEvar ev -> existential_opt_value sigma ev
+
+exception NotEvaluable
+let reference_value sigma env c =
+  match reference_opt_value sigma env c with
+    | None -> raise NotEvaluable
+    | Some d -> d
 
 (************************************************************************)
 (* Reduction of constant hiding fixpoints (e.g. for Simpl). The trick   *)
@@ -95,7 +127,7 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
   let li =
     List.map
       (function d -> match kind_of_term d with
-         | IsRel k ->
+         | Rel k ->
              if
 	       array_for_all (noccurn k) tys
 	       && array_for_all (noccurn (k+nbfix)) bds
@@ -129,7 +161,7 @@ let invert_name labs l na0 env sigma ref = function
 	  | EvalRel _ | EvalEvar _ -> None
 	  | EvalVar id' -> Some (EvalVar id)
 	  | EvalConst sp ->
-	      Some (EvalConst (make_path (dirpath sp) id CCI)) in
+	      Some (EvalConst (make_path (dirpath sp) id)) in
 	match refi with
 	  | None -> None
 	  | Some ref ->
@@ -151,12 +183,12 @@ let compute_consteval_direct sigma env ref =
   let rec srec env n labs c =
     let c',l = whd_betadeltaeta_stack env sigma c in
     match kind_of_term c' with
-      | IsLambda (id,t,g) when l=[] ->
-	  srec (push_rel_assum (id,t) env) (n+1) (t::labs) g
-      | IsFix fix ->
+      | Lambda (id,t,g) when l=[] ->
+	  srec (push_rel (id,None,t) env) (n+1) (t::labs) g
+      | Fix fix ->
 	  (try check_fix_reversibility labs l fix 
 	  with Elimconst -> NotAnElimination)
-      | IsMutCase (_,_,d,_) when isRel d -> EliminationCases n
+      | Case (_,_,d,_) when isRel d -> EliminationCases n
       | _ -> NotAnElimination
   in 
   match reference_opt_value sigma env ref with
@@ -168,9 +200,9 @@ let compute_consteval_mutual_fix sigma env ref =
     let c',l = whd_betaetalet_stack c in
     let nargs = List.length l in
     match kind_of_term c' with
-      | IsLambda (na,t,g) when l=[] ->
-	  srec (push_rel_assum (na,t) env) (minarg+1) (t::labs) ref g
-      | IsFix ((lv,i),(names,_,_) as fix) ->
+      | Lambda (na,t,g) when l=[] ->
+	  srec (push_rel (na,None,t) env) (minarg+1) (t::labs) ref g
+      | Fix ((lv,i),(names,_,_) as fix) ->
 	  (* Last known constant wrapping Fix is ref = [labs](Fix l) *)
 	  (match compute_consteval_direct sigma env ref with
 	     | NotAnElimination -> (*Above const was eliminable but this not!*)
@@ -285,7 +317,7 @@ let reduce_fix_use_function f whfun fix stack =
 	    whfun (recarg, empty_stack) in
         let stack' = stack_assign stack recargnum (app_stack recarg') in
 	(match kind_of_term recarg'hd with
-           | IsMutConstruct _ ->
+           | Construct _ ->
 	       Reduced (contract_fix_use_function f fix,stack')
 	   | _ -> NotReducible)
 
@@ -300,27 +332,27 @@ let contract_cofix_use_function f (bodynum,(_,names,bodies as typedbodies)) =
 
 let reduce_mind_case_use_function sp env mia =
   match kind_of_term mia.mconstr with 
-    | IsMutConstruct(ind_sp,i as cstr_sp) ->
-	let real_cargs = snd (list_chop (fst mia.mci) mia.mcargs) in
+    | Construct(ind_sp,i as cstr_sp) ->
+	let real_cargs = snd (list_chop mia.mci.ci_npar mia.mcargs) in
 	applist (mia.mlf.(i-1), real_cargs)
-    | IsCoFix (_,(names,_,_) as cofix) ->
+    | CoFix (_,(names,_,_) as cofix) ->
 	let build_fix_name i =
 	  match names.(i) with 
 	    | Name id ->
-		let sp = make_path (dirpath sp) id (kind_of_path sp) in
+		let sp = make_path (dirpath sp) id in
 		(match constant_opt_value env sp with
 		  | None -> None
 		  | Some _ -> Some (mkConst sp))
 	    | Anonymous -> None in 
 	let cofix_def = contract_cofix_use_function build_fix_name cofix in
-	mkMutCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
+	mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
     | _ -> assert false
 
 let special_red_case env whfun (ci, p, c, lf)  =
   let rec redrec s = 
     let (constr, cargs) = whfun s in 
     match kind_of_term constr with 
-      | IsConst cst -> 
+      | Const cst -> 
           (if not (Opaque.is_evaluable env (EvalConstRef cst)) then
             raise Redelimination;
 	  let gvalue = constant_value env cst in
@@ -377,21 +409,21 @@ let rec red_elim_const env sigma ref largs =
 and construct_const env sigma = 
   let rec hnfstack (x, stack as s) =
     match kind_of_term x with
-      | IsCast (c,_) -> hnfstack (c, stack)
-      | IsApp (f,cl) -> hnfstack (f, append_stack cl stack)
-      | IsLambda (id,t,c) ->
+      | Cast (c,_) -> hnfstack (c, stack)
+      | App (f,cl) -> hnfstack (f, append_stack cl stack)
+      | Lambda (id,t,c) ->
           (match decomp_stack stack with 
              | None -> assert false
              | Some (c',rest) -> 
 		   stacklam hnfstack [c'] c rest)
-      | IsLetIn (n,b,t,c) -> stacklam hnfstack [b] c stack
-      | IsMutCase (ci,p,c,lf) ->
+      | LetIn (n,b,t,c) -> stacklam hnfstack [b] c stack
+      | Case (ci,p,c,lf) ->
           hnfstack 
 	    (special_red_case env
               (construct_const env sigma) (ci,p,c,lf), stack)
-      | IsMutConstruct _ -> s
-      | IsCoFix _ -> s
-      | IsFix fix -> 
+      | Construct _ -> s
+      | CoFix _ -> s
+      | Fix fix -> 
 	  (match reduce_fix hnfstack fix stack with
              | Reduced s' -> hnfstack s'
 	     | NotReducible -> raise Redelimination)
@@ -403,7 +435,7 @@ and construct_const env sigma =
 	     (match reference_opt_value sigma env ref with
 		| Some cval ->
 		    (match kind_of_term cval with
-                       | IsCoFix _ -> s
+                       | CoFix _ -> s
                        | _ -> hnfstack (cval, stack))
 		| None ->
 		    raise Redelimination))
@@ -420,9 +452,9 @@ let internal_red_product env sigma c =
   let simpfun = clos_norm_flags (UNIFORM,betaiotazeta_red) env sigma in
   let rec redrec env x =
     match kind_of_term x with
-      | IsApp (f,l) -> 
+      | App (f,l) -> 
           (match kind_of_term f with
-             | IsFix fix ->
+             | Fix fix ->
                  let stack = append_stack l empty_stack in
                  (match fix_recarg fix stack with
                     | None -> raise Redelimination
@@ -431,10 +463,10 @@ let internal_red_product env sigma c =
                         let stack' = stack_assign stack recargnum recarg' in
                         simpfun (app_stack (f,stack')))
              | _ -> simpfun (appvect (redrec env f, l)))
-      | IsCast (c,_) -> redrec env c
-      | IsProd (x,a,b) -> mkProd (x, a, redrec (push_rel_assum (x,a) env) b)
-      | IsLetIn (x,a,b,t) -> redrec env (subst1 a t)
-      | IsMutCase (ci,p,d,lf) -> simpfun (mkMutCase (ci,p,redrec env d,lf))
+      | Cast (c,_) -> redrec env c
+      | Prod (x,a,b) -> mkProd (x, a, redrec (push_rel (x,None,a) env) b)
+      | LetIn (x,a,b,t) -> redrec env (subst1 a t)
+      | Case (ci,p,d,lf) -> simpfun (mkCase (ci,p,redrec env d,lf))
       | _ when isEvalRef env x -> 
           (* TO DO: re-fold fixpoints after expansion *)
           (* to get true one-step reductions *)
@@ -454,22 +486,22 @@ let red_product env sigma c =
 let hnf_constr env sigma c = 
   let rec redrec (x, largs as s) =
     match kind_of_term x with
-      | IsLambda (n,t,c) ->
+      | Lambda (n,t,c) ->
           (match decomp_stack largs with
              | None      -> app_stack s
              | Some (a,rest) -> 
 		 stacklam redrec [a] c rest)
-      | IsLetIn (n,b,t,c) -> stacklam redrec [b] c largs
-      | IsApp (f,cl)   -> redrec (f, append_stack cl largs)
-      | IsCast (c,_) -> redrec (c, largs)
-      | IsMutCase (ci,p,c,lf) ->
+      | LetIn (n,b,t,c) -> stacklam redrec [b] c largs
+      | App (f,cl)   -> redrec (f, append_stack cl largs)
+      | Cast (c,_) -> redrec (c, largs)
+      | Case (ci,p,c,lf) ->
           (try
              redrec 
 	       (special_red_case env (whd_betadeltaiota_state env sigma) 
 		  (ci, p, c, lf), largs)
            with Redelimination -> 
 	     app_stack s)
-      | IsFix fix ->
+      | Fix fix ->
 	  (match reduce_fix (whd_betadeltaiota_state env sigma) fix largs with
              | Reduced s' -> redrec s'
 	     | NotReducible -> app_stack s)
@@ -482,7 +514,7 @@ let hnf_constr env sigma c =
              match reference_opt_value sigma env ref with
 	       | Some c ->
 		   (match kind_of_term c with 
-                      | IsCoFix _ -> app_stack (x,largs)
+                      | CoFix _ -> app_stack (x,largs)
 		      | _ ->  redrec (c, largs))
 	       | None -> app_stack s)
       | _ -> app_stack s
@@ -495,20 +527,20 @@ let hnf_constr env sigma c =
 let whd_nf env sigma c = 
   let rec nf_app (c, stack as s) =
     match kind_of_term c with
-      | IsLambda (name,c1,c2)    ->
+      | Lambda (name,c1,c2)    ->
           (match decomp_stack stack with
              | None -> (c,empty_stack)
              | Some (a1,rest) -> 
 		 stacklam nf_app [a1] c2 rest)
-      | IsLetIn (n,b,t,c) -> stacklam nf_app [b] c stack
-      | IsApp (f,cl) -> nf_app (f, append_stack cl stack)
-      | IsCast (c,_) -> nf_app (c, stack)
-      | IsMutCase (ci,p,d,lf) ->
+      | LetIn (n,b,t,c) -> stacklam nf_app [b] c stack
+      | App (f,cl) -> nf_app (f, append_stack cl stack)
+      | Cast (c,_) -> nf_app (c, stack)
+      | Case (ci,p,d,lf) ->
           (try
              nf_app (special_red_case env nf_app (ci,p,d,lf), stack)
            with Redelimination -> 
 	     s)
-      | IsFix fix ->
+      | Fix fix ->
 	  (match reduce_fix nf_app fix stack with
              | Reduced s' -> nf_app s'
 	     | NotReducible -> s)
@@ -528,7 +560,7 @@ let nf env sigma c = strong whd_nf env sigma c
  * ol is the occurence list to find. *)
 let rec substlin env name n ol c =
   match kind_of_term c with
-    | IsConst const when EvalConstRef const = name ->
+    | Const const when EvalConstRef const = name ->
         if List.hd ol = n then
           try 
 	    (n+1, List.tl ol, constant_value env const)
@@ -539,18 +571,18 @@ let rec substlin env name n ol c =
         else 
 	  ((n+1), ol, c)
 
-    | IsVar id when EvalVarRef id = name ->
+    | Var id when EvalVarRef id = name ->
         if List.hd ol = n then
-          match lookup_named_value id env with
-	    | Some c -> (n+1, List.tl ol, c)
-	    | None -> 
+          match lookup_named id env with
+	    | (_,Some c,_) -> (n+1, List.tl ol, c)
+	    | _ -> 
 		errorlabstrm "substlin"
 		  [< pr_id id; 'sTR " is not a defined constant" >]
         else 
 	  ((n+1), ol, c)
 
     (* INEFFICIENT: OPTIMIZE *)
-    | IsApp (c1,cl) ->
+    | App (c1,cl) ->
         Array.fold_left 
 	  (fun (n1,ol1,c1') c2 ->
 	     (match ol1 with 
@@ -560,7 +592,7 @@ let rec substlin env name n ol c =
                     (n2,ol2,applist(c1',[c2']))))
           (substlin env name n ol c1) cl
 
-    | IsLambda (na,c1,c2) ->
+    | Lambda (na,c1,c2) ->
         let (n1,ol1,c1') = substlin env name n ol c1 in
         (match ol1 with 
            | [] -> (n1,[],mkLambda (na,c1',c2))
@@ -568,7 +600,7 @@ let rec substlin env name n ol c =
                let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
                (n2,ol2,mkLambda (na,c1',c2')))
 
-    | IsLetIn (na,c1,t,c2) ->
+    | LetIn (na,c1,t,c2) ->
         let (n1,ol1,c1') = substlin env name n ol c1 in
         (match ol1 with 
            | [] -> (n1,[],mkLetIn (na,c1',t,c2))
@@ -576,7 +608,7 @@ let rec substlin env name n ol c =
                let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
                (n2,ol2,mkLetIn (na,c1',t,c2')))
 
-    | IsProd (na,c1,c2) ->
+    | Prod (na,c1,c2) ->
         let (n1,ol1,c1') = substlin env name n ol c1 in
         (match ol1 with 
            | [] -> (n1,[],mkProd (na,c1',c2))
@@ -584,7 +616,7 @@ let rec substlin env name n ol c =
                let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
                (n2,ol2,mkProd (na,c1',c2')))
 	
-    | IsMutCase (ci,p,d,llf) -> 
+    | Case (ci,p,d,llf) -> 
         let rec substlist nn oll = function
           | []     -> (nn,oll,[])
           | f::lfe ->
@@ -597,16 +629,16 @@ let rec substlin env name n ol c =
 	in
 	let (n1,ol1,p') = substlin env name n ol p in  (* ATTENTION ERREUR *)
         (match ol1 with                                 (* si P pas affiche *)
-           | [] -> (n1,[],mkMutCase (ci, p', d, llf))
+           | [] -> (n1,[],mkCase (ci, p', d, llf))
            | _  ->
                let (n2,ol2,d') = substlin env name n1 ol1 d in
                (match ol2 with
-		  | [] -> (n2,[],mkMutCase (ci, p', d', llf))
+		  | [] -> (n2,[],mkCase (ci, p', d', llf))
 		  | _  -> 
 	              let (n3,ol3,lf') = substlist n2 ol2 (Array.to_list llf)
-                      in (n3,ol3,mkMutCaseL (ci, p', d', lf'))))
+                      in (n3,ol3,mkCase (ci, p', d', Array.of_list lf'))))
         
-    | IsCast (c1,c2)   ->
+    | Cast (c1,c2)   ->
         let (n1,ol1,c1') = substlin env name n ol c1 in
         (match ol1 with 
            | [] -> (n1,[],mkCast (c1',c2))
@@ -614,14 +646,14 @@ let rec substlin env name n ol c =
                let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
                (n2,ol2,mkCast (c1',c2')))
 
-    | IsFix _ -> 
+    | Fix _ -> 
         (warning "do not consider occurrences inside fixpoints"; (n,ol,c))
 	
-    | IsCoFix _ -> 
+    | CoFix _ -> 
         (warning "do not consider occurrences inside cofixpoints"; (n,ol,c))
 
-    | (IsRel _|IsMeta _|IsVar _|IsSort _
-      |IsEvar _|IsConst _|IsMutInd _|IsMutConstruct _) -> (n,ol,c)
+    | (Rel _|Meta _|Var _|Sort _
+      |Evar _|Const _|Ind _|Construct _) -> (n,ol,c)
 
 let string_of_evaluable_ref = function
   | EvalVarRef id -> string_of_id id
@@ -664,7 +696,7 @@ let fold_commands cl env sigma c =
 
 (* call by value reduction functions *)
 let cbv_norm_flags flags env sigma t =
-  cbv_norm (create_cbv_infos flags env sigma) t
+  cbv_norm (create_cbv_infos flags env) (nf_evar sigma t)
 
 let cbv_beta = cbv_norm_flags beta empty_env Evd.empty
 let cbv_betaiota = cbv_norm_flags betaiota empty_env Evd.empty
@@ -719,22 +751,22 @@ exception NotStepReducible
 let one_step_reduce env sigma c = 
   let rec redrec (x, largs as s) =
     match kind_of_term x with
-      | IsLambda (n,t,c)  ->
+      | Lambda (n,t,c)  ->
           (match decomp_stack largs with
              | None      -> raise NotStepReducible
              | Some (a,rest) -> (subst1 a c, rest))
-      | IsApp (f,cl) -> redrec (f, append_stack cl largs)
-      | IsLetIn (_,f,_,cl) -> (subst1 f cl,largs)
-      | IsMutCase (ci,p,c,lf) ->
+      | App (f,cl) -> redrec (f, append_stack cl largs)
+      | LetIn (_,f,_,cl) -> (subst1 f cl,largs)
+      | Case (ci,p,c,lf) ->
           (try
 	     (special_red_case env (whd_betadeltaiota_state env sigma)
 	       (ci,p,c,lf), largs)
            with Redelimination -> raise NotStepReducible)
-      | IsFix fix ->
+      | Fix fix ->
 	  (match reduce_fix (whd_betadeltaiota_state env sigma) fix largs with
              | Reduced s' -> s'
 	     | NotReducible -> raise NotStepReducible)
-      | IsCast (c,_) -> redrec (c,largs)
+      | Cast (c,_) -> redrec (c,largs)
       | _ when isEvalRef env x ->
 	  let ref =
             try destEvalRef x
@@ -757,10 +789,10 @@ let reduce_to_ind_gen allow_product env sigma t =
   let rec elimrec env t l = 
     let c, _ = whd_stack t in
     match kind_of_term c with
-      | IsMutInd (mind,args) -> ((mind,args),it_mkProd_or_LetIn t l)
-      | IsProd (n,ty,t') ->
+      | Ind (mind,args) -> ((mind,args),it_mkProd_or_LetIn t l)
+      | Prod (n,ty,t') ->
 	  if allow_product then
-	    elimrec (push_rel_assum (n,t) env) t' ((n,None,ty)::l)
+	    elimrec (push_rel (n,None,t) env) t' ((n,None,ty)::l)
 	  else
 	     errorlabstrm "tactics__reduce_to_mind"
 	       [< 'sTR"Not an inductive definition" >]
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index fc9e55e303..fbeadc9860 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -13,7 +13,7 @@ open Names
 open Term
 open Environ
 open Evd
-open Reduction
+open Reductionops
 open Closure
 (*i*)
 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
new file mode 100644
index 0000000000..f8dd8ce154
--- /dev/null
+++ b/pretyping/termops.ml
@@ -0,0 +1,709 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Term
+open Environ
+open Nametab
+open Sign
+
+let print_sort = function
+  | Prop Pos -> [< 'sTR "Set" >]
+  | Prop Null -> [< 'sTR "Prop" >]
+(*  | Type _ -> [< 'sTR "Type" >] *)
+  | Type u -> [< 'sTR "Type("; Univ.pr_uni u; 'sTR ")" >]
+
+(* prod_it b [xn:Tn;..;x1:T1] = (x1:T1)..(xn:Tn)b *)
+let prod_it = List.fold_left (fun c (n,t)  -> mkProd (n, t, c))
+
+(* lam_it b [xn:Tn;..;x1:T1] = [x1:T1]..[xn:Tn]b *)
+let lam_it = List.fold_left (fun c (n,t)  -> mkLambda (n, t, c))
+
+(* [Rel (n+m);...;Rel(n+1)] *)
+let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
+
+let rel_list n m = 
+  let rec reln l p = 
+    if p>m then l else reln (mkRel(n+p)::l) (p+1)
+  in 
+  reln [] 1
+
+(* Same as [rel_list] but takes a context as argument and skips let-ins *)
+let extended_rel_list n hyps =
+  let rec reln l p = function
+    | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps
+    | (_,Some _,_) :: hyps -> reln l (p+1) hyps
+    | [] -> l
+  in 
+  reln [] 1 hyps
+
+let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps)
+
+
+
+let push_rel_assum (x,t) env = push_rel (x,None,t) env
+
+let push_rels_assum assums =
+  push_rel_context (List.map (fun (x,t) -> (x,None,t)) assums)
+
+let push_named_rec_types (lna,typarray,_) env =
+  let ctxt =
+    array_map2_i
+      (fun i na t ->
+	 match na with
+	   | Name id -> (id, None, type_app (lift i) t)
+	   | Anonymous -> anomaly "Fix declarations must be named")
+      lna typarray in
+  Array.fold_left
+    (fun e assum -> push_named_decl assum e) env ctxt
+
+let rec lookup_rel_id id sign = 
+  let rec lookrec = function
+    | (n, (Anonymous,_,_)::l) -> lookrec (n+1,l)
+    | (n, (Name id',_,t)::l)  -> if id' = id then (n,t) else lookrec (n+1,l)
+    | (_, [])                 -> raise Not_found
+  in 
+  lookrec (1,sign)
+
+(* Constructs either [(x:t)c] or [[x=b:t]c] *)
+let mkProd_or_LetIn (na,body,t) c =
+  match body with
+    | None -> mkProd (na, t, c)
+    | Some b -> mkLetIn (na, b, t, c)
+
+(* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *)
+let mkProd_wo_LetIn (na,body,t) c =
+  match body with
+    | None -> mkProd (na, body_of_type t, c)
+    | Some b -> subst1 b c
+
+let it_mkProd_wo_LetIn   = List.fold_left (fun c d -> mkProd_wo_LetIn d c)
+let it_mkProd_or_LetIn   = List.fold_left (fun c d -> mkProd_or_LetIn d c)
+
+let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c)
+
+let it_named_context_quantifier f = List.fold_left (fun c d -> f d c)
+
+let it_mkNamedProd_or_LetIn = it_named_context_quantifier mkNamedProd_or_LetIn
+let it_mkNamedLambda_or_LetIn = it_named_context_quantifier mkNamedLambda_or_LetIn
+
+(* *)
+
+(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
+   subterms of [c]; it carries an extra data [l] (typically a name
+   list) which is processed by [g na] (which typically cons [na] to
+   [l]) at each binder traversal (with name [na]); it is not recursive
+   and the order with which subterms are processed is not specified *)
+
+let map_constr_with_named_binders g f l c = match kind_of_term c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> c
+  | Cast (c,t) -> mkCast (f l c, f l t)
+  | Prod (na,t,c) -> mkProd (na, f l t, f (g na l) c)
+  | Lambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c)
+  | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c)
+  | App (c,al) -> mkApp (f l c, Array.map (f l) al)
+  | Evar (e,al) -> mkEvar (e, Array.map (f l) al)
+  | Case (ci,p,c,bl) -> mkCase (ci, f l p, f l c, Array.map (f l) bl)
+  | Fix (ln,(lna,tl,bl)) ->
+      let l' = Array.fold_left (fun l na -> g na l) l lna in
+      mkFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
+  | CoFix(ln,(lna,tl,bl)) ->
+      let l' = Array.fold_left (fun l na -> g na l) l lna in
+      mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
+
+(* [map_constr_with_binders_left_to_right g f n c] maps [f n] on the
+   immediate subterms of [c]; it carries an extra data [n] (typically
+   a lift index) which is processed by [g] (which typically add 1 to
+   [n]) at each binder traversal; the subterms are processed from left
+   to right according to the usual representation of the constructions
+   (this may matter if [f] does a side-effect); it is not recursive;
+   in fact, the usual representation of the constructions is at the
+   time being almost those of the ML representation (except for
+   (co-)fixpoint) *)
+
+let array_map_left f a = (* Ocaml does not guarantee Array.map is LR *)
+  let l = Array.length a in (* (even if so), then we rewrite it *)
+  if l = 0 then [||] else begin
+    let r = Array.create l (f a.(0)) in
+    for i = 1 to l - 1 do
+      r.(i) <- f a.(i)
+    done;
+    r
+  end
+
+let array_map_left_pair f a g b =
+  let l = Array.length a in
+  if l = 0 then [||],[||] else begin
+    let r = Array.create l (f a.(0)) in
+    let s = Array.create l (g b.(0)) in
+    for i = 1 to l - 1 do
+      r.(i) <- f a.(i);
+      s.(i) <- g b.(i)
+    done;
+    r, s
+  end
+
+let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> c
+  | Cast (c,t) -> let c' = f l c in mkCast (c', f l t)
+  | Prod (na,t,c) -> let t' = f l t in mkProd (na, t', f (g l) c)
+  | Lambda (na,t,c) -> let t' = f l t in mkLambda (na, t', f (g l) c)
+  | LetIn (na,b,t,c) ->
+      let b' = f l b in let t' = f l t in mkLetIn (na, b', t', f (g l) c)
+  | App (c,al) -> 
+      let c' = f l c in mkApp (c', array_map_left (f l) al)
+  | Evar (e,al) -> mkEvar (e, array_map_left (f l) al)
+  | Case (ci,p,c,bl) ->
+      let p' = f l p in let c' = f l c in
+      mkCase (ci, p', c', array_map_left (f l) bl)
+  | Fix (ln,(lna,tl,bl)) ->
+      let l' = iterate g (Array.length tl) l in
+      let (tl',bl') = array_map_left_pair (f l) tl (f l') bl in
+      mkFix (ln,(lna,tl',bl'))
+  | CoFix(ln,(lna,tl,bl)) ->
+      let l' = iterate g (Array.length tl) l in
+      let (tl',bl') = array_map_left_pair (f l) tl (f l') bl in
+      mkCoFix (ln,(lna,tl',bl'))
+
+(* strong *)
+let map_constr_with_full_binders g f l c = match kind_of_term c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> c
+  | Cast (c,t) -> mkCast (f l c, f l t)
+  | Prod (na,t,c) -> mkProd (na, f l t, f (g (na,None,t) l) c)
+  | Lambda (na,t,c) -> mkLambda (na, f l t, f (g (na,None,t) l) c)
+  | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g (na,Some b,t) l) c)
+  | App (c,al) -> mkApp (f l c, Array.map (f l) al)
+  | Evar (e,al) -> mkEvar (e, Array.map (f l) al)
+  | Case (ci,p,c,bl) -> mkCase (ci, f l p, f l c, Array.map (f l) bl)
+  | Fix (ln,(lna,tl,bl)) ->
+      let l' =
+        array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+      mkFix (ln,(lna,Array.map (f l) tl, Array.map (f l') bl))
+  | CoFix(ln,(lna,tl,bl)) ->
+      let l' =
+        array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+      mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
+
+  
+(* [iter_constr f c] iters [f] on the immediate subterms of [c]; it is
+   not recursive and the order with which subterms are processed is
+   not specified *)
+
+let iter_constr f c = match kind_of_term c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _ | Construct _) -> ()
+  | Cast (c,t) -> f c; f t
+  | Prod (_,t,c) -> f t; f c
+  | Lambda (_,t,c) -> f t; f c
+  | LetIn (_,b,t,c) -> f b; f t; f c
+  | App (c,l) -> f c; Array.iter f l
+  | Evar (_,l) -> Array.iter f l
+  | Case (_,p,c,bl) -> f p; f c; Array.iter f bl
+  | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
+  | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
+
+ 
+(***************************)
+(* occurs check functions  *)                         
+(***************************)
+
+exception Occur
+
+let occur_meta c =
+  let rec occrec c = match kind_of_term c with
+    | Meta _ -> raise Occur
+    | _ -> iter_constr occrec c
+  in try occrec c; false with Occur -> true
+
+let occur_existential c = 
+  let rec occrec c = match kind_of_term c with
+    | Evar _ -> raise Occur
+    | _ -> iter_constr occrec c
+  in try occrec c; false with Occur -> true
+
+let occur_const s c = 
+  let rec occur_rec c = match kind_of_term c with
+    | Const sp when sp=s -> raise Occur
+    | _ -> iter_constr occur_rec c
+  in 
+  try occur_rec c; false with Occur -> true
+
+let occur_evar n c = 
+  let rec occur_rec c = match kind_of_term c with
+    | Evar (sp,_) when sp=n -> raise Occur
+    | _ -> iter_constr occur_rec c
+  in 
+  try occur_rec c; false with Occur -> true
+
+let occur_in_global env id constr =
+  let vars = vars_of_global env constr in
+  if List.mem id vars then raise Occur
+
+let occur_var env s c = 
+  let rec occur_rec c =
+    occur_in_global env s c;
+    iter_constr occur_rec c
+  in 
+  try occur_rec c; false with Occur -> true
+
+let occur_var_in_decl env hyp (_,c,typ) =
+  match c with
+    | None -> occur_var env hyp (body_of_type typ)
+    | Some body ->
+        occur_var env hyp (body_of_type typ) ||
+        occur_var env hyp body
+
+(* (dependent M N) is true iff M is eq_term with a subterm of N 
+   M is appropriately lifted through abstractions of N *)
+
+let dependent m t =
+  let rec deprec m t =
+    if (eq_constr m t) then
+      raise Occur
+    else
+      iter_constr_with_binders (lift 1) deprec m t
+  in 
+  try deprec m t; false with Occur -> true
+
+(* returns the list of free debruijn indices in a term *)
+
+let free_rels m = 
+  let rec frec depth acc c = match kind_of_term c with
+    | Rel n       -> if n >= depth then Intset.add (n-depth+1) acc else acc
+    | _ -> fold_constr_with_binders succ frec depth acc c
+  in 
+  frec 1 Intset.empty m
+
+
+(***************************)
+(*  substitution functions *)                         
+(***************************)
+
+(* First utilities for avoiding telescope computation for subst_term *)
+
+let prefix_application (k,c) (t : constr) = 
+  let c' = collapse_appl c and t' = collapse_appl t in
+  match kind_of_term c', kind_of_term t' with
+    | App (f1,cl1), App (f2,cl2) ->
+	let l1 = Array.length cl1
+	and l2 = Array.length cl2 in
+	if l1 <= l2
+	   && eq_constr c' (mkApp (f2, Array.sub cl2 0 l1)) then
+	  Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1)))
+	else 
+	  None
+    | _ -> None
+
+let my_prefix_application (k,c) (by_c : constr) (t : constr) = 
+  let c' = collapse_appl c and t' = collapse_appl t in
+  match kind_of_term c', kind_of_term t' with
+    | App (f1,cl1), App (f2,cl2) ->
+	let l1 = Array.length cl1
+	and l2 = Array.length cl2 in
+	if l1 <= l2
+	   && eq_constr c' (mkApp (f2, Array.sub cl2 0 l1)) then
+	  Some (mkApp ((lift k by_c), Array.sub cl2 l1 (l2 - l1)))
+	else 
+	  None
+    | _ -> None
+
+(* Recognizing occurrences of a given (closed) subterm in a term for Pattern :
+   [subst_term c t] substitutes [(Rel 1)] for all occurrences of (closed)
+   term [c] in a term [t] *)
+(*i Bizarre : si on cherche un sous terme clos, pourquoi le lifter ? i*)
+
+let subst_term_gen eq_fun c t = 
+  let rec substrec (k,c as kc) t =
+    match prefix_application kc t with
+      | Some x -> x
+      | None ->
+    (if eq_fun t c then mkRel k else match kind_of_term t with
+       | Const _ | Ind _ | Construct _ -> t
+       | _ ->
+	   map_constr_with_binders
+	     (fun (k,c) -> (k+1,lift 1 c))
+	     substrec kc t)
+  in 
+  substrec (1,c) t
+
+(* Recognizing occurrences of a given (closed) subterm in a term :
+   [replace_term c1 c2 t] substitutes [c2] for all occurrences of (closed)
+   term [c1] in a term [t] *)
+(*i Meme remarque : a priori [c] n'est pas forcement clos i*)
+
+let replace_term_gen eq_fun c by_c in_t = 
+  let rec substrec (k,c as kc) t =
+    match my_prefix_application kc by_c t with
+      | Some x -> x
+      | None ->
+    (if eq_fun t c then (lift k by_c) else match kind_of_term t with
+       | Const _ | Ind _ | Construct _ -> t
+       | _ ->
+	   map_constr_with_binders
+	     (fun (k,c) -> (k+1,lift 1 c))
+	     substrec kc t)
+  in 
+  substrec (0,c) in_t
+
+let subst_term = subst_term_gen eq_constr
+
+let replace_term = replace_term_gen eq_constr
+
+let rec subst_meta bl c = 
+  match kind_of_term c with
+    | Meta i -> (try List.assoc i bl with Not_found -> c)
+    | _ -> map_constr (subst_meta bl) c
+
+(* strips head casts and flattens head applications *)
+let rec strip_head_cast c = match kind_of_term c with
+  | App (f,cl) -> 
+      let rec collapse_rec f cl2 = match kind_of_term f with
+	| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
+	| Cast (c,_) -> collapse_rec c cl2
+	| _ -> if cl2 = [||] then f else mkApp (f,cl2)
+      in 
+      collapse_rec f cl
+  | Cast (c,t) -> strip_head_cast c
+  | _ -> c
+
+(* On reduit une serie d'eta-redex de tete ou rien du tout  *)
+(* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *)
+(* Remplace 2 versions précédentes buggées                  *)
+
+let rec eta_reduce_head c =
+  match kind_of_term c with
+    | Lambda (_,c1,c') ->
+	(match kind_of_term (eta_reduce_head c') with
+           | App (f,cl) ->
+               let lastn = (Array.length cl) - 1 in 
+               if lastn < 1 then anomaly "application without arguments"
+               else
+                 (match kind_of_term cl.(lastn) with
+                    | Rel 1 ->
+			let c' =
+                          if lastn = 1 then f
+			  else mkApp (f, Array.sub cl 0 lastn)
+			in
+			if not (dependent (mkRel 1) c')
+                        then lift (-1) c'
+                        else c
+                    | _   -> c)
+           | _ -> c)
+    | _ -> c
+
+(* alpha-eta conversion : ignore print names and casts *)
+let eta_eq_constr =
+  let rec aux t1 t2 =
+    let t1 = eta_reduce_head (strip_head_cast t1)
+    and t2 = eta_reduce_head (strip_head_cast t2) in
+    t1=t2 or compare_constr aux t1 t2
+  in aux
+
+(* Substitute only a list of locations locs, the empty list is
+   interpreted as substitute all, if 0 is in the list then no
+   substitution is done. The list may contain only negative occurrences
+   that will not be substituted. *)
+
+let subst_term_occ_gen locs occ c t =
+  let maxocc = List.fold_right max locs 0 in
+  let pos = ref occ in
+  let check = ref true in
+  let except = List.exists (fun n -> n<0) locs in
+  if except & (List.exists (fun n -> n>=0) locs) 
+  then error "mixing of positive and negative occurences"
+  else
+   let rec substrec (k,c as kc) t =
+    if (not except) & (!pos > maxocc) then t
+    else
+    if eq_constr t c then
+      let r = 
+	if except then 
+	  if List.mem (- !pos) locs then t else (mkRel k)
+	else 
+	  if List.mem !pos locs then (mkRel k) else t
+      in incr pos; r
+    else
+      match kind_of_term t with
+	| Const _ | Construct _ | Ind _ -> t
+	| _ ->
+	    map_constr_with_binders_left_to_right
+	      (fun (k,c) -> (k+1,lift 1 c)) substrec kc t
+  in
+  let t' = substrec (1,c) t in
+  (!pos, t')
+
+let subst_term_occ locs c t = 
+  if locs = [] then
+    subst_term c t
+  else if List.mem 0 locs then 
+    t
+  else 
+    let (nbocc,t') = subst_term_occ_gen locs 1 c t in
+    if List.exists (fun o -> o >= nbocc or o <= -nbocc) locs then
+      errorlabstrm "subst_term_occ" [< 'sTR "Too few occurences" >];
+    t'
+
+let subst_term_occ_decl locs c (id,bodyopt,typ as d) =
+  match bodyopt with
+    | None -> (id,None,subst_term_occ locs c typ)
+    | Some body -> 
+	if locs = [] then
+	  (id,Some (subst_term c body),type_app (subst_term c) typ)
+	else if List.mem 0 locs then 
+	  d
+	else 
+	  let (nbocc,body') = subst_term_occ_gen locs 1 c body in
+	  let (nbocc',t') = subst_term_occ_gen locs nbocc c typ in
+	  if List.exists (fun o -> o >= nbocc' or o <= -nbocc') locs then
+	    errorlabstrm "subst_term_occ_decl" [< 'sTR "Too few occurences" >];
+	  (id,Some body',t')
+
+
+
+(* First character of a constr *)
+
+let first_char id =
+  let id = string_of_id id in
+  assert (id <> "");
+  String.make 1 id.[0]
+
+let lowercase_first_char id = String.lowercase (first_char id)
+
+let id_of_global env ref = basename (sp_of_global env ref)
+
+let sort_hdchar = function
+  | Prop(_) -> "P"
+  | Type(_) -> "T"
+
+let hdchar env c = 
+  let rec hdrec k c =
+    match kind_of_term c with
+    | Prod (_,_,c)       -> hdrec (k+1) c
+    | Lambda (_,_,c)     -> hdrec (k+1) c
+    | LetIn (_,_,_,c)    -> hdrec (k+1) c
+    | Cast (c,_)         -> hdrec k c
+    | App (f,l)         -> hdrec k f
+    | Const sp       ->
+	let c = lowercase_first_char (basename sp) in
+	if c = "?" then "y" else c
+    | Ind ((sp,i) as x) ->
+	if i=0 then 
+	  lowercase_first_char (basename sp)
+	else 
+	  lowercase_first_char (id_of_global env (IndRef x))
+    | Construct ((sp,i) as x) ->
+	lowercase_first_char (id_of_global env (ConstructRef x))
+    | Var id  -> lowercase_first_char id
+    | Sort s -> sort_hdchar s
+    | Rel n ->
+	(if n<=k then "p" (* the initial term is flexible product/function *)
+	 else
+	   try match Environ.lookup_rel (n-k) env with
+	     | (Name id,_,_)   -> lowercase_first_char id
+	     | (Anonymous,_,t) -> hdrec 0 (lift (n-k) (body_of_type t))
+	   with Not_found -> "y")
+    | Fix ((_,i),(lna,_,_)) -> 
+	let id = match lna.(i) with Name id -> id | _ -> assert false in
+	lowercase_first_char id
+    | CoFix (i,(lna,_,_)) -> 
+	let id = match lna.(i) with Name id -> id | _ -> assert false in
+	lowercase_first_char id
+    | Meta _|Evar _|Case (_, _, _, _) -> "y"
+  in 
+  hdrec 0 c
+
+let id_of_name_using_hdchar env a = function
+  | Anonymous -> id_of_string (hdchar env a) 
+  | Name id   -> id
+
+let named_hd env a = function
+  | Anonymous -> Name (id_of_string (hdchar env a)) 
+  | x         -> x
+
+let named_hd_type env a = named_hd env (body_of_type a)
+
+let prod_name   env (n,a,b) = mkProd (named_hd_type env a n, a, b)
+let lambda_name env (n,a,b) = mkLambda (named_hd_type env a n, a, b)
+
+let prod_create   env (a,b) = mkProd (named_hd_type env a Anonymous, a, b)
+let lambda_create env (a,b) =  mkLambda (named_hd_type env a Anonymous, a, b)
+
+let name_assumption env (na,c,t) =
+  match c with
+    | None      -> (named_hd_type env t na, None, t)
+    | Some body -> (named_hd env body na, c, t)
+
+let name_context env hyps =
+  snd
+    (List.fold_left
+       (fun (env,hyps) d -> 
+	  let d' = name_assumption env d in (push_rel d' env, d' :: hyps))
+       (env,[]) (List.rev hyps))
+
+let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b 
+let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b
+
+let it_mkProd_or_LetIn_name env b hyps =
+  it_mkProd_or_LetIn b (name_context env hyps)
+let it_mkLambda_or_LetIn_name env b hyps =
+  it_mkLambda_or_LetIn b (name_context env hyps)
+
+(*************************)
+(*   Names environments  *)
+(*************************)
+type names_context = name list
+let add_name n nl = n::nl
+let lookup_name_of_rel p names =
+  try List.nth names (p-1)
+  with Invalid_argument _ | Failure _ -> raise Not_found
+let rec lookup_rel_of_name id names = 
+  let rec lookrec n = function
+    | Anonymous :: l  -> lookrec (n+1) l
+    | (Name id') :: l -> if id' = id then n else lookrec (n+1) l
+    | []            -> raise Not_found
+  in 
+  lookrec 1 names
+let empty_names_context = []
+
+let ids_of_rel_context sign =
+  Sign.fold_rel_context
+    (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l)
+    sign []
+let ids_of_named_context sign =
+  Sign.fold_named_context (fun (id,_,_) idl -> id::idl) sign []
+
+let ids_of_context env = 
+  (ids_of_rel_context (rel_context env))
+  @ (ids_of_named_context (named_context env))
+
+let names_of_rel_context env =
+  List.map (fun (na,_,_) -> na) (rel_context env)
+
+(* Nouvelle version de renommage des variables (DEC 98) *)
+(* This is the algorithm to display distinct bound variables 
+
+    - Règle 1 : un nom non anonyme, même non affiché, contribue à la liste
+      des noms à éviter 
+    - Règle 2 : c'est la dépendance qui décide si on affiche ou pas
+
+    Exemple : 
+    si bool_ind = (P:bool->Prop)(f:(P true))(f:(P false))(b:bool)(P b), alors
+    il est affiché (P:bool->Prop)(P true)->(P false)->(b:bool)(P b)
+    mais f et f0 contribue à la liste des variables à éviter (en supposant 
+    que les noms f et f0 ne sont pas déjà pris)
+    Intérêt : noms homogènes dans un but avant et après Intro
+*)
+
+type used_idents = identifier list
+
+let occur_rel p env id = 
+  try lookup_name_of_rel p env = Name id
+  with Not_found -> false (* Unbound indice : may happen in debug *)
+
+let occur_id env id0 c =
+  let rec occur n c = match kind_of_term c with
+    | Var id when  id=id0 -> raise Occur
+    | Const sp when basename sp = id0 -> raise Occur
+    | Ind ind_sp
+	when basename (path_of_inductive (Global.env()) ind_sp) = id0 ->
+        raise Occur
+    | Construct cstr_sp
+	when basename (path_of_constructor (Global.env()) cstr_sp) = id0 ->
+        raise Occur
+    | Rel p when p>n & occur_rel (p-n) env id0 -> raise Occur
+    | _ -> iter_constr_with_binders succ occur n c
+  in 
+  try occur 1 c; false
+  with Occur -> true
+
+let next_name_not_occuring name l env_names t =
+  let rec next id =
+    if List.mem id l or occur_id env_names id t then next (lift_ident id)
+    else id
+  in 
+  match name with
+    | Name id   -> next id
+    | Anonymous -> id_of_string "_"
+
+(* Remark: Anonymous var may be dependent in Evar's contexts *)
+let concrete_name l env_names n c =
+  if n = Anonymous & not (dependent (mkRel 1) c) then
+    (None,l)
+  else
+    let fresh_id = next_name_not_occuring n l env_names c in
+    let idopt = if dependent (mkRel 1) c then (Some fresh_id) else None in
+    (idopt, fresh_id::l)
+
+let concrete_let_name l env_names n c =
+  let fresh_id = next_name_not_occuring n l env_names c in
+  (Name fresh_id, fresh_id::l)
+
+let global_vars env ids = Idset.elements (global_vars_set env ids)
+
+let rec rename_bound_var env l c =
+  match kind_of_term c with
+  | Prod (Name s,c1,c2)  ->
+      if dependent (mkRel 1) c2 then
+        let s' = next_ident_away s (global_vars env c2@l) in
+        let env' = push_rel (Name s',None,c1) env in
+        mkProd (Name s', c1, rename_bound_var env' (s'::l) c2)
+      else 
+        let env' = push_rel (Name s,None,c1) env in
+	mkProd (Name s, c1, rename_bound_var env' l c2)
+  | Prod (Anonymous,c1,c2) ->
+        let env' = push_rel (Anonymous,None,c1) env in
+        mkProd (Anonymous, c1, rename_bound_var env' l c2)
+  | Cast (c,t) -> mkCast (rename_bound_var env l c, t)
+  | x -> c
+
+(* iterator on rel context *)
+let process_rel_context f env =
+  let sign = named_context env in
+  let rels = rel_context env in
+  let env0 = reset_with_named_context sign env in
+  Sign.fold_rel_context f rels env0
+
+let assums_of_rel_context sign =
+  Sign.fold_rel_context
+    (fun (na,c,t) l ->
+      match c with
+          Some _ -> l
+        | None -> (na,body_of_type t)::l)
+    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)
+	::(liftrec (k-1) sign)
+    | [] -> []
+  in
+  liftrec (rel_context_length sign) sign
+
+let fold_named_context_both_sides = list_fold_right_and_left
+
+let rec mem_named_context id = function
+  | (id',_,_) :: _ when id=id' -> true
+  | _ :: sign -> mem_named_context id sign
+  | [] -> false
+
+let make_all_name_different env =
+  let avoid = ref (ids_of_named_context (named_context env)) in
+  process_rel_context
+    (fun (na,c,t) newenv -> 
+       let id = next_name_away na !avoid in
+       avoid := id::!avoid;
+       push_rel (Name id,c,t) newenv)
+    env
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
new file mode 100644
index 0000000000..30a7fa8ca4
--- /dev/null
+++ b/pretyping/termops.mli
@@ -0,0 +1,143 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Util
+open Pp
+open Names
+open Term
+open Sign
+open Environ
+
+val print_sort : sorts -> std_ppcmds
+val prod_it : init:types -> (name * types) list -> types
+val lam_it : init:constr -> (name * types) list -> constr
+val rel_vect : int -> int -> constr array
+val rel_list : int -> int -> constr list
+val extended_rel_list : int -> rel_context -> constr list
+val extended_rel_vect : int -> rel_context -> constr array
+val push_rel_assum : name * types -> env -> env
+val push_rels_assum : (name * types) list -> env -> env
+val push_named_rec_types : name array * types array * 'a -> env -> env
+val lookup_rel_id : identifier -> rel_context -> int * types
+val mkProd_or_LetIn : rel_declaration -> types -> types
+val mkProd_wo_LetIn : rel_declaration -> types -> types
+val it_mkProd_wo_LetIn : init:types -> rel_context -> types
+val it_mkProd_or_LetIn   : init:types -> rel_context -> types
+val it_mkLambda_or_LetIn : init:constr -> rel_context -> constr
+val it_named_context_quantifier :
+  (named_declaration -> 'a -> 'a) -> init:'a -> named_context -> 'a
+val it_mkNamedProd_or_LetIn   : init:types -> named_context -> types
+val it_mkNamedLambda_or_LetIn : init:constr -> named_context -> constr
+
+val map_constr_with_named_binders :
+  (name -> 'a -> 'a) ->
+  ('a -> types -> types) -> 'a -> constr -> constr
+val map_constr_with_binders_left_to_right :
+  ('a -> 'a) -> ('a -> types -> types) -> 'a -> constr -> constr
+val map_constr_with_full_binders :
+  (name * types option * types -> 'a -> 'a) ->
+  ('a -> types -> types) -> 'a -> constr -> constr
+val iter_constr : (types -> unit) -> constr -> unit
+
+(* occur checks *)
+exception Occur
+val occur_meta : types -> bool
+val occur_existential : types -> bool
+val occur_const : constant -> types -> bool
+val occur_evar : existential_key -> types -> bool
+val occur_in_global : env -> identifier -> constr -> unit
+val occur_var : env -> identifier -> types -> bool
+val occur_var_in_decl :
+  env ->
+  identifier -> 'a * types option * types -> bool
+val dependent : constr -> constr -> bool
+val free_rels : constr -> Intset.t
+
+(* substitution *)
+val prefix_application :
+  int * constr -> constr -> constr option
+val my_prefix_application :
+  int * constr -> constr -> constr -> constr option
+val subst_term_gen :
+  (constr -> constr -> bool) ->
+  constr -> constr -> constr
+val replace_term_gen :
+  (constr -> constr -> bool) ->
+  constr -> constr -> constr -> constr
+val subst_term : constr -> constr -> constr
+val replace_term : constr -> constr -> constr -> constr
+val subst_meta : (int * constr) list -> constr -> constr
+val strip_head_cast : constr -> constr
+val eta_reduce_head : constr -> constr
+val eta_eq_constr : constr -> constr -> bool
+val subst_term_occ_gen :
+  int list -> int -> constr -> types -> int * types
+val subst_term_occ : int list -> constr -> types -> types
+val subst_term_occ_decl :
+  int list -> constr -> named_declaration -> named_declaration
+
+(* finding "intuitive" names to hypotheses *)
+val first_char : identifier -> string
+val lowercase_first_char : identifier -> string
+val id_of_global : env -> Nametab.global_reference -> identifier
+val sort_hdchar : sorts -> string
+val hdchar : env -> types -> string
+val id_of_name_using_hdchar :
+  env -> types -> name -> identifier
+val named_hd : env -> types -> name -> name
+val named_hd_type : env -> types -> name -> name
+val prod_name : env -> name * types * types -> constr
+val lambda_name : env -> name * types * constr -> constr
+val prod_create : env -> types * types -> constr
+val lambda_create : env -> types * constr -> constr
+val name_assumption : env -> rel_declaration -> rel_declaration
+val name_context : env -> rel_context -> rel_context
+
+val mkProd_or_LetIn_name : env -> types -> rel_declaration -> types
+val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr
+val it_mkProd_or_LetIn_name   : env -> types -> rel_context -> types
+val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
+
+(* name contexts *)
+type names_context = name list
+val add_name : name -> names_context -> names_context
+val lookup_name_of_rel : int -> names_context -> name
+val lookup_rel_of_name : identifier -> names_context -> int
+val empty_names_context : names_context
+val ids_of_rel_context : rel_context -> identifier list
+val ids_of_named_context : named_context -> identifier list
+val ids_of_context : env -> identifier list
+val names_of_rel_context : env -> names_context
+
+(* sets of free identifiers *)
+type used_idents = identifier list
+val occur_rel : int -> name list -> identifier -> bool
+val occur_id : name list -> identifier -> constr -> bool
+
+val next_name_not_occuring :
+  name -> identifier list -> name list -> constr -> identifier
+val concrete_name :
+  identifier list -> name list -> name ->
+  constr -> identifier option * identifier list
+val concrete_let_name :
+  identifier list -> name list ->
+  name -> constr -> name * identifier list
+val global_vars : env -> constr -> identifier list
+val rename_bound_var : env -> identifier list -> types -> types
+
+(* other signature iterators *)
+val process_rel_context : (rel_declaration -> env -> env) -> env -> env
+val assums_of_rel_context : rel_context -> (name * constr) list
+val lift_rel_context : int -> rel_context -> rel_context
+val fold_named_context_both_sides :
+  ('a -> named_declaration -> named_context -> 'a) ->
+    named_context -> 'a -> 'a
+val mem_named_context : identifier -> named_context -> bool
+val make_all_name_different : env -> env
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index f9110c62ae..7dd552e383 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -12,8 +12,10 @@ open Util
 open Names
 open Term
 open Environ
-open Reduction
+open Reductionops
 open Type_errors
+open Pretype_errors
+open Inductive
 open Typeops
 
 let vect_lift = Array.mapi lift
@@ -26,111 +28,108 @@ type 'a mach_flags = {
 (* The typing machine without information, without universes but with
    existential variables. *)
 
+let assumption_of_judgment env sigma j =
+  assumption_of_judgment env (j_nf_evar sigma j)
+
+let type_judgment env sigma j =
+  type_judgment env (j_nf_evar sigma j)
+
+
 let rec execute mf env sigma cstr =
   match kind_of_term cstr with
-    | IsMeta n ->
+    | Meta n ->
 	error "execute: found a non-instanciated goal"
 
-    | IsEvar ev ->
-	let ty = type_of_existential env sigma ev in
+    | Evar ev ->
+	let ty = Instantiate.existential_type sigma ev in
 	let jty = execute mf env sigma ty in
 	let jty = assumption_of_judgment env sigma jty in
 	{ uj_val = cstr; uj_type = jty }
 	
-    | IsRel n -> 
-	relative env n
-
-    | IsVar id -> 
-      (try
-         make_judge cstr (snd (lookup_named id env))
-       with Not_found ->
-         error ("execute: variable " ^ (string_of_id id) ^ " not defined"))
+    | Rel n -> 
+	judge_of_relative env n
+
+    | Var id -> 
+        judge_of_variable env id
 	  
-    | IsConst c ->
-        make_judge cstr (type_of_constant env sigma c)
+    | Const c ->
+        make_judge cstr (constant_type env c)
 	  
-    | IsMutInd ind ->
-	make_judge cstr (type_of_inductive env sigma ind)
+    | Ind ind ->
+	make_judge cstr (type_of_inductive env ind)
 	  
-    | IsMutConstruct cstruct -> 
-	make_judge cstr (type_of_constructor env sigma cstruct)
+    | Construct cstruct -> 
+	make_judge cstr (type_of_constructor env cstruct)
 	  
-    | IsMutCase (ci,p,c,lf) ->
+    | Case (ci,p,c,lf) ->
         let cj = execute mf env sigma c in
         let pj = execute mf env sigma p in
         let lfj = execute_array mf env sigma lf in
-        let (j,_) = judge_of_case env sigma ci pj cj lfj in
+        let (j,_) = judge_of_case env ci pj cj lfj in
         j
   
-    | IsFix ((vn,i as vni),recdef) ->
+    | Fix ((vn,i as vni),recdef) ->
         if (not mf.fix) && array_exists (fun n -> n < 0) vn then
           error "General Fixpoints not allowed";
-        let (_,tys,_ as recdef') = execute_fix mf env sigma recdef in
+        let (_,tys,_ as recdef') = execute_recdef mf env sigma recdef in
 	let fix = (vni,recdef') in
-        check_fix env sigma fix;
+        check_fix env fix;
 	make_judge (mkFix fix) tys.(i)
 	  
-    | IsCoFix (i,recdef) ->
-        let (_,tys,_ as recdef') = execute_fix mf env sigma recdef in
+    | CoFix (i,recdef) ->
+        let (_,tys,_ as recdef') = execute_recdef mf env sigma recdef in
         let cofix = (i,recdef') in
-        check_cofix env sigma cofix;
+        check_cofix env cofix;
 	make_judge (mkCoFix cofix) tys.(i)
 	  
-    | IsSort (Prop c) -> 
+    | Sort (Prop c) -> 
 	judge_of_prop_contents c
 
-    | IsSort (Type u) ->
+    | Sort (Type u) ->
 	let (j,_) = judge_of_type u in j
 	  
-    | IsApp (f,args) ->
+    | App (f,args) ->
 	let j = execute mf env sigma f in
-        let jl = execute_list mf env sigma (Array.to_list args) in
-	let (j,_) = apply_rel_list env sigma mf.nocheck jl j in
+        let jl = execute_array mf env sigma args in
+	let (j,_) = judge_of_apply env j jl in
 	j
 	    
-    | IsLambda (name,c1,c2) -> 
+    | Lambda (name,c1,c2) -> 
         let j = execute mf env sigma c1 in
-	let var = assumption_of_judgment env sigma j in
-	let env1 = push_rel_assum (name,var) env in
+	let var = type_judgment env sigma j in
+	let env1 = push_rel (name,None,var.utj_val) env in
         let j' = execute mf env1 sigma c2 in 
-        let (j,_) = abs_rel env1 sigma name var j' in
-	j
+        judge_of_abstraction env1 name var j'
 	  
-    | IsProd (name,c1,c2) ->
+    | Prod (name,c1,c2) ->
         let j = execute mf env sigma c1 in
         let varj = type_judgment env sigma j in
-	let env1 = push_rel_assum (name,varj.utj_val) env in
+	let env1 = push_rel (name,None,varj.utj_val) env in
         let j' = execute mf env1 sigma c2 in
         let varj' = type_judgment env sigma j' in
-	let (j,_) = gen_rel env1 sigma name varj varj' in
+	let (j,_) = judge_of_product env1 name varj varj' in
 	j
 
-     | IsLetIn (name,c1,c2,c3) ->
-        let j1 = execute mf env sigma c1 in
-        let j2 = execute mf env sigma c2 in
-	let tj2 = assumption_of_judgment env sigma j2 in
-	let { uj_val = b; uj_type = t },_ = cast_rel env sigma j1 tj2 in
-        let j3 = execute mf (push_rel_def (name,b,t) env) sigma c3 in
-	{ uj_val = mkLetIn (name, j1.uj_val, tj2, j3.uj_val) ;
-	  uj_type = type_app (subst1 j1.uj_val) j3.uj_type }
+     | LetIn (name,c1,c2,c3) ->
+        let j1 = execute mf env sigma (mkCast (c1, c2)) in
+        let env1 = push_rel (name,Some j1.uj_val,j1.uj_type) env in
+        let j3 = execute mf env1 sigma c3 in
+        judge_of_letin env name j1 j3
   
-    | IsCast (c,t) ->
+    | Cast (c,t) ->
         let cj = execute mf env sigma c in
         let tj = execute mf env sigma t in
-	let tj = assumption_of_judgment env sigma tj in
-        let j, _ = cast_rel env sigma cj tj in
+	let tj = type_judgment env sigma tj in
+        let j, _ = judge_of_cast env cj tj in
 	j
-	  
-and execute_fix mf env sigma (names,lar,vdef) =
+
+and execute_recdef mf env sigma (names,lar,vdef) =
   let larj = execute_array mf env sigma lar in
   let lara = Array.map (assumption_of_judgment env sigma) larj in
-  let ctxt = 
-    array_map2_i (fun i na ty -> (na, type_app (lift i) ty)) names lara in
-  let env1 = 
-    Array.fold_left (fun env nvar -> push_rel_assum nvar env) env ctxt in
+  let env1 = push_rec_types (names,lara,vdef) env in
   let vdefj = execute_array mf env1 sigma vdef in
   let vdefv = Array.map j_val vdefj in
-  let cst3 = type_fixpoint env1 sigma names lara vdefj in
+  let _ = type_fixpoint env1 names lara vdefj in
   (names,lara,vdefv)
 
 and execute_array mf env sigma v =