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@590 85f007b7-540e-0410-9357-904b9bb8a0f7

18 files changed, 291 insertions, 303 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 9b0d24632..e5dfff04c 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Sign
 open Inductive
@@ -177,9 +177,8 @@ let (inAutoHint,outAutoHint) =
 (*                     The "Hint" vernacular command                      *)
 (**************************************************************************)
 
-let rec nb_hyp = function
-  | DOP2(Prod,_,DLAM(_,c2)) -> 
-      if dependent (Rel 1) c2 then nb_hyp c2 else 1+(nb_hyp c2)
+let rec nb_hyp c = match kind_of_term c with
+  | IsProd(_,_,c2) -> if dependent (mkRel 1) c2 then nb_hyp c2 else 1+(nb_hyp c2)
   | _ -> 0 
 
 (* adding and removing tactics in the search table *)
@@ -189,16 +188,18 @@ let try_head_pattern c =
   with BoundPattern -> error "Bound head variable"
 
 let make_exact_entry name (c,cty) =
-  match strip_outer_cast cty with
-    | DOP2(Prod,_,_) -> 
+  let cty = strip_outer_cast cty in
+  match kind_of_term cty with
+    | IsProd (_,_,_) -> 
 	failwith "make_exact_entry"
-    | cty ->
+    | _ ->
 	(head_of_constr_reference (List.hd (head_constr cty)),
 	   { hname=name; pri=0; pat=None; code=Give_exact c })
 
 let make_apply_entry (eapply,verbose) name (c,cty) =
