Ajout d'un LetIn primitif.

Abstraction de constr via kind_of_constr dans une bonne partie du code.


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

13 files changed, 425 insertions, 405 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1d25ba84d..b01b3e283 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1,7 +1,7 @@
 
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Declarations
 open Inductive
@@ -22,7 +22,7 @@ open Evarconv
 (* This was previously in Indrec but creates existential holes       *)
 
 let mkExistential isevars env =
-  new_isevar isevars env (mkCast dummy_sort dummy_sort) CCI
+  new_isevar isevars env (mkCast (dummy_sort, dummy_sort)) CCI
 
 let norec_branch_scheme env isevars cstr =
   it_mkProd_or_LetIn (mkExistential isevars env) cstr.cs_args 
@@ -31,14 +31,16 @@ let rec_branch_scheme env isevars ((sp,j),_) recargs cstr =
   let rec crec (args,recargs) = 
     match args, recargs with 
       | (name,None,c)::rea,(ra::reca) -> 
-          DOP2(Prod,body_of_type c,DLAM(name,
-	       match ra with 
-		 | Mrec k when k=j -> 
-		     mkArrow (mkExistential isevars env)
-		       (crec (List.rev (lift_rel_context 1 (List.rev rea)),reca))
-                 | _ -> crec (rea,reca)))
-      | (name,Some d,c)::rea, reca -> failwith "TODO"
-(*	  mkLetIn (name,d,body_of_type c,crec (rea,reca))) *)
+	  let d =
+ 	    match ra with 
+	      | Mrec k when k=j -> 
+		  mkArrow (mkExistential isevars env)
+		    (crec (List.rev (lift_rel_context 1 (List.rev rea)),reca))
+              | _ -> crec (rea,reca) in
+          mkProd (name, body_of_type c, d)
+
+      | (name,Some d,c)::rea, reca -> 
+	  mkLetIn (name, d, body_of_type c, crec (rea,reca))
       | [],[] -> mkExistential isevars env
       | _ -> anomaly "rec_branch_scheme"
   in 
@@ -58,9 +60,9 @@ 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 c else 
-    match whd_betadeltaiota env sigma c with
-      | DOP2(Prod,_,DLAM(n,c_0)) -> decrec (m-1) c_0
-      | _                        -> failwith "Typing.concl_n"
+    match kind_of_term (whd_betadeltaiota env sigma c) with
+      | IsProd (n,_,c_0) -> decrec (m-1) c_0
+      | _                -> failwith "Typing.concl_n"
   in 
   decrec
 
@@ -378,9 +380,9 @@ let dependencies_in_rhs nargs eqns =
    already dependent *)
 
 let rec is_dep_on_previous n t = function
-  | ((_,IsInd _),_)::_ when dependent (Rel n) t -> DepOnPrevious
+  | ((_,IsInd _),_)::_ when dependent (mkRel n) t -> DepOnPrevious
   | ((_,NotInd _),(DepOnPrevious,DepInRhs))::_ 
-      when dependent (Rel n) t -> DepOnPrevious
+      when dependent (mkRel n) t -> DepOnPrevious
   | _::rest -> is_dep_on_previous (n+1) t rest
   | [] -> NotDepOnPrevious
 
@@ -513,11 +515,13 @@ let noccur_between_without_evar n m term =
     | VAR _         -> ()
     | DOPN(Evar _,cl) -> ()
     | DOPN(_,cl)    -> Array.iter (occur_rec n) cl
-    | DOPL(_,cl)    -> List.iter (occur_rec n) cl
     | DOP1(_,c)     -> occur_rec n c
     | DOP2(_,c1,c2) -> occur_rec n c1; occur_rec n c2
     | DLAM(_,c)     -> occur_rec (n+1) c
     | DLAMV(_,v)    -> Array.iter (occur_rec (n+1)) v
+    | CLam (_,t,c)   -> occur_rec n (body_of_type t); occur_rec (n+1) c
+    | CPrd (_,t,c)   -> occur_rec n (body_of_type t); occur_rec (n+1) c
+    | CLet (_,b,t,c) -> occur_rec n b; occur_rec n (body_of_type t); occur_rec (n+1) c
     | _             -> ()
   in 
   try occur_rec n term; true with Occur -> false
@@ -645,7 +649,7 @@ let rec weaken_predicate n pred =
 
 let rec extract_predicate = function
   | PrProd ((_,na,t),pred) ->
-      mkProd na (type_of_tomatch_type t) (extract_predicate pred)
+      mkProd (na, type_of_tomatch_type t, extract_predicate pred)
   | PrLetIn ((args,Some c),pred) -> substl (c::(List.rev args)) (extract_predicate pred)
   | PrLetIn ((args,None),pred) -> substl (List.rev args) (extract_predicate pred)
   | PrCcl ccl -> ccl
@@ -962,9 +966,9 @@ let build_expected_arity env isevars isdep tomatchl =
     | tm::ltm ->
 	let (ty1,aritysign) = cook n tm in
 	let rec follow n = function
-	  | (na,ty2)::sign -> DOP2(Prod,ty2,DLAM(na,follow (n+1) sign))
+	  | (na,ty2)::sign -> mkProd (na, ty2, follow (n+1) sign)
 	  | _ ->
-	      if isdep then DOP2(Prod,ty1,DLAM(Anonymous,buildrec (n+1) ltm))
+	      if isdep then mkProd (Anonymous, ty1, buildrec (n+1) ltm)
 	      else buildrec n ltm
 	in follow n (List.rev aritysign)
   in buildrec 0 tomatchl
@@ -988,17 +992,18 @@ let build_initial_predicate isdep pred tomatchl =
   in buildrec 0 pred tomatchl
 
 let rec eta_expand0 env sigma n c t =
-  match whd_betadeltaiota env sigma t with
-      DOP2(Prod,a,DLAM(na,b)) ->
-	DOP2(Lambda,a,DLAM(na,eta_expand0 env sigma (n+1) c b))
-   | _ -> applist (lift n c, rel_list 0 n)
+  match kind_of_term (whd_betadeltaiota env sigma t) with
+    | IsProd (na,a,b) -> mkLambda (na,a,eta_expand0 env sigma (n+1) c b)
+    | _ -> applist (lift n c, rel_list 0 n)
 
 
 let rec eta_expand env sigma c t =
-  match whd_betadeltaiota env sigma c, whd_betadeltaiota env sigma t with
-   | (DOP2(Lambda,ta,DLAM(na,cb)), DOP2(Prod,_,DLAM(_,tb))) ->
-       DOP2(Lambda,ta,DLAM(na,eta_expand env sigma cb tb))
-   | (c, t) -> eta_expand0 env sigma 0 c t
+  let c' = whd_betadeltaiota env sigma c in 
+  let t' = whd_betadeltaiota env sigma t in
+  match kind_of_term c', kind_of_term t' with
+   | IsLambda (na,ta,cb), IsProd (_,_,tb) ->
+       mkLambda (na,ta,eta_expand env sigma cb tb)
+   | _, _ -> eta_expand0 env sigma 0 c' t'
 
 (* determines wether the multiple case is dependent or not. For that
  * the predicate given by the user is eta-expanded. If the result
diff --git a/pretyping/class.ml b/pretyping/class.ml
index 419bd1bf3..5c56ce9b6 100644
--- a/pretyping/class.ml
+++ b/pretyping/class.ml
@@ -4,7 +4,7 @@
 open Util
 open Pp
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Inductive
 open Declarations
@@ -129,6 +129,7 @@ let constructor_at_head1 t =
       | IsAppL(f,args) -> 
 	  let t',_,l,c,_ = aux f in t',args,l,c,List.length args
       | IsProd (_,_,_) -> t',[],[],CL_FUN,0
+      | IsLetIn (_,_,_,c) -> aux c
       | IsSort _ -> t',[],[],CL_SORT,0
       |  _ -> raise Not_found
   in 
@@ -203,23 +204,15 @@ let get_target t ind =
     let v2,_,_,cl2,p2 = constructor_at_head1 t in cl2,p2,v2
 
 let prods_of t = 
-  let rec aux acc = function
-    | DOP2(Prod,c1,DLAM(_,c2)) -> aux (c1::acc) c2
-    | (DOP2(Cast,c,_)) -> aux acc c
-    | t -> t::acc
+  let rec aux acc d = match kind_of_term d with
+    | IsProd (_,c1,c2) -> aux (c1::acc) c2
+    | IsCast (c,_) -> aux acc c
+    | _ -> d::acc
   in 
   aux [] t
 
 (* coercion identite' *)
 
-let lams_of t = 
-  let rec aux acc = function
-    | DOP2(Lambda,c1,DLAM(x,c2)) -> aux ((x,c1)::acc) c2
-    | DOP2(Cast,c,_) -> aux acc c
-    | t -> acc,t
-  in 
-  aux [] t
-
 let build_id_coercion idf_opt ids =
   let env = Global.env () in
   let vs = construct_reference env CCI ids in 
@@ -234,24 +227,22 @@ let build_id_coercion idf_opt ids =
           [< 'sTR(string_of_id ids); 
 	     'sTR" must be a transparent constant" >] 
   in
-  let lams,t = lams_of c in
-  let lams = List.rev lams in
+  let lams,t = Sign.decompose_lam_assum c in
   let llams = List.length lams in
+  let lams = List.rev lams in
   let val_f =
-    List.fold_right
-      (fun (x,t) u -> DOP2(Lambda,t,DLAM(x,u)))
-      lams
-      (DOP2(Lambda,(applistc vs (rel_list 0 llams)),
-	    DLAM(Name (id_of_string "x"),Rel 1))) 
+    it_mkLambda_or_LetIn
+      (mkLambda (Name (id_of_string "x"),
+		 applistc vs (rel_list 0 llams),
+		 Rel 1))
+       lams
   in
   let typ_f =
-    List.fold_right
-      (fun (x,t) c -> DOP2(Prod,t,DLAM(x,c)))
+    it_mkProd_wo_LetIn
+      (mkProd (Anonymous, applistc vs (rel_list 0 llams), lift 1 t))
       lams
-      (DOP2(Prod,(applistc vs (rel_list 0 llams)),
-	    DLAM(Anonymous,lift 1 t))) 
-  in 
-  let constr_f = DOP2(Cast,val_f,typ_f) in
+  in
+  let constr_f = mkCast (val_f, typ_f) in
   (* juste pour verification *)
   let _ = 
     try 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 230c2cb84..4e991a5fd 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -9,7 +9,7 @@ open Environ
 open Libobject
 open Declare
 open Term
-open Generic
+(*i open Generic i*)
 open Rawterm
 
 (* usage qque peu general: utilise aussi dans record *)
@@ -188,14 +188,15 @@ let _ =
 (* constructor_at_head : constr -> cl_typ * int *)
 
 let constructor_at_head t = 
-  let rec aux t' = match t' with
-    | VAR id -> CL_Var id,0
-    | DOPN(Const sp,_) -> CL_SP sp,0
-    | DOPN(MutInd ind_sp,_) -> CL_IND ind_sp,0
-    | DOP2(Prod,_,DLAM(_,c)) -> CL_FUN,0
-    | DOP0(Sort(_)) -> CL_SORT,0
-    | DOP2(Cast,c,_) -> aux (collapse_appl c)
-    | DOPN(AppL,cl) -> let c,_ = aux (array_hd cl) in c,Array.length(cl)-1
+  let rec aux t' = match kind_of_term t' with
+    | IsVar id -> CL_Var id,0
+    | IsConst (sp,_) -> CL_SP 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)
+    | IsAppL (f,args) -> let c,_ = aux f in c, List.length args
     |  _ -> raise Not_found
   in 
   aux (collapse_appl t)
@@ -230,11 +231,11 @@ let fully_applied id p p1 =
   if p <> p1 then  errorlabstrm "fully_applied" 
     [< 'sTR"Wrong number of parameters for ";'sTR(string_of_id id) >]
 
-let rec arity_sort = function
-  | DOP0(Sort(Prop(_))) -> 0
-  | DOP0(Sort(Type(_))) -> 0
-  | DOP2(Prod,_,DLAM(_,c)) -> (arity_sort c) +1
-  | DOP2(Cast,c,_) -> arity_sort c
+let rec arity_sort a = match kind_of_term a with
+  | IsSort (Prop _ | Type _) -> 0
+  | IsProd (_,_,c) -> (arity_sort c) +1
+  | IsLetIn (_,_,_,c) -> arity_sort c    (* Utile ?? *)
+  | IsCast (c,_) -> arity_sort c
   | _ -> raise Not_found
 
 let stre_of_cl = function 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 8269a4741..d4a7ef4a6 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -1,7 +1,7 @@
 (* $Id$ *)
 
 open Util
-open Generic
+(*i open Generic i*)
 open Names
 open Term
 open Reduction
@@ -30,8 +30,8 @@ let apply_coercion_args env argl funj =
               uj_type= typed_app (fun _ -> typ) funj.uj_type }
     | h::restl ->
       (* On devrait pouvoir s'arranger pour qu'on ait pas à faire hnf_constr *)
-  	match whd_betadeltaiota env Evd.empty typ with
-	  | DOP2(Prod,c1,DLAM(_,c2)) -> 
+  	match kind_of_term (whd_betadeltaiota env Evd.empty typ) with
+	  | IsProd (_,c1,c2) -> 
               (* Typage garanti par l'appel a app_coercion*)
 	      apply_rec (h::acc) (subst1 h c2) restl
 	  | _ -> anomaly "apply_coercion_args"
@@ -60,8 +60,9 @@ let apply_pcoercion env p hj typ_cl =
   with _ -> anomaly "apply_pcoercion"
 
 let inh_app_fun env isevars j = 
-  match whd_betadeltaiota env !isevars (body_of_type j.uj_type) with
-    | DOP2(Prod,_,DLAM(_,_)) -> j
+  let t = whd_betadeltaiota env !isevars (body_of_type j.uj_type) in
+  match kind_of_term t with
+    | IsProd (_,_,_) -> j
     | _ ->
        	(try
  	   let t,i1 = class_of1 env !isevars (body_of_type j.uj_type) in
@@ -116,13 +117,13 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj =
       inh_coerce_to_fail env isevars c1 hj
     with NoCoercion ->  (* try ... with _ -> ... is BAD *)
       (*   (match (hnf_constr !isevars t,hnf_constr !isevars c1) with*)
-      (match (whd_betadeltaiota env !isevars t,
-	      whd_betadeltaiota env !isevars c1) with
-	 | (DOP2(Prod,t1,DLAM(_,t2)),DOP2(Prod,u1,DLAM(name,u2))) -> 
+      (match kind_of_term (whd_betadeltaiota env !isevars t),
+	     kind_of_term (whd_betadeltaiota env !isevars c1) with
+	 | IsProd (_,t1,t2), IsProd (name,u1,u2) -> 
  	     (* let v' = hnf_constr !isevars v in *)
              let v' = whd_betadeltaiota env !isevars v in
-             if (match v' with
-                   | DOP2(Lambda,v1,DLAM(_,v2)) ->
+             if (match kind_of_term v' with
+                   | IsLambda (_,v1,v2) ->
                        the_conv_x env isevars v1 u1 (* leq v1 u1? *)
                    | _  -> false)
              then 
@@ -162,7 +163,7 @@ let inh_conv_coerce_to loc env isevars cj tj =
       let at = nf_ise1 !isevars (body_of_type tj) in
       error_actual_type_loc loc env rcj.uj_val (body_of_type rcj.uj_type) at
   in
-  { uj_val = (* mkCast *) cj'.uj_val (* (body_of_type tj) *);
+  { uj_val = cj'.uj_val;
     uj_type = tj }
 
 let inh_apply_rel_list nocheck apploc env isevars argjl funj tycon =
@@ -179,8 +180,8 @@ let inh_apply_rel_list nocheck apploc env isevars argjl funj tycon =
 	   | None -> resj)
 
     | hj::restjl ->
-      	match whd_betadeltaiota env !isevars typ with
-          | DOP2(Prod,c1,DLAM(_,c2)) ->
+      	match kind_of_term (whd_betadeltaiota env !isevars typ) with
+          | IsProd (_,c1,c2) ->
               let hj' =
               	if nocheck then 
 		  hj 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 90697191a..596310512 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Univ
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Inductive
 open Sign
@@ -44,9 +44,11 @@ let occur_id env_names id0 c =
     | DOPN(_,cl)         -> array_exists (occur n) cl
     | DOP1(_,c)          -> occur n c
     | DOP2(_,c1,c2)      -> (occur n c1) or (occur n c2)
-    | DOPL(_,cl)         -> List.exists (occur n) cl
     | DLAM(_,c)          -> occur (n+1) c
     | DLAMV(_,v)         -> array_exists (occur (n+1)) v
+    | CLam (_,t,c)   -> occur n (body_of_type t) or occur (n+1) c
+    | CPrd (_,t,c)   -> occur n (body_of_type t) or occur (n+1) c
+    | CLet (_,b,t,c) -> occur n b or occur n (body_of_type t) or occur (n+1) c
     | Rel p              ->
     	p>n &
     	(try lookup_name_of_rel (p-n) env_names = Name id0
@@ -66,32 +68,25 @@ let next_name_not_occuring name l env_names t =
 
 (* Remark: Anonymous var may be dependent in Evar's contexts *)
 let concrete_name l env_names n c =
-  if n = Anonymous & not (dependent (Rel 1) c) then
+  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 (Rel 1) c then (Some fresh_id) else None in
+    let idopt = if dependent (mkRel 1) c then (Some fresh_id) else None in
     (idopt, fresh_id::l)
 
     (* Returns the list of global variables and constants in a term *)
 let global_vars_and_consts t =
-  let rec collect acc = function
-    | VAR id             -> id::acc
-    | DOPN (Const sp,cl) -> (basename sp)::(Array.fold_left collect acc cl)
-    | DOPN (Abst sp,cl)  -> (basename sp)::(Array.fold_left collect acc cl)
-    | DOPN (MutInd ind_sp, cl) as t       -> 
-	(basename (path_of_inductive_path ind_sp))
-	::(Array.fold_left collect acc cl)
-    | DOPN (MutConstruct cstr_sp, cl) as t -> 
-	(basename (path_of_constructor_path cstr_sp))
-	::(Array.fold_left collect acc cl)
-    | DOPN(_,cl)         -> Array.fold_left collect acc cl
-    | DOP1(_,c)          -> collect acc c
-    | DOP2(_,c1,c2)      -> collect (collect acc c1) c2
-    | DOPL(_,cl)         -> List.fold_left collect acc cl
-    | DLAM(_,c)          -> collect acc c
-    | DLAMV(_,v)         -> Array.fold_left collect acc v
-    | _                  -> acc
+  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'
+    | OpAbst 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)
     
@@ -156,7 +151,7 @@ module PrintingCasesMake =
     let check (_,lc) =
       if not (Test.test lc) then 
 	errorlabstrm "check_encode" [< 'sTR Test.error_message >]
-    let decode (spi,_) = sp_of_spi spi
+    let printer (spi,_) = [< 'sTR(string_of_path (sp_of_spi spi)) >]
     let key = Goptions.SecondaryTable ("Printing",Test.field)
     let title = Test.title
     let member_message = Test.member_message
@@ -194,8 +189,8 @@ module PrintingCasesLet =
           ^ " are not printed using a `let' form"
   end)
 
-module PrintingIf  = Goptions.MakeTable(PrintingCasesIf)
-module PrintingLet = Goptions.MakeTable(PrintingCasesLet)
+module PrintingIf  = Goptions.MakeIdentTable(PrintingCasesIf)
+module PrintingLet = Goptions.MakeIdentTable(PrintingCasesLet)
 
 let force_let (lc,(indsp,_,_,_,_)) = PrintingLet.active (indsp,lc)
 let force_if (lc,(indsp,_,_,_,_)) = PrintingIf.active (indsp,lc)
@@ -244,10 +239,10 @@ let computable p k =
        sinon on perd la réciprocité de la synthèse (qui, lui,
        engendrera un prédicat non dépendant) *)
 
-  let rec striprec = function
-    | (0,DOP2(Lambda,_,DLAM(_,d))) -> false
-    | (0,d               )         -> noccur_between 1 k d
-    | (n,DOP2(Lambda,_,DLAM(_,d))) -> striprec (n-1,d)
+  let rec striprec (n,c) = match n, kind_of_term c with
+    | (0,IsLambda (_,_,d)) -> false
+    | (0,_)                -> noccur_between 1 k c
+    | (n,IsLambda (_,_,d)) -> striprec (n-1,d)
     |  _                           -> false
   in 
   striprec (k,p)
@@ -262,24 +257,24 @@ let ids_of_var cl =
 *)
 
 let lookup_name_as_renamed ctxt t s =
-  let rec lookup avoid env_names n = function
-      DOP2(Prod,t,DLAM(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'))
-     | DOP2(Cast,c,_) -> lookup avoid env_names n c
-     | _ -> None
+  let rec lookup avoid env_names n c = match kind_of_term c with
+    | IsProd (name,t,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
+    | _ -> None
   in lookup (ids_of_var_context ctxt) empty_names_context 1 t
 
 let lookup_index_as_renamed t n =
-  let rec lookup n d = function
-      DOP2(Prod,_,DLAM(name,c')) -> 
+  let rec lookup n d c = match kind_of_term c with
+    | IsProd (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')
-    | DOP2(Cast,c,_) -> lookup n d c
+    | IsCast (c,_) -> lookup n d c
     | _ -> None
   in lookup n 1 t
 
@@ -310,6 +305,7 @@ let rec detype avoid env t =
 	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
     | IsAppL (f,args) ->
 	RApp (dummy_loc,detype avoid env f,List.map (detype avoid env) args)
     | IsConst (sp,cl) ->
@@ -356,7 +352,7 @@ let rec detype avoid env t =
 	end
 	
     | IsFix (nvn,(cl,lfn,vt)) -> detype_fix (RFix nvn) avoid env cl lfn vt
-    | IsCoFix (n,(cl,lfn,vt))  -> detype_fix (RCofix n) avoid env cl lfn vt)
+    | IsCoFix (n,(cl,lfn,vt))  -> detype_fix (RCoFix n) avoid env cl lfn vt)
 
 and detype_fix fk avoid env cl lfn vt =
   let lfi = List.map (fun id -> next_name_away id avoid) lfn in
@@ -369,34 +365,35 @@ and detype_fix fk avoid env cl lfn vt =
 
 and detype_eqn avoid env constr_id construct_nargs branch =
   let make_pat x avoid env b ids =
-    if not (force_wildcard ()) or (dependent (Rel 1) b) then
+    if not (force_wildcard ()) or (dependent (mkRel 1) b) then
       let id = next_name_away_with_default "x" x avoid in
       PatVar (dummy_loc,Name id),id::avoid,(add_name (Name id) env),id::ids
     else 
       PatVar (dummy_loc,Anonymous),avoid,(add_name Anonymous env),ids
   in
-  let rec buildrec ids patlist avoid env = function
-    | 0  , rhs	-> 
-	(ids, [PatCstr(dummy_loc, constr_id, List.rev patlist,Anonymous)],
-	 detype avoid env rhs)
-
-    | n, DOP2(Lambda,_,DLAM(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)
-
-    | n, DOP2(Cast,b,_) ->    (* Oui, il y a parfois des cast *)
-	buildrec ids patlist avoid env (n,b)
-	  
-    | n, b -> (* eta-expansion : n'arrivera plus lorsque tous les
-                   termes seront construits à partir de la syntaxe Cases *)
-	(* nommage de la nouvelle variable *)
-	let new_b = DOPN(AppL,[|lift 1 b; Rel 1|]) in
-        let pat,new_avoid,new_env,new_ids =
-	  make_pat Anonymous avoid env new_b ids in
-	buildrec new_ids (pat::patlist) new_avoid new_env (n-1,new_b)
+  let rec buildrec ids patlist avoid env n b =
+    if n=0 then
+      (ids, [PatCstr(dummy_loc, constr_id, List.rev patlist,Anonymous)],
+       detype avoid env b)
+    else
+      match kind_of_term b with
+	| IsLambda (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 *)
+	    buildrec ids patlist avoid env n c
+
+	| _ -> (* eta-expansion : n'arrivera plus lorsque tous les
+                  termes seront construits à partir de la syntaxe Cases *)
+            (* nommage de la nouvelle variable *)
+	    let new_b = applist (lift 1 b, [Rel 1]) in
+            let pat,new_avoid,new_env,new_ids =
+	      make_pat Anonymous avoid env new_b ids in
+	    buildrec new_ids (pat::patlist) new_avoid new_env (n-1) new_b
 	  
   in 
-  buildrec [] [] avoid env (construct_nargs,branch)
+  buildrec [] [] avoid env construct_nargs branch
 
 and detype_binder bk avoid env na ty c =
   let na',avoid' = match concrete_name avoid env na c with
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3afc73469..e4e2e48c5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -3,7 +3,7 @@
 
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Reduction
 open Instantiate
@@ -105,10 +105,10 @@ and evar_conv_x env isevars pbty term1 term2 =
     else 
       evar_eqappr_x env isevars pbty (t1,l1) (t2,l2)
 
-and evar_eqappr_x env isevars pbty appr1 appr2 =
+and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
   (* Evar must be undefined since we have whd_ised *)
-  match (appr1,appr2) with
-    | ((DOPN(Evar sp1,al1) as term1,l1), (DOPN(Evar sp2,al2) as term2,l2)) ->
+  match (kind_of_term term1, kind_of_term term2) with
+    | IsEvar (sp1,al1), IsEvar (sp2,al2) ->
 	let f1 () =
 	  if List.length l1 > List.length l2 then 
             let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
@@ -125,7 +125,7 @@ and evar_eqappr_x env isevars pbty appr1 appr2 =
 	in 
 	ise_try isevars [f1; f2]
 
-    | ((DOPN(Evar sp1,al1) as term1,l1), (DOPN(Const sp2,al2) as term2,l2)) ->
+    | IsEvar (sp1,al1), IsConst (sp2,al2) ->
 	let f1 () =
 	  (List.length l1 <= List.length l2) &
 	  let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
@@ -139,7 +139,7 @@ and evar_eqappr_x env isevars pbty appr1 appr2 =
 	in 
 	ise_try isevars [f1; f4]
 
-    | ((DOPN(Const sp1,al1) as term1,l1), (DOPN(Evar sp2,al2) as term2,l2)) ->
+    | IsConst (sp1,al1), IsEvar (sp2,al2) ->
 	let f1 () =
        	  (List.length l2 <= List.length l1) &
        	  let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
@@ -154,7 +154,7 @@ and evar_eqappr_x env isevars pbty appr1 appr2 =
 	in 
 	ise_try isevars [f1; f4]
 
-    | ((DOPN(Const sp1,al1) as term1,l1), (DOPN(Const sp2,al2) as term2,l2)) ->
+    | IsConst (sp1,al1), IsConst (sp2,al2) ->
 	let f2 () =
           (sp1 = sp2)
 	  & (array_for_all2 (evar_conv_x env isevars CONV) al1 al2)  
@@ -176,19 +176,19 @@ and evar_eqappr_x env isevars pbty appr1 appr2 =
 	in 
 	ise_try isevars [f2; f3; f4]
 
-    | ((DOPN(Evar _,_) as term1,l1),(t2,l2)) ->
+    | IsEvar (_,_), _ ->
        	(List.length l1 <= List.length l2) &
        	let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
-	solve_pb env isevars(pbty,term1,applist(t2,deb2))
+	solve_pb env isevars(pbty,term1,applist(term2,deb2))
         & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2
 
-    | ((t1,l1),(DOPN(Evar _,_) as t2,l2))  -> 
+    | _, IsEvar (_,_) ->
        	(List.length l2 <= List.length l1) &
        	let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
-	solve_pb env isevars(pbty,applist(t1,deb1),t2)
+	solve_pb env isevars(pbty,applist(term1,deb1),term2)
         & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2
 
-    | ((DOPN(Const _,_) as term1,l1),(t2,l2)) ->
+    | IsConst (_,_), _ ->
 	let f3 () =
 	  (try conv_record env isevars (check_conv_record appr1 appr2)
            with _ -> false)
@@ -199,18 +199,18 @@ and evar_eqappr_x env isevars pbty appr1 appr2 =
 	in 
 	ise_try isevars [f3; f4]
 	     
-    | ((t1,l1),(DOPN(Const _,_) as t2,l2))  -> 
+    | _ , IsConst (_,_) -> 
 	let f3 () = 
 	  (try (conv_record env isevars (check_conv_record appr2 appr1))
            with _ -> false)
 	and f4 () =
-          evaluable_constant env t2 &
+          evaluable_constant env term2 &
  	  evar_eqappr_x env isevars pbty
-            appr1 (evar_apprec env isevars l2 (constant_value env t2))
+            appr1 (evar_apprec env isevars l2 (constant_value env term2))
 	in 
 	ise_try isevars [f3; f4]
 
-    | ((DOPN(Abst _,_) as term1,l1),(DOPN(Abst _,_) as term2,l2)) ->
+    | IsAbst (_,_), IsAbst (_,_) ->
 	let f1 () =
           (term1=term2) &
  	  (List.length(l1) = List.length(l2)) &
@@ -226,75 +226,89 @@ and evar_eqappr_x env isevars pbty appr1 appr2 =
 	in 
 	ise_try isevars [f1; f2]
 
-    | ((DOPN(Abst _,_) as term1,l1),_) ->  
+    | IsAbst (_,_), _ ->  
         (evaluable_abst env term1)
 	& evar_eqappr_x env isevars pbty
           (evar_apprec env isevars l1 (abst_value env term1)) appr2
 	  
-    | (_,(DOPN(Abst _,_) as term2,l2))  -> 
+    | _, IsAbst (_,_)  -> 
         (evaluable_abst env term2)
 	& evar_eqappr_x env isevars pbty
  	  appr1 (evar_apprec env isevars l2 (abst_value env term2))
 
-    | ((Rel(n),l1),(Rel(m),l2)) ->
+    | IsRel n, IsRel m ->
 	n=m
 	  & (List.length(l1) = List.length(l2))
 	  & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2)
 
-    | ((DOP2(Cast,c,_),l),_) -> evar_eqappr_x env isevars pbty (c,l) appr2
+    | IsCast (c1,_), _ -> evar_eqappr_x env isevars pbty (c1,l1) appr2
 
-    | (_,(DOP2(Cast,c,_),l)) -> evar_eqappr_x env isevars pbty appr1 (c,l)
+    | _, IsCast (c2,_) -> evar_eqappr_x env isevars pbty appr1 (c2,l2)
 
-    | ((VAR id1,l1),(VAR id2,l2)) ->
+    | IsVar id1, IsVar id2 ->
 	(id1=id2 & (List.length l1 = List.length l2)
 	     & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2))
 
-    | ((DOP0(Meta(n)),l1),(DOP0(Meta(m)),l2)) ->
+    | IsMeta n, IsMeta m ->
 	(n=m & (List.length(l1) = List.length(l2))
 	   & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2))
 
-    | ((DOP0(Sort s1),[]),(DOP0(Sort s2),[])) -> base_sort_cmp pbty s1 s2
+    | IsSort s1, IsSort s2 when l1=[] & l2=[] -> base_sort_cmp pbty s1 s2
 
-    | ((DOP2(Lambda,c1,DLAM(_,c2)),[]), (DOP2(Lambda,c'1,DLAM(_,c'2)),[])) -> 
-	evar_conv_x env isevars CONV c1 c'1
-	& evar_conv_x env isevars CONV c2 c'2
+    | IsLambda (_,c1,c'1), IsLambda (_,c2,c'2) when l1=[] & l2=[] -> 
+	evar_conv_x env isevars CONV c1 c2
+	& evar_conv_x env isevars CONV c'1 c'2
 
-    | ((DOP2(Prod,c1,DLAM(n,c2)),[]), (DOP2(Prod,c'1,DLAM(_,c'2)),[])) -> 
-        evar_conv_x env isevars CONV c1 c'1 
+    | IsLetIn (_,b1,_,c'1), IsLetIn (_,b2,_,c'2) ->
+	let f1 () =
+	  evar_conv_x env isevars CONV b1 b2
+	  & evar_conv_x 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 () =
+	  evar_eqappr_x env isevars pbty (subst1 b1 c'1,l1) (subst1 b2 c'2,l2)
+	in 
+	ise_try isevars [f1; f2]
+
+    | IsLetIn (_,b1,_,c'1), _ ->  (* On fait commuter les args avec le Let *)
+	evar_eqappr_x env isevars pbty (subst1 b1 c'1,l1) appr2
+
+    | _, IsLetIn (_,b2,_,c'2) ->
+	evar_eqappr_x env isevars pbty appr1 (subst1 b2 c'2,l2)
+
+    | IsProd (n,c1,c'1), IsProd (_,c2,c'2) when l1=[] & l2=[] -> 
+        evar_conv_x env isevars CONV c1 c2
         & 
 	(let d = Retyping.get_assumption_of env !isevars (nf_ise1 !isevars c1)
-	 in evar_conv_x (push_rel_decl (n,d) env) isevars pbty c2 c'2)
+	 in evar_conv_x (push_rel_decl (n,d) env) isevars pbty c'1 c'2)
 
-    | ((DOPN(MutInd _ as o1,cl1) as ind1,l'1),
-       (DOPN(MutInd _ as o2,cl2) as ind2,l'2)) ->
-	o1=o2
-	   & array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2
-           & list_for_all2eq (evar_conv_x env isevars CONV) l'1 l'2
+    | IsMutInd (sp1,cl1), IsMutInd (sp2,cl2) ->
+	sp1=sp2
+	& array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2
+        & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2
              
-    | ((DOPN(MutConstruct _ as o1,cl1) as constr1,l1),
-       (DOPN(MutConstruct _ as o2,cl2) as constr2,l2)) ->
-	o1=o2
-           & array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2
-           & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2
-
-    | ((DOPN(MutCase _,_) as constr1,l'1),
-       (DOPN(MutCase _,_) as constr2,l'2)) ->
-	let (_,p1,c1,cl1) = destCase constr1 in
-	let (_,p2,c2,cl2) = destCase constr2 in
+    | IsMutConstruct (sp1,cl1), IsMutConstruct (sp2,cl2) ->
+	sp1=sp2
+        & array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2
+        & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2
+
+    | IsMutCase (_,p1,c1,cl1), IsMutCase (_,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) l'1 l'2)
+	& (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
 
-    | ((DOPN(Fix _ as o1,cl1),l1),(DOPN(Fix _ as o2,cl2),l2))   ->
-	o1=o2 & 
-	   (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)), IsFix (li2,(tys2,_,bds2)) ->
+	li1=li2
+	& (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2)
+	& (array_for_all2 (evar_conv_x env isevars CONV) bds1 bds2)
+	& (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
 	     
-    | ((DOPN(CoFix(i1),cl1),l1),(DOPN(CoFix(i2),cl2),l2))   ->
-	i1=i2 & 
-	   (array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2) &
-	   (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
+    | IsCoFix (i1,(tys1,_,bds1)), IsCoFix (i2,(tys2,_,bds2)) ->
+	i1=i2 
+	& (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2)
+	& (array_for_all2 (evar_conv_x env isevars CONV) bds1 bds2)
+	& (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
 
     (***
     | (DOP0(Implicit),[]),(DOP0(Implicit),[]) -> true
@@ -302,13 +316,16 @@ and evar_eqappr_x env isevars pbty appr1 appr2 =
      * But b (optional env) is not updated! *)
     ***)
 
-    | (DLAM(_,c1),[]),(DLAM(_,c2),[]) -> 
-	evar_conv_x env isevars pbty c1 c2
+    | (IsRel _ | IsVar _ | IsMeta _ | IsXtra _ | IsLambda _), _ -> false
+    | _, (IsRel _ | IsVar _ | IsMeta _ | IsXtra _ | IsLambda _) -> false
+
+    | (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _), _ -> false
+    | _, (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _) -> false
+
+    | (IsAppL _ | IsMutCase _ | IsFix _ | IsCoFix _), 
+      (IsAppL _ | IsMutCase _ | IsFix _ | IsCoFix _) -> false
 
-    | (DLAMV(_,vc1),[]),(DLAMV(_,vc2),[]) ->
-	array_for_all2 (evar_conv_x env isevars pbty) vc1 vc2
 
-    | _ -> false
 
 and conv_record env isevars (c,bs,(xs,xs1),(us,us1),(ts,ts1),t) = 
   let ks =
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 804d635db..2d35fb753 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -5,7 +5,7 @@ open Util
 open Pp
 open Names
 open Univ
-open Generic
+(*i open Generic i*)
 open Term
 open Sign
 open Environ
@@ -57,11 +57,15 @@ let new_isevar_sign env sigma typ instance =
    any type has type Type. May cause some trouble, but not so far... *)
 let dummy_sort = mkType dummy_univ
 
+let make_instance env =
+  fold_var_context
+    (fun env (id, b, _) l -> if b=None then mkVar id :: l else l)
+    env []
+
 (* Declaring any type to be in the sort Type shouldn't be harmful since
    cumulativity now includes Prop and Set in Type. *)
 let new_type_var env sigma =
-  let sign = var_context env in
-  let instance = List.map mkVar (ids_of_var_context sign) in
+  let instance = make_instance env in
   let (sigma',c) = new_isevar_sign env sigma dummy_sort instance in
   (sigma', c)
 
@@ -74,7 +78,7 @@ let split_evar_to_arrow sigma c =
   let nvar = next_ident_away (id_of_string "x") (ids_of_var_context hyps) in
   let newenv = push_var_decl (nvar,make_typed dom (Type dummy_univ)) 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 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
@@ -109,7 +113,7 @@ let do_restrict_hyps sigma c =
   in
   let sign' = List.rev rsign in
   let env' = change_hyps (fun _ -> sign') env in
-  let instance = List.map mkVar (ids_of_var_context sign') in
+  let instance = make_instance env' in
   let (sigma',nc) = new_isevar_sign env' sigma evd.evar_concl instance in
   let sigma'' = Evd.define sigma' ev nc in
   (sigma'', nc)
@@ -188,14 +192,34 @@ let real_clean isevars sp args rhs =
     | DOP1(o,a) -> DOP1(o, subs k a)
     | DOP2(o,a,b) -> DOP2(o, subs k a, subs k b)
     | DOPN(o,v) -> restrict_hyps isevars (DOPN(o, Array.map (subs k) v))
-    | DOPL(o,l) -> DOPL(o, List.map (subs k) l)
     | DLAM(n,a) -> DLAM(n, subs (k+1) a)
-    | DLAMV(n,v) -> DLAMV(n, Array.map (subs (k+1)) v) in
+    | DLAMV(n,v) -> DLAMV(n, Array.map (subs (k+1)) v)
+    | CLam (n,t,c)   -> CLam (n, typed_app (subs k) t, subs (k+1) c)  
+    | CPrd (n,t,c)   -> CPrd (n, typed_app (subs k) t, subs (k+1) c)
+    | CLet (n,b,t,c) -> CLet (n, subs k b, typed_app (subs k) t, subs (k+1) c)
+  in
   let body = subs 0 rhs in
   (* if not (closed0 body) then error_not_clean CCI empty_env sp body; *)
   body
 
-
+let make_instance_with_rel env =
+  let n = rel_context_length (rel_context env) in
+  let vars = 
+    fold_var_context
+      (fun env (id,b,_) l -> if b=None then mkVar id :: l else l)
+      env [] in
+  snd (fold_rel_context
+    (fun env (_,b,_) (i,l) -> (i-1, if b=None then mkRel i :: l else l))
+    env (n+1,vars))
+
+let make_subst env args =
+  snd (fold_var_context
+    (fun env (id,b,c) (args,l as g) ->
+       match b, args with
+	 | None, a::rest -> (rest, (id,a)::l)
+	 | Some _, _ -> g
+	 | _ -> anomaly "Instance does not match its signature")
+    env (List.rev 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 *)
@@ -203,9 +227,7 @@ let real_clean isevars sp args rhs =
 let new_isevar isevars env typ k =
   let subst,env' = push_rels_to_vars env in
   let typ' = substl subst typ in
-  let instance =
-    (List.rev (rel_list 0 (rel_context_length (rel_context env))))
-    @(List.map mkVar (ids_of_var_context (var_context env))) in
+  let instance = make_instance_with_rel env in
   let (sigma',evar) = new_isevar_sign env' !isevars typ' instance in
   isevars := sigma';
   evar
@@ -233,9 +255,8 @@ let evar_define isevars lhs rhs =
   let args = List.map (function (VAR _ | Rel _) as t -> t | _ -> mkImplicit)
       (Array.to_list argsv) in 
   let evd = ise_map isevars ev in
-  let hyps = var_context evd.evar_env in
   (* the substitution to invert *)
-  let worklist = List.combine (ids_of_var_context hyps) args in
+  let worklist = make_subst evd.evar_env args in
   let body = real_clean isevars ev worklist rhs in
   ise_define isevars ev body;
   [ev]
@@ -306,30 +327,21 @@ let rec solve_simple_eqn conv_algo isevars ((pbty,t1,t2) as pb) =
 
 
 let has_undefined_isevars isevars c =
-  let rec hasrec = function
-    | DOPN(Evar ev,cl) as k ->
-	if ise_in_dom isevars ev then 
-	  if ise_defined isevars k then 
-	    hasrec (existential_value !isevars (ev,cl))
-	  else 
-	    failwith "caught"
-	else 
-	  Array.iter hasrec cl
-    | DOP1(_,c) -> hasrec c
-    | DOP2(_,c1,c2) -> (hasrec c1; hasrec c2)
-    | DOPL(_,l) -> List.iter hasrec l
-    | DOPN(_,cl) -> Array.iter hasrec cl
-    | DLAM(_,c) -> hasrec c
-    | DLAMV(_,cl) -> Array.iter hasrec cl
-    | (VAR _|Rel _|DOP0 _) -> ()
+  let rec hasrec k = match splay_constr k with
+    | OpEvar ev, cl when ise_in_dom isevars ev ->
+	if ise_defined isevars k then 
+	  hasrec (existential_value !isevars (ev,cl))
+	else
+	  failwith "caught"
+    | _, cl -> Array.iter hasrec cl
   in 
   (try (hasrec c ; false) with Failure "caught" -> true)
 
 let head_is_exist isevars = 
-  let rec hrec = function
-    | DOPN(Evar _,_) as k -> ise_undefined isevars k
-    | DOPN(AppL,cl) -> hrec (array_hd cl)
-    | DOP2(Cast,c,_) -> hrec c
+  let rec hrec k = match kind_of_term k with
+    | IsEvar _     -> ise_undefined isevars k
+    | IsAppL (f,l) -> hrec f
+    | IsCast (c,_) -> hrec c
     | _ -> false
   in 
   hrec 
@@ -399,15 +411,17 @@ let mk_valcon c = Some c
 let split_tycon loc env isevars = function
   | None -> None,None
   | Some c ->
-      (match whd_betadeltaiota env !isevars c with
-         | DOP2(Prod,dom,DLAM(na,rng)) ->
-	    Some dom, Some rng
-	| t when ise_undefined isevars t ->
-	    let (sigma,dom,rng) = split_evar_to_arrow !isevars t in
-	    isevars := sigma;
-	    Some dom, Some rng
+      let t = whd_betadeltaiota env !isevars c in
+      match kind_of_term t with
+        | IsProd (na,dom,rng) -> Some dom, Some rng
 	| _ ->
-	    Stdpp.raise_with_loc loc (Type_errors.TypeError (CCI,env,Type_errors.NotProduct c)))
+	    if ise_undefined isevars t then
+	      let (sigma,dom,rng) = split_evar_to_arrow !isevars t in
+	      isevars := sigma;
+	      Some dom, Some rng
+	    else
+	      Stdpp.raise_with_loc loc
+		(Type_errors.TypeError (CCI,env,Type_errors.NotProduct c))
 
 let valcon_of_tycon x = x
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c2770f196..09dd23065 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Sign
 open Evd
 open Term
@@ -27,34 +27,37 @@ open Coercion
 open Inductive
 open Instantiate
 
+(*
 (* Pour le vieux "match" que Program utilise encore, vieille histoire ... *)
 
 (* Awful special reduction function which skips abstraction on Xtra in
    order to be safe for Program ... *)
 
 let stacklamxtra recfun = 
-  let rec lamrec sigma p_0 p_1 = match p_0,p_1 with 
-    | (stack, (DOP2(Lambda,DOP1(XTRA "COMMENT",_),DLAM(_,c)) as t)) ->
+  let rec lamrec sigma s t = match s,kind_of_term t with 
+    | (stack, IsLambda (_,DOP1(XTRA "COMMENT",_),_)) ->
         recfun stack (substl sigma t)
-    | ((h::t), (DOP2(Lambda,_,DLAM(_,c)))) -> lamrec (h::sigma) t c
-    | (stack, t) -> recfun stack (substl sigma t)
+    | ((h::t), IsLambda (_,_,c)) -> lamrec (h::sigma) t c
+    | (stack, _) -> recfun stack (substl sigma t)
   in 
   lamrec 
 
 let rec whrec x stack =
-  match x with   
-    | DOP2(Lambda,DOP1(XTRA "COMMENT",c),DLAM(name,t)) ->
+  match kind_of_term x with   
+    | IsLambda (name, DOP1(XTRA "COMMENT",c),t) ->
     	let t' = applist (whrec t (List.map (lift 1) stack)) in 
-	DOP2(Lambda,DOP1(XTRA "COMMENT",c),DLAM(name,t')),[]
-    | DOP2(Lambda,c1,DLAM(name,c2)) ->
+	mkLambda (name,DOP1(XTRA "COMMENT",c),t'),[]
+    | IsLambda (name,c1,c2) ->
     	(match stack with
-	   | [] -> (DOP2(Lambda,c1,DLAM(name,whd_betaxtra c2)),[])
+	   | [] -> mkLambda (name,c1,whd_betaxtra c2),[]
 	   | a1::rest -> stacklamxtra (fun l x -> whrec x l) [a1] rest c2)
-    | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl stack)
-    | DOP2(Cast,c,_) ->  whrec c stack
-    | x -> x,stack
+    | IsAppL (f,args) -> whrec f (args@stack)
+    | IsCast (c,_) ->  whrec c stack
+    | _ -> x,stack
 
 and whd_betaxtra x = applist(whrec x [])
+*)
+let whd_betaxtra = whd_beta
 
 let lift_context n l = 
   let k = List.length l in 
@@ -111,10 +114,8 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) =
 		 applist (whd_beta_stack (lift (nar+1) p) (rel_list 1 nar)))))
           lnames 
       in
-      let fix = DOPN(Fix([|nar|],0),
-		     [|typPfix;
-		       DLAMV(Name(id_of_string "F"),[|deffix|])|])
-      in 
+      let fix = mkFix (([|nar|],0),
+		       ([|typPfix|],[Name(id_of_string "F")],[|deffix|])) in
       applist (fix,realargs@[c])
   else
     let ci = make_default_case_info mispec in
@@ -217,31 +218,9 @@ let pretype_ref pretype loc isevars env lvar = function
     make_judge (mkConst cst) (type_of_constant env !isevars cst)
 
 | RAbst sp -> failwith "Pretype: abst doit disparaître"
-(*
-  if sp = let_path then
-      (match Array.to_list cl with
-       [m;DLAM(na,b)] ->
-       let mj = pretype empty_tycon isevars env m in
-	 (try 
-	    let mj = inh_ass_of_j isevars env mj in
-	    let mb = body_of_type mj in
-	    let bj =
-	     pretype empty_tycon (push_rel (na,mj) env) isevars b in
-	   {uj_val = DOPN(Abst sp,[|mb;DLAM(na,bj.uj_val)|]);
-            uj_type = sAPP (DLAM(na,bj.uj_type)) mb;
-            uj_kind = pop bj.uj_kind }
-	 with UserError _ -> 
-	   pretype vtcon isevars env (abst_value cstr)) 
-      | _ -> errorlabstrm "Trad.constr_of_com" [< 'sTR"Malformed ``let''" >])
-   else if evaluable_abst cstr then
-     pretype vtcon isevars env (abst_value cstr)
-   else error "Cannot typecheck an unevaluable abstraction"
-*)
+
 | REVar (sp,ctxt) -> error " Not able to type terms with dependent subgoals"
-(* Not able to type goal existential yet
-    let cstr = mkConst (sp,ctxt_of_ids ids) in
-    make_judge cstr (type_of_existential env !isevars cstr)
-*)
+
 | RInd (ind_sp,ctxt) ->
     let ind = (ind_sp,Array.map pretype ctxt) in
     make_judge (mkMutInd ind) (type_of_inductive env !isevars ind)
@@ -285,16 +264,6 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 
 | RHole loc ->
   if !compter then nbimpl:=!nbimpl+1;
-(* OLD
-  (match vtcon with
-    (true,(Some v, _)) ->
-      {uj_val=v.utj_val; uj_type=make_typed (mkSort v.utj_type) (Type Univ.dummy_univ)}
-  | (false,(None,Some ty)) ->
-      let c = new_isevar isevars env ty CCI in
-      {uj_val=c;uj_type=make_typed ty (Type Univ.dummy_univ)}
-  | (true,(None,None)) ->
-      let ty = mkCast dummy_sort dummy_sort in
-*)
   (match tycon with
   | Some ty ->
       let c = new_isevar isevars env ty CCI in
@@ -328,7 +297,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 	 let fix = (vni,(larav,List.rev lfi,Array.map j_val_only vdefj)) in
 	 check_fix env !isevars fix;
 	 make_judge (mkFix fix) lara.(i)
-     | RCofix i -> 
+     | RCoFix i -> 
 	 let cofix = (i,(larav,List.rev lfi,Array.map j_val_only vdefj)) in
 	 check_cofix env !isevars cofix;
 	 make_judge (mkCoFix cofix) lara.(i))
@@ -365,6 +334,13 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
     (try fst (gen_rel env !isevars name assum j')
      with TypeError _ as e -> Stdpp.raise_with_loc loc e)
 
+| RBinder(loc,BLetIn,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 j' = pretype tycon (push_rel_def var env) isevars lvar lmeta c2 in
+    { uj_val = mkLetIn (name, j.uj_val, body_of_type j.uj_type, j'.uj_val) ;
+      uj_type = typed_app (subst1 j.uj_val) j'.uj_type }
+
 | ROldCase (loc,isrec,po,c,lf) ->
   let cj = pretype empty_tycon env isevars lvar lmeta c in
   let (IndType (indf,realargs) as indt) = 
@@ -427,7 +403,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 	let ci = make_default_case_info mis in
 	mkMutCaseA ci pj.uj_val cj.uj_val (Array.map (fun j-> j.uj_val) lfj)
     in
-    let s = destSort (snd (splay_prod env !isevars evalPt)) in
+    let s = snd (splay_arity env !isevars evalPt) in
     {uj_val = v;
      uj_type = make_typed rsty s }
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index fe7830620..10c7cee07 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -11,7 +11,7 @@ open Library
 open Classops
 (*
 open Pp_control
-open Generic
+(*i open Generic i*)
 open Initial
 *)
 
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 5872bd922..0f90afeb5 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -4,7 +4,7 @@
 (*i*)
 open Names
 open Term
-open Generic
+(*i open Generic i*)
 open Classops
 open Libobject
 open Library
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 72a3d3d51..aa499fb63 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -5,7 +5,7 @@ open Util
 open Term
 open Inductive
 open Names
-open Generic
+(*i open Generic i*)
 open Reduction
 open Environ
 open Typeops
@@ -13,15 +13,15 @@ open Typeops
 type metamap = (int * constr) list
 
 let outsort env sigma t =
-  match whd_betadeltaiota env sigma t with
-      DOP0(Sort s) -> s
+  match kind_of_term (whd_betadeltaiota env sigma t) with
+    | IsSort s -> s
     | _ -> anomaly "Retyping: found a type of type which is not a sort"
 
 let rec subst_type env sigma typ = function
-    [] -> typ
+  | [] -> typ
   | h::rest ->
-      match whd_betadeltaiota env sigma typ with
-          DOP2(Prod,c1,DLAM(_,c2)) -> subst_type env sigma (subst1 h c2) rest
+      match kind_of_term (whd_betadeltaiota env sigma typ) with
+          IsProd (_,c1,c2) -> subst_type env sigma (subst1 h c2) rest
         | _ -> anomaly "Non-functional construction"
 
 (* Si ft est le type d'un terme f, lequel est appliqué à args, *)
@@ -31,16 +31,16 @@ let rec subst_type env sigma typ = function
 
 let sort_of_atomic_type env sigma ft args =
   let rec concl_of_arity ar =
-    match whd_betadeltaiota env sigma ar with
-      | DOP2 (Prod, _, DLAM (_, b)) -> concl_of_arity b
-      | DOP0 (Sort s) -> s
+    match kind_of_term (whd_betadeltaiota env sigma ar) with
+      | IsProd (_, _, b) -> concl_of_arity b
+      | IsSort s -> s
       | _ -> outsort env sigma (subst_type env sigma ft args)
   in concl_of_arity ft
 
 let typeur sigma metamap =
 let rec type_of env cstr=
   match kind_of_term cstr with
-      IsMeta n ->
+    | IsMeta 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)))
@@ -65,14 +65,17 @@ let rec type_of env cstr=
         whd_betadeltaiota env sigma (applist (p,al))
     | IsLambda (name,c1,c2) ->
         let var = make_typed c1 (sort_of env c1) in
-          mkProd name c1 (type_of (push_rel_decl (name,var) env) c2)
+          mkProd (name, c1, type_of (push_rel_decl (name,var) env) c2)
+    | IsLetIn (name,b,c1,c2) ->
+        let var = make_typed c1 (sort_of env c1) in
+         subst1 b (type_of (push_rel_def (name,b,var) env) c2)
     | IsFix ((vn,i),(lar,lfi,vdef)) -> lar.(i)
     | IsCoFix (i,(lar,lfi,vdef)) -> lar.(i)
     | IsAppL(f,args)->
       strip_outer_cast (subst_type env sigma (type_of env f) args)
     | IsCast (c,t) -> t
     | IsSort _ | IsProd (_,_,_) | IsMutInd _ -> mkSort (sort_of env cstr)
-    | _ -> error "type_of: Unexpected constr"
+    | IsXtra _ -> error "type_of: Unexpected constr"
 
 and sort_of env t = 
   match kind_of_term t with
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index a0fe84ee6..16eebbefb 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Inductive
 open Environ
@@ -48,8 +48,10 @@ let make_elim_fun f lv n largs =
     let fi = DOPN(Const(make_path (dirpath sp) id (kind_of_path sp)),args) in
     list_fold_left_i 
       (fun i c (k,a) -> 
-	 DOP2(Lambda,(substl (rev_firstn_liftn (n-k) (-i) la') a),
-              DLAM(Name(id_of_string"x"),c))) 0 (applistc fi la') lv
+	 mkLambda (Name(id_of_string"x"),
+		   substl (rev_firstn_liftn (n-k) (-i) la') a,
+		   c))
+      0 (applistc fi la') lv
 
 (* [f] is convertible to [DOPN(Fix(recindices,bodynum),bodyvect)] make 
    the reduction using this extra information *)
@@ -145,120 +147,124 @@ let rec red_elim_const env sigma k largs =
     | _ -> raise Redelimination
 
 and construct_const env sigma c stack = 
-  let rec hnfstack x stack =
-    match x with
-      | (DOPN(Const _,_)) as k  ->
+  let rec hnfstack (x, stack as s) =
+    match kind_of_term x with
+      | IsConst _  ->
           (try
-             let (c',lrest) = red_elim_const env sigma k stack in 
-	     hnfstack c' lrest
+	     hnfstack (red_elim_const env sigma x stack)
            with Redelimination ->
-             if evaluable_constant env k then 
-	       let cval = constant_value env k in
+             if evaluable_constant env x then 
+	       let cval = constant_value env x in
 	       (match cval with
-                  | DOPN (CoFix _,_) -> (k,stack)
-                  | _ -> hnfstack cval stack) 
+                  | DOPN (CoFix _,_) -> s
+                  | _ -> hnfstack (cval, stack))
              else 
 	       raise Redelimination)
+(*
       | (DOPN(Abst _,_) as a) ->
           if evaluable_abst env a then 
 	    hnfstack (abst_value env a) stack
           else 
 	    raise Redelimination
-      | DOP2(Cast,c,_) -> hnfstack c stack
-      | DOPN(AppL,cl) -> hnfstack (array_hd cl) (array_app_tl cl stack)
-      | DOP2(Lambda,_,DLAM(_,c)) ->
+*)
+      | IsCast (c,_) -> hnfstack (c, stack)
+      | IsAppL (f,cl) -> hnfstack (f, cl@stack)
+      | IsLambda (_,_,c) ->
           (match stack with 
              | [] -> assert false
              | c'::rest -> stacklam hnfstack [c'] c rest)
-      | DOPN(MutCase _,_) as c_0 ->
-          let (ci,p,c,lf) = destCase c_0 in
+      | IsMutCase (ci,p,c,lf) ->
           hnfstack 
-	    (special_red_case env (construct_const env sigma) p c ci lf) 
-	    stack
-      | DOPN(MutConstruct _,_) as c_0 -> c_0,stack
-      | DOPN(CoFix _,_) as c_0 -> c_0,stack
-      | DOPN(Fix (_) ,_) as fix -> 
-          let (reduced,(fix,stack')) = reduce_fix hnfstack fix stack in 
-	  if reduced then hnfstack fix stack' else raise Redelimination
+	    (special_red_case env (construct_const env sigma) p c ci lf, stack)
+      | IsMutConstruct _ -> s
+      | IsCoFix _ -> s
+      | IsFix fix -> 
+	  (match reduce_fix hnfstack fix stack with
+             | Reduced s' -> hnfstack s'
+	     | NotReducible -> raise Redelimination)
       | _ -> raise Redelimination
   in 
-  hnfstack c stack
+  hnfstack (c, stack)
 
 (* Hnf reduction tactic: *)
 
 let hnf_constr env sigma c = 
-  let rec redrec x largs =
-    match x with
-      | DOP2(Lambda,t,DLAM(n,c)) ->
+  let rec redrec (x, largs as s) =
+    match kind_of_term x with
+      | IsLambda (n,t,c) ->
           (match largs with
-             | []      -> applist(x,largs)
+             | []      -> applist s
              | a::rest -> stacklam redrec [a] c rest)
-      | DOPN(AppL,cl)   -> redrec (array_hd cl) (array_app_tl cl largs)
-      | DOPN(Const _,_) ->
+      | IsAppL (f,cl)   -> redrec (f, cl@largs)
+      | IsConst _ ->
           (try
              let (c',lrest) = red_elim_const env sigma x largs in 
-	     redrec c' lrest
+	     redrec (c', lrest)
            with Redelimination ->
              if evaluable_constant env x then
                let c = constant_value env x in
 	       (match c with 
                   | DOPN(CoFix _,_) -> applist(x,largs)
-		  | _ ->  redrec c largs)
+		  | _ ->  redrec (c, largs))
              else 
-	       applist(x,largs))
+	       applist s)
+(*
       | DOPN(Abst _,_) ->
           if evaluable_abst env x then 
 	    redrec (abst_value env x) largs
           else 
-	    applist(x,largs)
-      | DOP2(Cast,c,_) -> redrec c largs
-      | DOPN(MutCase _,_) ->
-          let (ci,p,c,lf) = destCase x in
+	    applist s
+*)
+      | IsCast (c,_) -> redrec (c, largs)
+      | IsMutCase (ci,p,c,lf) ->
           (try
              redrec 
 	       (special_red_case env (whd_betadeltaiota_stack env sigma) 
-		  p c ci lf) largs
+		  p c ci lf, largs)
            with Redelimination -> 
-	     applist(x,largs))
-      | (DOPN(Fix _,_)) ->
-          let (reduced,(fix,stack)) = 
-            reduce_fix (whd_betadeltaiota_stack env sigma) x largs
-          in 
-	  if reduced then redrec fix stack else applist(x,largs)
-      | _ -> applist(x,largs)
+	     applist s)
+      | IsFix fix ->
+	  (match reduce_fix
+	     (fun (c,l) -> whd_betadeltaiota_stack env sigma c l)
+	     fix largs
+	   with
+             | Reduced s' -> redrec s'
+	     | NotReducible -> applist s)
+      | _ -> applist s
   in 
-  redrec c []
+  redrec (c, [])
 
 (* Simpl reduction tactic: same as simplify, but also reduces
    elimination constants *)
 
 let whd_nf env sigma c = 
-  let rec nf_app c stack =
-    match c with
-      | DOP2(Lambda,c1,DLAM(name,c2))    ->
+  let rec nf_app (c, stack as s) =
+    match kind_of_term c with
+      | IsLambda (name,c1,c2)    ->
           (match stack with
              | [] -> (c,[])
              | a1::rest -> stacklam nf_app [a1] c2 rest)
-      | DOPN(AppL,cl) -> nf_app (array_hd cl) (array_app_tl cl stack)
-      | DOP2(Cast,c,_) -> nf_app c stack
-      | DOPN(Const _,_) ->
+      | IsAppL (f,cl) -> nf_app (f, cl@stack)
+      | IsCast (c,_) -> nf_app (c, stack)
+      | IsConst _ ->
           (try
-             let (c',lrest) = red_elim_const env sigma c stack in 
-	     nf_app c' lrest
+	     nf_app (red_elim_const env sigma c stack)
            with Redelimination -> 
-	     (c,stack))
-      | DOPN(MutCase _,_) ->
-          let (ci,p,d,lf) = destCase c in
+	     s)
+      | IsMutCase (ci,p,d,lf) ->
           (try
-             nf_app (special_red_case env nf_app p d ci lf) stack
+             nf_app
+	       (special_red_case env (fun c l -> nf_app (c,l)) p d ci lf,
+		stack)
            with Redelimination -> 
-	     (c,stack))
-      | DOPN(Fix _,_) ->
-          let (reduced,(fix,rest)) = reduce_fix nf_app c stack in 
-	  if reduced then nf_app fix rest else (fix,stack)
-      | _ -> (c,stack)
+	     s)
+      | IsFix fix ->
+	  (match reduce_fix nf_app fix stack with
+             | Reduced s' -> nf_app s'
+	     | NotReducible -> s)
+      | _ -> s
   in 
-  applist (nf_app c [])
+  applist (nf_app (c, []))
 
 let nf env sigma c = strong whd_nf env sigma c
 
@@ -286,65 +292,66 @@ let reduction_of_redexp = function
 
 (* Used in several tactics. *)
 
-let one_step_reduce env sigma = 
-  let rec redrec largs x =
-    match x with
-      | DOP2(Lambda,t,DLAM(n,c))  ->
+let one_step_reduce env sigma c = 
+  let rec redrec (x, largs as s) =
+    match kind_of_term x with
+      | IsLambda (n,t,c)  ->
           (match largs with
              | []      -> error "Not reducible 1"
              | a::rest -> applistc (subst1 a c) rest)
-      | DOPN(AppL,cl) -> redrec (array_app_tl cl largs) (array_hd cl)
-      | DOPN(Const _,_) ->
+      | IsAppL (f,cl) -> redrec (f, cl@largs)
+      | IsConst _ ->
           (try
              let (c',l) = red_elim_const env sigma x largs in applistc c' l
            with Redelimination ->
              if evaluable_constant env x then
                applistc (constant_value env x) largs
              else error "Not reductible 1")
+(*
       | DOPN(Abst _,_) ->
           if evaluable_abst env x then applistc (abst_value env x) largs
           else error "Not reducible 0"
-      | DOPN(MutCase _,_) ->
-          let (ci,p,c,lf) = destCase x in
+*)
+      | IsMutCase (ci,p,c,lf) ->
           (try
 	     applistc 
 	       (special_red_case env (whd_betadeltaiota_stack env sigma) 
 		  p c ci lf) largs 
            with Redelimination -> error "Not reducible 2")
-      | DOPN(Fix _,_) ->
-          let (reduced,(fix,stack)) = 
-	    reduce_fix (whd_betadeltaiota_stack env sigma) x largs
-          in 
-	  if reduced then applistc fix stack else error "Not reducible 3"
-      | DOP2(Cast,c,_) -> redrec largs c
+      | IsFix fix ->
+	  (match reduce_fix
+	     (fun (x,l) -> whd_betadeltaiota_stack env sigma x l)
+	     fix largs
+	   with
+             | Reduced s' -> applist s'
+	     | NotReducible -> error "Not reducible 3")
+      | IsCast (c,_) -> redrec (c,largs)
       | _ -> error "Not reducible 3"
   in 
-  redrec []
+  redrec (c, [])
 
 (* put t as t'=(x1:A1)..(xn:An)B with B an inductive definition of name name
    return name, B and t' *)
 
 let reduce_to_mind env sigma t = 
   let rec elimrec t l = 
-    match whd_castapp_stack t [] with
-      | (DOPN(MutInd mind,args),_) -> ((mind,args),t,prod_it t l)
-      | (DOPN(Const _,_),_) -> 
-          (try 
-	     let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in 
-	     elimrec t' l
-           with UserError _ -> errorlabstrm "tactics__reduce_to_mind"
-               [< 'sTR"Not an inductive product : it is a constant." >])
-      | (DOPN(MutCase _,_),_) ->
+    let c, _ = whd_castapp_stack t [] in
+    match kind_of_term c with
+      | IsMutInd (mind,args) -> ((mind,args),t,it_mkProd_or_LetIn t l)
+      | IsConst _ | IsMutCase _ ->
           (try 
 	     let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in 
 	     elimrec t' l
            with UserError _ -> errorlabstrm "tactics__reduce_to_mind"
-               [< 'sTR"Not an inductive product:"; 'sPC;
-		  'sTR"it is a case analysis term" >])
-      | (DOP2(Cast,c,_),[]) -> elimrec c l
-      | (DOP2(Prod,ty,DLAM(n,t')),[]) -> elimrec t' ((n,ty)::l)
+               [< 'sTR"Not an inductive product." >])
+      | IsProd (n,ty,t') ->
+	let ty' = Retyping.get_assumption_of (Global.env()) Evd.empty ty in
+	elimrec t' ((n,None,ty')::l)
+      | IsLetIn (n,b,ty,t') ->
+	  let ty' = Retyping.get_assumption_of (Global.env()) Evd.empty ty in
+	  elimrec t' ((n,Some b,ty')::l)
       | _ -> error "Not an inductive product"
- in 
+ in
  elimrec t []
 
 let reduce_to_ind env sigma t =
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 0dc0d0a5b..5dfcfdce3 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -3,7 +3,7 @@
 
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Environ
 open Reduction
@@ -105,7 +105,15 @@ let rec execute mf env sigma cstr =
         let j' = execute mf env1 sigma c2 in
 	let (j,_) = gen_rel env1 sigma name varj j' in
 	j
-	  
+
+     | IsLetIn (name,c1,c2,c3) ->
+        let j1 = execute mf env sigma c1 in
+        let j2 = execute mf env sigma c2 in
+	let { uj_val = b; uj_type = t } = cast_rel env sigma j1 j2 in
+        let j3 = execute mf (push_rel_def (name,b,t) env) sigma c3 in
+	{ uj_val = mkLetIn (name, j1.uj_val, j2.uj_val, j3.uj_val) ;
+	  uj_type = typed_app (subst1 j1.uj_val) j3.uj_type }
+  
     | IsCast (c,t) ->
         let cj = execute mf env sigma c in
         let tj = execute mf env sigma t in