-  match hnf_constr (Global.env()) Evd.empty cty with
-    | DOP2(Prod,_,_) as cty ->
+  let cty = hnf_constr (Global.env()) Evd.empty cty in
+  match kind_of_term cty with
+    | IsProd _ ->
         let ce = mk_clenv_from () (c,cty) in
 	let pat = Pattern.pattern_of_constr (clenv_template_type ce).rebus in
         let hd = (try head_pattern_bound pat
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index d673b9316..aeb3f306c 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -2,7 +2,7 @@
 (* $Id$ *)
 
 (*i*)
-open Generic
+(*i open Generic i*)
 open Term
 open Pattern
 (*i*)
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 237af5c06..4190cb17d 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -107,7 +107,7 @@ Qed.
 open Pp
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Environ
 open Reduction
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 25bb62ab4..6eab9ae08 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Sign
 open Reduction
@@ -70,16 +70,11 @@ let prolog_tac lcom n gl =
     errorlabstrm "Prolog.prolog" [< 'sTR "Prolog failed" >]
 
 let evars_of evc c = 
-  let rec evrec acc = function
-    | DOPN(Evar n,_) as k when Evd.in_dom evc n -> k :: acc
-    | DOPN(_,cl) -> Array.fold_right (fun c acc -> evrec acc c) cl acc
-    | DOP2(_,c1,c2) -> evrec (evrec acc c2) c1
-    | DOP1(_,c) -> evrec acc c
-    | DLAM(_,c) -> evrec acc c
-    | DLAMV(_,cl) -> Array.fold_right (fun c acc -> evrec acc c) cl acc
-    | _ -> acc
+  let rec evrec acc c = match splay_constr c with
+    | OpEvar n, _ when Evd.in_dom evc n -> c :: acc
+    | _, cl -> Array.fold_left evrec acc cl
   in 
-  List.rev (evrec [] c)
+  evrec [] c
 
 let instantiate n c gl =
   let sigma = project gl in
diff --git a/tactics/elim.ml b/tactics/elim.ml
index a9df949ea..0fbfcae9a 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Reduction
 open Inductive
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ae5bed674..c301b62d1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Names
 open Univ
-open Generic
+(*i open Generic i*)
 open Term
 open Inductive
 open Environ
@@ -40,7 +40,7 @@ let general_rewrite_bindings lft2rgt (c,l) gl =
   let ctype = pf_type_of gl c in 
   let env = pf_env gl in
   let sigma = project gl in 
-  let sign,t = splay_prod env sigma ctype in
+  let _,t = splay_prod env sigma ctype in
   match match_with_equation t with
     | None -> error "The term provided does not end with an equation" 
     | Some (hdcncl,_) -> 
@@ -267,12 +267,6 @@ let match_eq eqn eq_pat =
     | [(1,t);(2,x);(3,y)] -> (t,x,y)
     | _ -> anomaly "match_eq: an eq pattern should match 3 terms"
 
-
-let rec hd_of_prod prod =
-  match strip_outer_cast prod with
-    | (DOP2(Prod,c,DLAM(n,t'))) -> hd_of_prod t'
-    |  t -> t
-
 type elimination_types =
   | Set_Type
   | Type_Type
@@ -470,8 +464,8 @@ let descend_then sigma env head dirn =
 	let result = if i = dirn then dirnval else dfltval in
 	it_mkLambda_or_LetIn_name env result cstr.(i-1).cs_args
       in
-      mkMutCase (make_default_case_info mispec) p head 
-	(List.map build_branch (interval 1 (mis_nconstr mispec)))))
+      mkMutCase (make_default_case_info mispec, p, head,
+		 List.map build_branch (interval 1 (mis_nconstr mispec)))))
   
 (* Now we need to construct the discriminator, given a discriminable
    position.  This boils down to:
@@ -515,8 +509,8 @@ let construct_discriminator sigma env dirn c sort =
     it_mkLambda_or_LetIn endpt cstrs.(i-1).cs_args 
   in
   let build_match =
-    mkMutCase (make_default_case_info mispec) p c 
-      (List.map build_branch (interval 1 (mis_nconstr mispec)))
+    mkMutCase (make_default_case_info mispec, p, c,
+	       List.map build_branch (interval 1 (mis_nconstr mispec)))
   in
   build_match
     
@@ -571,8 +565,8 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq gls =
   let env = pf_env gls in
   let (indt,_) = find_mrectype env (project gls) t in 
   let arity = Global.mind_arity indt in
-  let sort = pf_type_of gls (pf_concl gls) in 
-  match necessary_elimination (destSort(hd_of_prod arity)) (destSort sort) with
+  let sort = pf_type_of gls (pf_concl gls) in
+  match necessary_elimination (snd (destArity arity)) (destSort sort) with
     | Type_Type  ->
  	let eq_elim     = build_rect lbeq in
 	let eq_term     = build_eq lbeq in
@@ -710,14 +704,14 @@ let find_sigma_data s =
  *)
 
 let make_tuple env sigma (rterm,rty) lind =
-  if dependent (Rel lind) rty then
+  if dependent (mkRel lind) rty then
     let {intro = exist_term; ex = sig_term} =
       find_sigma_data (get_sort_of env sigma rty) in
     let a = type_of env sigma (Rel lind) in
     (* We replace (Rel lind) by (Rel 1) in rty then abstract on (na:a) *)
     let rty' = substnl [Rel 1] lind rty in
     let na = fst (lookup_rel_type lind env) in
-    let p = mkLambda na a rty' in
+    let p = mkLambda (na, a, rty') in
     (applist(exist_term,[a;p;(Rel lind);rterm]),
      applist(sig_term,[a;p]))
   else
@@ -859,10 +853,10 @@ let build_injector sigma env (t1,t2) c cpath =
 let try_delta_expand env sigma t =
   let whdt = whd_betadeltaiota env sigma t  in 
   let rec hd_rec c  =
-    match c with
-      | DOPN(MutConstruct _,_) -> whdt
-      | DOPN(AppL,cl)  -> hd_rec (array_hd cl)
-      | DOP2(Cast,c,_) -> hd_rec c
+    match kind_of_term c with
+      | IsMutConstruct _ -> whdt
+      | IsAppL (f,_)  -> hd_rec f
+      | IsCast (c,_) -> hd_rec c
       | _  -> t
   in 
   hd_rec whdt 
@@ -1200,7 +1194,7 @@ let subst_tuple_term env sigma dep_pair b =
 let revSubstInConcl eqn gls =
   let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in
   let body = subst_tuple_term (pf_env gls) (project gls) e2 (pf_concl gls) in
-  assert (dependent (Rel 1) body);
+  assert (dependent (mkRel 1) body);
   bareRevSubstInConcl lbeq body (t,e1,e2) gls
 
 (* |- (P e1)
@@ -1216,7 +1210,7 @@ let substInConcl eqn gls =
 let substInHyp eqn id gls =
   let (lbeq,(t,e1,e2)) = (find_eq_data_decompose eqn) in 
   let body = subst_term e1 (clause_type (Some id) gls) in
-  if not (dependent (Rel 1) body) then errorlabstrm  "SubstInHyp" [<>];
+  if not (dependent (mkRel 1) body) then errorlabstrm  "SubstInHyp" [<>];
   (tclTHENS (cut_replacing id (subst1 e2 body))
      ([tclIDTAC;
        (tclTHENS (bareRevSubstInConcl lbeq body (t,e1,e2))
@@ -1251,118 +1245,104 @@ let rec list_int n cmr l =
 
 (* Tells if two constrs are equal modulo unification *)
 
+(* Alpha-conversion *)
 let bind_eq = function
   | (Anonymous,Anonymous) -> true
   | (Name _,Name _) -> true
   | _ -> false
 
-let rec eq_mod_rel l_meta = function
-  | (t,DOP0(Meta n)) ->
-      if not (List.mem n (fst (List.split l_meta))) then
-	Some ([(n,t)]@l_meta)
-      else if (List.assoc n l_meta) = t then
-	Some l_meta
-     else
-       None
-  | (DOP1(op0,c0),DOP1(op1,c1)) ->
-      if op0 = op1 then
-	eq_mod_rel l_meta (c0,c1)
-      else
-	None
-  | (DOP2(op0,t0,c0),DOP2(op1,t1,c1)) ->
-      if op0 = op1 then
-	match (eq_mod_rel l_meta (t0,t1)) with
-          | None -> None
-          | Some l -> eq_mod_rel l (c0,c1)	
-      else
-	None
-  | (DOPN(op0,t0),DOPN(op1,t1)) ->
-      if (op0 = op1) & (Array.length t0 = Array.length t1) then
-	List.fold_left2
-          (fun a c1 c2 ->
-             match a with
-	       | None -> None
-               | Some l -> eq_mod_rel l (c1,c2)) (Some l_meta)
-          (Array.to_list t0) (Array.to_list t1)
-      else
-	None
-  | (DLAM(n0,t0),DLAM(n1,t1)) ->
-      if bind_eq (n0,n1) then
-	eq_mod_rel l_meta (t0,t1)
-      else
-	None
-  | (t,u) ->
-      if t = u then
-	Some l_meta
-      else
-	None
+let eqop_mod_names = function
+  | OpLambda n0, OpLambda n1 -> bind_eq (n0,n1)
+  | OpProd n0, OpProd n1 -> bind_eq (n0,n1)
+  | OpLetIn n0, OpLetIn n1 -> bind_eq (n0,n1)
+  | op0, op1 -> op0 = op1
+
+exception NotEqModRel
+
+let rec eq_mod_rel l_meta t0 t1 =
+  match splay_constr_with_binders t1 with
+    | OpMeta n, [], [||] ->
+	if not (List.mem_assoc n l_meta) then
+	  [(n,t0)]@l_meta
+	else if (List.assoc n l_meta) = t0 then
+	  l_meta
+	else
+	  raise NotEqModRel
+    | op1, bd1, v1 ->
+	match splay_constr_with_binders t0 with
+	  | op0, bd0, v0
+	      when (eqop_mod_names (op0, op1)
+		    & (List.length bd0 = List.length bd1)
+		    & (Array.length v0 = Array.length v1)) ->
+	      array_fold_left2 eq_mod_rel
+		(List.fold_left2 eq_mod_rel_binders l_meta bd0 bd1)
+		v0 v1
+	    | _ -> raise NotEqModRel
+
+  and eq_mod_rel_binders l_meta t0 t1 = match (t0,t1) with
+    | (na0,Some b0,t0), (na1,Some b1,t1) when bind_eq (na0,na1) ->
+	eq_mod_rel (eq_mod_rel l_meta b0 b1) t0 t1
+    | (na0,None,t0), (na1,None,t1) when bind_eq (na0,na1) ->
+	eq_mod_rel l_meta t0 t1
+    | _ -> raise NotEqModRel
 
 (* Verifies if the constr has an head constant *)
 
-let is_hd_const = function
-  | DOPN(AppL,t) ->
-      (match t.(0) with
-         | DOPN(Const c,_) -> Some (Const c, array_tl t)
+let is_hd_const c = match kind_of_term c with
+  | IsAppL (f,args) ->
+      (match kind_of_term f with
+         | IsConst (c,_) -> Some (c, Array.of_list args)
          |_ -> None)
   | _ -> None
-	  
-(* Gives the occurences number of t in u *)
-let rec nb_occ_term t u =
-  let one_step t = function
-    | DOP1(_,c) -> nb_occ_term t c
-    | DOP2(_,c0,c1) -> (nb_occ_term t c0) + (nb_occ_term t c1)
-    | DOPN(_,a) -> Array.fold_left (fun a x -> a + (nb_occ_term t x)) 0 a
-    | DOPL(_,l) -> List.fold_left (fun a x -> a + (nb_occ_term t x)) 0 l
-    | DLAM(_,c) -> nb_occ_term t c
-    | DLAMV(_,a) -> Array.fold_left (fun a x -> a + (nb_occ_term t x)) 0 a
-    | _ -> 0
-  in
-  if t = u then
-    1
-  else
-    one_step t u
 
-(* Gives Some(first instance of ceq in cref,occurence number for this
-   instance) or None if no instance of ceq can be found in cref *)
+(* Gives the occurrences number of a t in u
+   Rem: t is assumed closed then there is no need to lift it
+*)
+
+let nb_occ_term t u =
+  let rec nbrec nocc u =
+    if t = u then   (* Pourquoi pas eq_constr ?? *)
+      nocc + 1
+    else
+      Array.fold_left nbrec nocc (snd (splay_constr u))
+  in nbrec 0 u
+    
 
+(* Gives Some(first instance of ceq in cref,occurence number for this
+   instance) or None if no instance of ceq can be found in cref
+   Rem: t_eq is assumed closed then there is no need to lift it
+*)
 let sub_term_with_unif cref ceq =
-  let rec find_match l_meta nb_occ op_ceq t_eq = function
-    | DOPN(AppL,t) as u ->
-	(match (t.(0)) with
-           | DOPN(op,t_op) ->
-               let t_args=Array.of_list (List.tl (Array.to_list t)) in
-               if op = op_ceq then
-                 match
-                   (List.fold_left2 
-                      (fun a c0 c1 ->
-                         match a with
-                           | None -> None
-                           | Some l -> eq_mod_rel l (c0,c1)) (Some l_meta)
-                      (Array.to_list t_args) (Array.to_list t_eq))
-                 with
-                   | None ->
-                       List.fold_left
-                         (fun (l_meta,nb_occ) x -> find_match l_meta nb_occ
-                              op_ceq t_eq x) (l_meta,nb_occ) (Array.to_list
-								t_args)
-                   | Some l -> (l,nb_occ+1)
-               else
-                 List.fold_left 
-		   (fun (l_meta,nb_occ) x -> find_match l_meta
-			nb_occ op_ceq t_eq x) (l_meta,nb_occ) (Array.to_list t)
-           | VAR _ ->
-	       List.fold_left 
+  let rec find_match l_meta nb_occ hdsp t_args u = match splay_constr u with
+    | OpAppL, cl -> begin
+	let f, args = destApplication u in
+	match kind_of_term f with
+          | IsConst (sp,_) when sp = hdsp -> begin
+	      try (array_fold_left2 eq_mod_rel l_meta args t_args, nb_occ+1)
+	      with NotEqModRel ->
+		Array.fold_left
+                  (fun (l_meta,nb_occ) x -> find_match l_meta nb_occ
+                       hdsp t_args x) (l_meta,nb_occ) args
+	    end
+
+          | IsConst _ | IsVar _ | IsMutInd _ | IsMutConstruct _
+	  | IsFix _ | IsCoFix _ ->
+               Array.fold_left 
 		 (fun (l_meta,nb_occ) x -> find_match l_meta
-		      nb_occ op_ceq t_eq x) (l_meta,nb_occ) (Array.to_list t)
-           |_ -> (l_meta,nb_occ))
-    | DOP2(_,t,DLAM(_,c)) ->
-	let (lt,nbt)=find_match l_meta nb_occ op_ceq t_eq t in
-        find_match lt nbt op_ceq t_eq c
-    | DOPN(_,t) -> 
-	List.fold_left 
-	  (fun (l_meta,nb_occ) x -> find_match l_meta nb_occ op_ceq
-	       t_eq x) (l_meta,nb_occ) (Array.to_list t)
-    |_ -> (l_meta,nb_occ)
+		      nb_occ hdsp t_args x) (l_meta,nb_occ) cl
+
+	   (* Pourquoi ne récurre-t-on pas dans f ? *)
+           | _ -> (l_meta,nb_occ)
+      end
+
+(* Le code original ne récurrait pas sous les Cast 
+    | OpCast, _ -> (l_meta,nb_occ)
+*)
+    | _, t -> 
+	Array.fold_left 
+	  (fun (l_meta,nb_occ) x -> find_match l_meta nb_occ hdsp t_args x)
+	  (l_meta,nb_occ) t
+
   in
   match (is_hd_const ceq) with
     | None ->
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 285da7261..fd54744fe 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Reduction
 open Inductive
@@ -211,9 +211,9 @@ let match_with_nottype t =
 
 let is_nottype t = op2bool (match_with_nottype t)
 		     
-let is_imp_term = function
-  | DOP2(Prod,_,DLAM(_,b)) -> not (dependent (Rel 1) b)
-  | _                      -> false
+let is_imp_term c = match kind_of_term c with
+  | IsProd (_,_,b) -> not (dependent (mkRel 1) b)
+  | _              -> false
 
 
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 39254ace0..82863269b 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Global
 open Sign
@@ -323,9 +323,7 @@ let res_case_then gene thin indbinding id status gl =
   let env = pf_env gl and sigma = project gl in
   let c = VAR id in
   let (wc,kONT) = startWalk gl in
-  let t = 
-    strong_prodspine (fun _ _ -> pf_whd_betadeltaiota gl) 
-      env sigma (pf_type_of gl c) in
+  let t = strong_prodspine (pf_whd_betadeltaiota gl) (pf_type_of gl c) in
   let indclause = mk_clenv_from wc (c,t) in
   let indclause' = clenv_constrain_with_bindings indbinding indclause in
   let newc = clenv_instance_template indclause' in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 9e4386f1d..57baf0b15 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Sign
 open Evd
@@ -130,6 +130,11 @@ let rec add_prods_sign env sigma t =
 	let b'= subst1 (VAR id) b in
 	let j = Retyping.get_assumption_of env sigma c1 in
         add_prods_sign (Environ.push_var_decl (id,j) env) sigma b'
+    | IsLetIn (na,c1,t1,b) ->
+	let id = Environ.id_of_name_using_hdchar env t na in
+	let b'= subst1 (VAR id) b in
+	let j = Retyping.get_assumption_of env sigma t1 in
+        add_prods_sign (Environ.push_var_def (id,c1,j) env) sigma b'
     | _ -> (env,t)
 
 (* [dep_option] indicates wether the inversion lemma is dependent or not.
@@ -153,7 +158,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
     if dep_option  then
       let pty = make_arity env true indf sort in
       let goal = 
-	mkProd Anonymous (mkAppliedInd ind) (applist(VAR p,realargs@[Rel 1]))
+	mkProd (Anonymous, mkAppliedInd ind, applist(VAR p,realargs@[Rel 1]))
       in
       pty,goal
     else
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index 09b772950..ae0f5a6c9 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -3,7 +3,7 @@
 
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Libobject
 open Library
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index 5100d6c66..f68fc89e7 100644
--- a/tactics/nbtermdn.mli
+++ b/tactics/nbtermdn.mli
@@ -2,7 +2,7 @@
 (* $Id$ *)
 
 (*i*)
-open Generic
+(*i open Generic i*)
 open Term
 open Pattern
 (*i*)
diff --git a/tactics/refine.ml b/tactics/refine.ml
index e4a36a525..f188eba7f 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -42,7 +42,7 @@
 open Pp
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Tacmach
 open Sign
@@ -85,24 +85,24 @@ and pp_sg sg =
  *)
 
 let replace_by_meta env = function
-  | TH (DOP0(Meta _) | DOP2(Cast,DOP0(Meta _),_) as m, mm, sgp) -> m,mm,sgp
+  | TH (m, mm, sgp) when isMeta (strip_outer_cast m) -> m,mm,sgp
   | (TH (c,mm,_)) as th ->
       let n = new_meta() in
       let m = DOP0(Meta n) in
       (* quand on introduit une mv on calcule son type *)
-      let ty = match c with
-	| DOP2(Lambda,c1,DLAM(Name id,DOP2(Cast,_,ty))) ->
-	    mkNamedProd id c1 ty
-	| DOP2(Lambda,c1,DLAM(Anonymous,DOP2(Cast,_,ty))) ->
-	    mkArrow c1 ty
-	| DOPN((AppL|MutCase _),_) ->
+      let ty = match kind_of_term c with
+	| IsLambda (Name id,c1,c2) when isCast c2 ->
+	    mkNamedProd id c1 (snd (destCast c2))
+	| IsLambda (Anonymous,c1,c2) when isCast c2 ->
+	    mkArrow c1 (snd (destCast c2))
+	| (IsAppL _ | IsMutCase _) ->
 	    (** let j = ise_resolve true empty_evd mm (gLOB sign) c in **)
 	    Retyping.get_type_of_with_meta env Evd.empty mm c
-	| DOPN(Fix (_,j),v) ->
+	| IsFix ((_,j),(v,_,_)) ->
 	    v.(j) (* en pleine confiance ! *)
 	| _ -> invalid_arg "Tcc.replace_by_meta (TO DO)" 
       in
-      DOP2(Cast,m,ty),[n,ty],[Some th]
+      mkCast (m,ty),[n,ty],[Some th]
 
 exception NoMeta
 
@@ -122,24 +122,22 @@ let fresh env n =
   let id = match n with Name x -> x | _ -> id_of_string "_" in
   next_global_ident_away id (ids_of_var_context (var_context env))
 
-let rec compute_metamap env = function
+let rec compute_metamap env c = match kind_of_term c with
   (* le terme est directement une preuve *)
-  | DOP0(Sort _)
-  | DOPN((Const _ | Abst _ | MutInd _ | MutConstruct _),_)
-  | VAR _ | Rel _ as c -> TH (c,[],[])
+  | (IsConst _ | IsEvar _ | IsAbst _ | IsMutInd _ | IsMutConstruct _ |
+    IsSort _ | IsVar _ | IsRel _) -> TH (c,[],[])
 
   (* le terme est une mv => un but *)
-  | DOP0(Meta n) as c ->
+  | IsMeta n ->
       Pp.warning (Printf.sprintf ("compute_metamap: MV(%d) sans type !\n") n);
       TH (c,[],[None])
-  | DOP2(Cast,DOP0(Meta n),ty) as c -> TH (c,[n,ty],[None])
+  | IsCast (DOP0(Meta n),ty) -> TH (c,[n,ty],[None])
 
   (* abstraction => il faut décomposer si le terme dessous n'est pas pur
    *    attention : dans ce cas il faut remplacer (Rel 1) par (VAR x)
    *    où x est une variable FRAICHE *)
-  | DOP2(Lambda,c1,DLAM(name,c2)) as c ->
+  | IsLambda (name,c1,c2) ->
       let v = fresh env name in
-      (** let tj = ise_resolve_type true empty_evd [] (gLOB sign) c1 in **)
       let tj = Retyping.get_assumption_of env Evd.empty c1 in
       let env' = push_var_decl (v,tj) env in
       begin match compute_metamap env' (subst1 (VAR v) c2) with
@@ -148,11 +146,26 @@ let rec compute_metamap env = function
 	(* terme de preuve incomplet *)    
 	| th ->
 	    let m,mm,sgp = replace_by_meta env' th in
-	    TH (DOP2(Lambda,c1,DLAM(Name v,m)), mm, sgp)
+	    TH (mkLambda (Name v,c1,m), mm, sgp)
       end
 
+  | IsLetIn (name, c1, t1, c2) -> (* Adaptation to confirm *)
+      compute_metamap env (subst1 c1 c2)
+
   (* 4. Application *)
-  | DOPN((AppL|MutCase _) as op,v) as c ->
+  | IsAppL (f,v) ->
+      let a = Array.map (compute_metamap env) (Array.of_list (f::v)) in
+      begin
+	try
+	  let v',mm,sgp = replace_in_array env a in TH (mkAppL v',mm,sgp)
+	with NoMeta ->
+	  TH (c,[],[])
+      end
+
+  | IsMutCase _ ->
+      (* bof... *)
+      let op,v =
+	match c with DOPN(MutCase _ as op,v) -> (op,v) | _ -> assert false in
       let a = Array.map (compute_metamap env) v in
       begin
 	try
@@ -162,8 +175,7 @@ let rec compute_metamap env = function
       end
 
   (* 5. Fix. *)
-  | DOPN(Fix _,_) as c ->
-      let ((ni,i),(ai,fi,v)) = destFix c in
+  | IsFix ((ni,i),(ai,fi,v)) ->
       let vi = List.rev (List.map (fresh env) fi) in
       let env' =
 	List.fold_left
@@ -186,19 +198,19 @@ let rec compute_metamap env = function
       end
 	      
   (* Cast. Est-ce bien exact ? *)
-  | DOP2(Cast,c,t) -> compute_metamap env c
+  | IsCast (c,t) -> compute_metamap env c
       (*let TH (c',mm,sgp) = compute_metamap sign c in
-	TH (DOP2(Cast,c',t),mm,sgp) *)
+	TH (mkCast (c',t),mm,sgp) *)
       
   (* Produit. Est-ce bien exact ? *)
-  | DOP2(Prod,_,_) as c ->
+  | IsProd (_,_,_) ->
       if occur_meta c then
 	error "Refine: proof term contains metas in a product"
       else
       	TH (c,[],[])
- 
+
   (* Autres cas. *)
-  | _ ->
+  | IsXtra _|IsCoFix _ ->
       invalid_arg "Tcc.compute_metamap"
 
 
@@ -208,9 +220,12 @@ let rec compute_metamap env = function
  *)
 
 let rec tcc_aux (TH (c,mm,sgp) as th) gl =
-  match (c,sgp) with
+  match (kind_of_term c,sgp) with
     (* mv => sous-but : on ne fait rien *)
-    | (DOP0(Meta _) | DOP2(Cast,DOP0(Meta _),_)) , _ ->
+    | IsMeta _ , _ ->
+	tclIDTAC gl
+
+    | IsCast (c,_), _ when isMeta c ->
 	tclIDTAC gl
 	  
     (* terme pur => refine *)
@@ -218,8 +233,7 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl =
 	refine c gl
 	
     (* abstraction => intro *)
-    | DOP2(Lambda,_,
-	   DLAM(Name id,(DOP0(Meta _)|DOP2(Cast,DOP0(Meta _),_) as m))) ,_ ->
+    | IsLambda (Name id,_,m) , _ when isMeta (strip_outer_cast m) ->
 	begin match sgp with
 	  | [None] -> introduction id gl
 	  | [Some th] ->
@@ -227,12 +241,11 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl =
 	  | _ -> invalid_arg "Tcc.tcc_aux (bad length)"
 	end
 	
-    | DOP2(Lambda,_,_),_ ->
+    | IsLambda (_,_,_) , _ ->
 	error "invalid abstraction passed to function tcc_aux !"
       
     (* fix => tactique Fix *)
-    | DOPN(Fix _,_) , _ ->
-      	let ((ni,_),(ai,fi,_)) = destFix c in
+    | IsFix ((ni,_),(ai,fi,_)) , _ ->
 	let ids =
 	  List.map (function Name id -> id | _ ->
 		      error "recursive functions must have names !") fi 
@@ -269,7 +282,7 @@ let my_constr_of_com_casted sigma env com typ =
   Printf.printf "LA\n"; flush stdout;
   c
   (**
-  let cc = mkCast (nf_ise1 sigma c) (nf_ise1 sigma typ) in
+  let cc = mkCast (nf_ise1 sigma c, nf_ise1 sigma typ) in
   try (unsafe_machine env sigma cc).uj_val
   with e -> Stdpp.raise_with_loc (Ast.loc com) e
   **)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index a37a395dd..87a4370cb 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Sign
 open Declarations
@@ -243,17 +243,22 @@ type branch_assumptions = {
  *  --Eduardo (11/8/97) *)
 
 let reduce_to_ind_goal gl t = 
-  let rec elimrec t l = 
-    match decomp_app(t) with
-      | (DOPN(MutInd ind_sp,args) as mind,_) -> 
-	  ((ind_sp,args),path_of_inductive_path ind_sp,t,prod_it t l)
-      | (DOPN(Const _,_),_) -> 
-	  elimrec (pf_nf_betaiota gl (pf_one_step_reduce gl t)) l
-      | (DOP2(Cast,c,_),[]) -> elimrec c l
-      | (DOP2(Prod,ty,DLAM(n,t')),[]) -> elimrec t' ((n,ty)::l)
+  let rec elimrec t =
+    let c,args = decomp_app t in
+    match kind_of_term c with
+      | IsMutInd (ind_sp,args as ity) -> 
+	  ((ity, path_of_inductive_path ind_sp, t), t)
+      | IsConst _ ->
+	  elimrec (pf_nf_betaiota gl (pf_one_step_reduce gl t))
+      | IsCast (c,_) when args = [] ->
+	  elimrec c
+      | IsProd (n,ty,t') when args = [] ->
+	  let (ind, t) = elimrec t' in (ind, mkProd (n,ty,t))
+      | IsLetIn (n,c,ty,t') when args = [] ->
+	  let (ind, t) = elimrec t' in (ind, mkLetIn (n,c,ty,t))
       | _ -> error "Not an inductive product"
   in 
-  elimrec t []
+  elimrec t
 
 let case_sign ity i = 
   let rec analrec acc = function 
@@ -284,13 +289,13 @@ let sort_of_goal gl =
 (* Find the right elimination suffix corresponding to the sort of the goal *)
 (* c should be of type A1->.. An->B with B an inductive definition *)
 
-let last_arg = function
-  | DOPN(AppL,cl) -> cl.(Array.length cl - 1)
+let last_arg c = match kind_of_term c with
+  | IsAppL (f,cl) -> List.nth cl (List.length cl - 1)
   | _ -> anomaly "last_arg"
 
 let general_elim_then_using 
   elim elim_sign_fun tac predicate (indbindings,elimbindings) c gl =
-  let (ity,_,_,t) = reduce_to_ind_goal gl (pf_type_of gl c) in
+  let ((ity,_,_),t) = reduce_to_ind_goal gl (pf_type_of gl c) in
   let name_elim =
     (match elim with
        | DOPN(Const sp,_) -> id_of_string(string_of_path sp)
@@ -302,10 +307,10 @@ let general_elim_then_using
   let indclause  = mk_clenv_from wc (c,t) in
   let indclause' = clenv_constrain_with_bindings indbindings indclause in
   let elimclause = mk_clenv_from () (elim,w_type_of wc elim) in
-  let indmv  = 
-    match last_arg (clenv_template elimclause).rebus with
-      | DOP0(Meta mv) -> mv
-      | _            -> error "elimination"
+  let indmv = 
+    match kind_of_term (last_arg (clenv_template elimclause).rebus) with
+      | IsMeta mv -> mv
+      | _         -> error "elimination"
   in
   let pmv = 
     match decomp_app (clenv_template_type elimclause).rebus with
@@ -338,7 +343,7 @@ let general_elim_then_using
 
 
 let elimination_then_using tac predicate (indbindings,elimbindings) c gl = 
-  let (ity,path_name,_,t) = reduce_to_ind_goal gl (pf_type_of gl c) in
+  let ((ity,path_name,_),t) = reduce_to_ind_goal gl (pf_type_of gl c) in
   let elim = lookup_eliminator (pf_env gl) path_name (sort_of_goal gl) in
   general_elim_then_using
     elim elim_sign tac predicate (indbindings,elimbindings) c gl
@@ -349,7 +354,7 @@ let simple_elimination_then tac = elimination_then tac ([],[])
 
 let case_then_using tac predicate (indbindings,elimbindings) c gl =
   (* finding the case combinator *)
-  let (ity,_,_,t) = reduce_to_ind_goal gl (pf_type_of gl c) in
+  let ((ity,_,_),t) = reduce_to_ind_goal gl (pf_type_of gl c) in
   let sigma = project gl in 
   let sort  = sort_of_goal gl  in
   let elim  = Indrec.make_case_gen (pf_env gl) sigma ity sort in  
@@ -358,7 +363,7 @@ let case_then_using tac predicate (indbindings,elimbindings) c gl =
 
 let case_nodep_then_using tac predicate (indbindings,elimbindings) c gl =
   (* finding the case combinator *)
-  let (ity,_,_,t) = reduce_to_ind_goal gl (pf_type_of gl c) in
+  let ((ity,_,_),t) = reduce_to_ind_goal gl (pf_type_of gl c) in
   let sigma = project gl in 
   let sort  = sort_of_goal gl  in
   let elim  = Indrec.make_case_nodep (pf_env gl) sigma ity sort in  
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2c418bbae..3b24ad75d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@ open Util
 open Stamps
 open Names
 open Sign
-open Generic
+(*i open Generic i*)
 open Term
 open Inductive
 open Reduction
@@ -67,15 +67,14 @@ let string_head c =
 
 let rec head_constr_bound t l =
   let t = strip_outer_cast(collapse_appl t) in
-  match t with
-    | DOP2(Prod,_,DLAM(_,c2))     -> head_constr_bound c2 l 
-    | DOPN(AppL,cl)               -> 
-	head_constr_bound (array_hd cl) ((List.tl (Array.to_list cl))@l)
-    | DOPN(Const _,_) as x        -> x::l
-    | DOPN(MutInd _,_) as x       -> x::l
-    | DOPN(MutConstruct _,_) as x -> x::l
-    | VAR _ as x                  -> x::l
-    | _                           -> raise Bound
+  match kind_of_term t with
+    | IsProd (_,_,c2)  -> head_constr_bound c2 l 
+    | IsAppL (f,args)  -> head_constr_bound f (args@l)
+    | IsConst _        -> t::l
+    | IsMutInd _       -> t::l
+    | IsMutConstruct _ -> t::l
+    | IsVar _          -> t::l
+    | _                -> raise Bound
 
 let head_constr c = 
   try head_constr_bound c [] with Bound -> error "Bound head variable"
@@ -269,8 +268,8 @@ let id_of_name_with_default s = function
   | Name id   -> id
 
 let default_id gl =
-  match strip_outer_cast (pf_concl gl) with
-    | DOP2(Prod,c1,DLAM(name,c2)) ->
+  match kind_of_term (strip_outer_cast (pf_concl gl)) with
+    | IsProd (name,c1,c2) ->
   	(match pf_whd_betadeltaiota gl (pf_type_of gl c1) with
 	   | DOP0(Sort(Prop _))  -> (id_of_name_with_default "H" name)
 	   | DOP0(Sort(Type(_))) -> (id_of_name_with_default "X" name)
@@ -383,11 +382,11 @@ let dyn_intros_until = function
 
 let intros_do n g = 
   let depth = 
-    let rec lookup all nodep = function
-      | DOP2(Prod,_,DLAM(name,c')) -> 
+    let rec lookup all nodep c = match kind_of_term c with
+      | IsProd (name,_,c') -> 
 	  (match name with
 	     | Name(s')  -> 
-		 if dependent (Rel 1) c' then 
+		 if dependent (mkRel 1) c' then 
 		   lookup (all+1) nodep c'
 		 else if nodep = n then 
 		   all
@@ -395,7 +394,7 @@ let intros_do n g =
 		   lookup (all+1) (nodep+1) c'
              | Anonymous -> 
 		 if nodep=n then all else lookup (all+1) (nodep+1) c')
-      | DOP2(Cast,c,_) -> lookup all nodep c
+      | IsCast (c,_) -> lookup all nodep c
       | _ -> error "No such hypothesis in current goal"
     in 
     lookup 1 1 (pf_concl g)
@@ -453,11 +452,10 @@ let rec intros_rmove = function
  *  of the type of a term. *)
 
 let apply_type hdcty argl gl =
-  refine (DOPN(AppL,Array.of_list
-                 ((DOP2(Cast,DOP0(Meta(new_meta())),hdcty))::argl))) gl
+  refine (applist (mkCast (mkMeta (new_meta()),hdcty),argl)) gl
     
 let apply_term hdc argl gl =
-  refine (DOPN(AppL,Array.of_list(hdc::argl))) gl
+  refine (applist (hdc,argl)) gl
 
 let bring_hyps clsl gl = 
   let ids = 
@@ -495,8 +493,8 @@ let apply_with_bindings  (c,lbind) gl =
   let t = w_hnf_constr wc (w_type_of wc c) in 
   let clause = make_clenv_binding_apply wc (c,t) lbind in
   let apply = 
-    match c with 
-      | DOP2(Lambda,_,_) -> res_pf_cast 
+    match kind_of_term c with 
+      | IsLambda _ -> res_pf_cast 
       | _ -> res_pf 
   in 
   apply kONT clause gl
@@ -532,12 +530,12 @@ let dyn_apply l =
 
 let cut_and_apply c gl =
   let goal_constr = pf_concl gl in 
-  match (pf_hnf_constr gl (pf_type_of gl c)) with
-    | DOP2(Prod,c1,DLAM(_,c2)) when not (dependent (Rel 1) c2) ->
+  match kind_of_term (pf_hnf_constr gl (pf_type_of gl c)) with
+    | IsProd (_,c1,c2) when not (dependent (mkRel 1) c2) ->
 	tclTHENS 
-	  (apply_type (DOP2(Prod,c2,DLAM(Anonymous,goal_constr))) 
-	     [DOP0(Meta(new_meta()))]) 
-	  [tclIDTAC;apply_term c [DOP0(Meta(new_meta()))]] gl
+	  (apply_type (mkProd (Anonymous,c2,goal_constr))
+	     [DOP0(Meta(new_meta()))])
+	  [tclIDTAC;apply_term c [mkMeta (new_meta())]] gl
     | _ -> error "Imp_elim needs a non-dependent product"
 
 let dyn_cut_and_apply = function 
@@ -552,8 +550,8 @@ let dyn_cut_and_apply = function
 let cut c gl =
   match hnf_type_of gl c with
     | (DOP0(Sort _)) ->
-	apply_type (DOP2(Prod,c,DLAM(Anonymous,(pf_concl gl)))) 
-          [DOP0(Meta (new_meta()))] gl
+	apply_type (mkProd (Anonymous, c, pf_concl gl)) 
+          [mkMeta (new_meta())] gl
     | _  -> error "Not a proposition or a type"
 
 let dyn_cut = function
@@ -588,7 +586,7 @@ let generalize_goal gl c cl =
     | _        -> 
         let cl' = subst_term c cl in 
         if noccurn 1 cl' then 
-	  DOP2(Prod,t,DLAM(Anonymous,cl))
+	  mkProd (Anonymous,t,cl)
           (* On ne se casse pas la tete : on prend pour nom de variable
              la premiere lettre du type, meme si "ci" est une
              constante et qu'on pourrait prendre directement son nom *)
@@ -1057,17 +1055,19 @@ let induct_discharge indpath statuslists cname destopt avoid (_,t) =
       id_of_string ((string_of_id cname)^"_1") 
   in
   let hyprecname = id_of_string ("Hrec"^(string_of_id recvarname)) in
-  let rec peel_tac = function
-    | DOP2 (Prod,t,DLAM(na,DOP2(Prod,tr,DLAM(nar,c))))
-	when is_rec_arg indpath t
-	  -> if !tophyp=None then tophyp:=Some hyprecname;(* for lstatus *)
-	    tclTHENLIST
-	      [ central_intro (IBasedOn (recvarname,avoid)) destopt false;
-		central_intro (IBasedOn (hyprecname,avoid)) None false;
-		peel_tac c]
-    | DOP2 (Cast,c,_) -> peel_tac c
-    | DOP2 (Prod,t,DLAM(na,c))
-      -> tclTHEN (central_intro (IAvoid avoid) destopt false)
+  let rec peel_tac c = match kind_of_term c with
+    | IsProd (na,t,c2) when is_rec_arg indpath t ->
+	(match kind_of_term c2 with
+	   | IsProd (nar,tr,c3) ->
+	       if !tophyp=None then tophyp:=Some hyprecname;(* for lstatus *)
+	       tclTHENLIST
+		 [ central_intro (IBasedOn (recvarname,avoid)) destopt false;
+		   central_intro (IBasedOn (hyprecname,avoid)) None false;
+		   peel_tac c3]
+	   | _ -> anomaly "induct_discharge: rec arg leads to 2 products")
+    | IsCast (c,_) -> peel_tac c
+    | IsProd (na,t,c) ->
+	tclTHEN (central_intro (IAvoid avoid) destopt false)
 	  (peel_tac c)
     | _ -> tclIDTAC
   in
@@ -1271,7 +1271,7 @@ let induction_tac varname typ (elimc,elimt) gl =
   let c = VAR varname in
   let (wc,kONT)  = startWalk gl                    in
   let indclause  = make_clenv_binding wc (c,typ) []  in
-  let elimclause = make_clenv_binding wc (DOP2(Cast,elimc,elimt),elimt) [] in
+  let elimclause = make_clenv_binding wc (mkCast (elimc,elimt),elimt) [] in
   elimination_clause_scheme kONT wc elimclause indclause gl
 
 let get_constructors varname (elimc,elimt) mind mindpath =
@@ -1425,8 +1425,8 @@ let elim_scheme_type elim t gl =
 let elim_type t gl =
   let (path_name,tind,t) = reduce_to_ind (pf_env gl) (project gl) t in
   let elimc = lookup_eliminator (pf_env gl) path_name (sort_of_goal gl) in
-  match t with 
-    | DOP2(Prod,_,_) -> error "Not an inductive definition"
+  match kind_of_term t with 
+    | IsProd (_,_,_) -> error "Not an inductive definition"
     | _              -> elim_scheme_type elimc tind gl
 
 let dyn_elim_type = function
@@ -1437,8 +1437,8 @@ let dyn_elim_type = function
 let case_type t gl =
   let env = pf_env gl in
   let (mind,_,t) = reduce_to_mind env (project gl) t in  
-  match t with 
-    | DOP2(Prod,_,_) -> error "Not an inductive definition"
+  match kind_of_term t with 
+    | IsProd (_,_,_) -> error "Not an inductive definition"
     | _             -> 
         let sigma = project gl in 
         let sort  = sort_of_goal gl in
diff --git a/tactics/tauto.ml b/tactics/tauto.ml
index 47f7a40cf..416e81cd2 100644
--- a/tactics/tauto.ml
+++ b/tactics/tauto.ml
@@ -6,7 +6,7 @@
 open Pp
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Sign
 open Environ
@@ -65,7 +65,7 @@ let not_pattern_mark   = put_pat mmk "(not ?1)"
 let imply_squeleton = put_squel mmk "?1 -> ?2"
 let mkIMP a b = soinstance imply_squeleton [a;b]
 *)
-let mkIMP a b = mkProd Anonymous a b
+let mkIMP a b = mkProd (Anonymous, a, b)
 
 let false_pattern () = get_pat false_pattern_mark
 let true_pattern () = get_pat true_pattern_mark
@@ -1667,8 +1667,8 @@ let (tAUTOFAIL : tactic) = fun _ -> errorlabstrm "TAUTOFAIL"
                                           [< 'sTR "Tauto failed.">]
 
 let is_imp_term t =
-  match t with
-    | DOP2(Prod,_,DLAM(_,b)) -> (not((dependent (Rel 1) b)))
+  match kind_of_term t with
+    | IsProd (_,_,b) -> (not((dependent (mkRel 1) b)))
     | _ -> false
 
 (* Chet's code depends on the names of the logical constants. *)
@@ -1700,8 +1700,8 @@ let tauto_of_cci_fmla gls cciterm =
     else if pf_is_matching gls (true_pattern ()) cciterm then
       FTrue
     else if is_imp_term cciterm then
-      match cciterm with
-        | DOP2(Prod,a,DLAM(_,b)) -> FImp(tradrec a,tradrec (Generic.pop b))
+      match kind_of_term cciterm with
+        | IsProd (_,a,b) -> FImp(tradrec a,tradrec (pop b))
 	| _ -> assert false
     else FPred cciterm
   in 
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index ec621c4a7..9cdb34ab2 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -2,7 +2,7 @@
 (* $Id$ *)
 
 open Util
-open Generic
+(*i open Generic i*)
 open Names
 open Term
 open Pattern
@@ -16,10 +16,10 @@ type 'a t = (constr_label,constr_pattern,'a) Dn.t
 (*If we have: f a b c ..., decomp gives: (f,[a;b;c;...])*)
 
 let decomp = 
-  let rec decrec acc = function
-    | DOPN(AppL,cl) -> decrec (array_app_tl cl acc) (array_hd cl)
-    | DOP2(Cast,c1,_) -> decrec acc c1
-    | c -> (c,acc)
+  let rec decrec acc c = match kind_of_term c with
+    | IsAppL (f,l) -> decrec (l@acc) f
+    | IsCast (c1,_) -> decrec acc c1
+    | _ -> (c,acc)
   in 
   decrec []
 
@@ -41,12 +41,13 @@ let constr_pat_discr t =
       | _ -> None
 
 let constr_val_discr t =
-  match decomp t with
-    (* DOPN(Const _,_) as c,l -> Some(TERM c,l) *)
-    | DOPN(MutInd ind_sp,_) as c,l -> Some(IndNode ind_sp,l)
-    | DOPN(MutConstruct cstr_sp,_) as c,l -> Some(CstrNode cstr_sp,l)
-    | VAR id as c,l -> Some(VarNode id,l)
-    | c -> None
+  let c, l = decomp t in
+  match kind_of_term c with
+    (* IsConst _,_) -> Some(TERM c,l) *)
+    | IsMutInd (ind_sp,_) -> Some(IndNode ind_sp,l)
+    | IsMutConstruct (cstr_sp,_) -> Some(CstrNode cstr_sp,l)
+    | IsVar id -> Some(VarNode id,l)
+    | _ -> None
 
 (* Les deux fonctions suivantes ecrasaient les precedentes, 
    ajout d'un suffixe _nil CP 16/08 *) 
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index 10726df13..107026ef6 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -2,7 +2,7 @@
 (* $Id$ *)
 
 (*i*)
-open Generic
+(*i open Generic i*)
 open Term
 open Pattern
 (*i*)
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index 005be137e..25c63e536 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Sign
 open Reduction
@@ -91,9 +91,11 @@ let clenv_constrain_with_bindings bl clause =
     matchrec clause bl
 
 let add_prod_rel sigma (t,env) =
-  match t with
-    | DOP2(Prod,c1,(DLAM(na,b))) ->
-        (b,push_rel_decl (na,Retyping.get_assumption_of env sigma c1) env)
+  match kind_of_term t with
+    | IsProd (na,t1,b) ->
+        (b,push_rel_decl (na,Retyping.get_assumption_of env sigma t1) env)
+    | IsLetIn (na,c1,t1,b) ->
+        (b,push_rel_def (na,c1,Retyping.get_assumption_of env sigma t1) env)
     | _ -> failwith "add_prod_rel"
 
 let rec add_prods_rel sigma (t,env) =
@@ -102,22 +104,6 @@ let rec add_prods_rel sigma (t,env) =
   with Failure "add_prod_rel" -> 
     (t,env)
 
-(***TODO: SUPPRIMMER ??
-let add_prod_sign sigma (t,sign) =
-  match t with
-    | DOP2(Prod,c1,(DLAM(na,_) as b)) ->
-        let id = Environ.id_of_name_using_hdchar t na in  
-	(sAPP b (VAR id),
-         add_sign (id, fexecute_type sigma sign c1) sign)
-    | _ -> failwith "add_prod_sign"
-
-let rec add_prods_sign sigma (t,sign) =
-  try 
-    add_prods_sign sigma (add_prod_sign sigma (whd_betadeltaiota sigma t,sign))
-  with Failure "add_prod_sign" -> 
-    (t,sign)
-***)
-
 (* What follows is part of the contents of the former file tactics3.ml *)
     
 let res_pf_THEN kONT clenv tac gls =
@@ -133,22 +119,23 @@ let elim_res_pf_THEN_i kONT clenv tac gls =
   tclTHEN_i (clenv_refine kONT clenv') (tac clenv') gls
 
 let rec build_args acc ce p_0 p_1 =
-  match p_0,p_1 with 
-    | ((DOP2(Prod,a,DLAM(na,b))), (a_0::bargs)) ->
+  match kind_of_term p_0, p_1 with 
+    | (IsProd (na,a,b), (a_0::bargs)) ->
         let (newa,ce') = (build_term ce (na,Some a) a_0) in 
 	build_args (newa::acc) ce' (subst1 a_0 b) bargs
+    | (IsLetIn (na,a,t,b), args) -> build_args acc ce (subst1 a b) args
     | (_, [])     -> (List.rev acc,ce)
     | (_, (_::_)) -> failwith "mk_clenv_using"
 
-and build_term ce p_0 p_1 =
+and build_term ce p_0 c =
   let env = Global.env() in
-  match p_0,p_1 with 
-    | ((na,Some t), (DOP0(Meta mv))) -> 
+  match p_0, kind_of_term c with 
+    | ((na,Some t), IsMeta mv) -> 
 (*    	let mv = new_meta() in *)
 	(DOP0(Meta mv),
          clenv_pose (na,mv,t) ce)
-    | ((na,_), (DOP2(Cast,c,t))) -> build_term ce (na,Some t) c
-    | ((na,Some t), c) ->
+    | ((na,_), IsCast (c,t)) -> build_term ce (na,Some t) c
+    | ((na,Some t), _) ->
     	if (not((occur_meta c))) then 
 	  (c,ce)
     	else 
@@ -163,7 +150,7 @@ and build_term ce p_0 p_1 =
 	    (newc,ce') 
 	  else 
 	    failwith "mk_clenv_using"
-    | ((na,None), c) ->
+    | ((na,None), _) ->
     	if (not((occur_meta c))) then 
 	  (c,ce)
     	else 
@@ -195,13 +182,16 @@ let clenv_apply_n_times n ce =
   and templval = (clenv_template ce).rebus in   
   let rec apprec ce argacc (n,ty) =
     let env = Global.env () in
-    match (n, whd_betadeltaiota env (w_Underlying ce.hook) ty) with 
-      | (0, templtyp) ->
+    let templtyp = whd_betadeltaiota env (w_Underlying ce.hook) ty in
+    match (n, kind_of_term templtyp) with 
+      | (0, _) ->
 	  clenv_change_head (applist(templval,List.rev argacc), templtyp) ce
-      | (n, (DOP2(Prod,dom,DLAM(na,rng)))) ->
+      | (n, IsProd (na,dom,rng)) ->
           let mv = new_meta() in
           let newce = clenv_pose (na,mv,dom) ce in
 	  apprec newce (mkMeta mv::argacc) (n-1, subst1 (mkMeta mv) rng)
+      | (n, IsLetIn (na,b,t,c)) ->
+	  apprec ce argacc (n, subst1 b c)
       | (n, _) -> failwith "clenv_apply_n_times"
   in 
   apprec ce [] (n, templtyp)