Nettoyage de Generic

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

9 files changed, 287 insertions, 389 deletions

diff --git a/kernel/abstraction.ml b/kernel/abstraction.ml
index e0b86dbf27..9df751b46f 100644
--- a/kernel/abstraction.ml
+++ b/kernel/abstraction.ml
@@ -11,6 +11,15 @@ type abstraction_body = {
   abs_arity : int array;
   abs_rhs : constr }
 
+let rec count_dlam = function
+  | DLAM (_,c) -> 1 + (count_dlam c)
+  | _ -> 0
+
+let sAPP c n =
+  match c with 
+    | DLAM(na,m) -> subst1 n m
+    | _ -> invalid_arg "SAPP"
+	  
 let contract_abstraction ab args =
   if array_for_all2 (fun c i -> (count_dlam c) = i) args ab.abs_arity then
     Sosub.soexecute (Array.fold_left sAPP ab.abs_rhs args)
diff --git a/kernel/generic.ml b/kernel/generic.ml
index 2a8af630da..70acca45dd 100644
--- a/kernel/generic.ml
+++ b/kernel/generic.ml
@@ -23,9 +23,6 @@ type 'oper term =
 exception FreeVar
 exception Occur
 
-let isRel = function Rel _ -> true | _ -> false
-let isVAR = function VAR _ -> true | _ -> false
-
 (* returns the list of free debruijn indices in a term *)
 
 let free_rels m = 
@@ -59,7 +56,7 @@ let closedn =
   in 
   closed_rec
 
-(* (closed M) is true iff M is a (deBruijn) closed term *)
+(* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
 
 let closed0 term =
   try closedn 0 term; true with FreeVar -> false
@@ -80,10 +77,10 @@ let noccurn n term =
   in 
   try occur_rec n term; true with Occur -> false
 
-(* (noccur_bet n m M) returns true iff (Rel p) does NOT occur in term M 
+(* (noccur_between n m M) returns true iff (Rel p) does NOT occur in term M 
   for n <= p < n+m *)
 
-let noccur_bet n m term = 
+let noccur_between n m term = 
   let rec occur_rec n = function
     | Rel(p)        -> if n<=p && p<n+m then raise Occur
     | VAR _         -> ()
@@ -146,7 +143,8 @@ let liftn k n =
     | el -> exliftn el
  
 let lift k = liftn k 1
-let lift1 c = exliftn (ELSHFT(ELID,1)) c
+
+let pop t = lift (-1) t
 
 let lift_context n l = 
   let k = List.length l in 
@@ -242,85 +240,11 @@ let substn_many lamv n =
   in 
   substrec n
 
+let substnl laml k =
+  substn_many (Array.map make_substituend (Array.of_list laml)) k
 let substl laml =
   substn_many (Array.map make_substituend (Array.of_list laml)) 0
 let subst1 lam = substl [lam]
-let pop t = lift (-1) t
-
-
-(* Various occurs checks *)
-
-let occur_opern s = 
-  let rec occur_rec = function
-    | DOPN(oper,cl) -> s=oper or (array_exists occur_rec cl)
-    | DOPL(oper,cl) -> s=oper or (List.exists occur_rec cl)
-    | VAR _         -> false
-    | DOP1(_,c)     -> occur_rec c 
-    | DOP2(_,c1,c2) -> (occur_rec c1) or (occur_rec c2)
-    | DLAM(_,c)     -> occur_rec c
-    | DLAMV(_,v)    -> array_exists occur_rec v
-    | _             -> false
-  in 
-  occur_rec 
-
-let occur_oper0 s = 
-  let rec occur_rec = function
-    | DOPN(_,cl)    -> (array_exists occur_rec cl)
-    | DOPL(_,cl)    -> (List.exists occur_rec cl)
-    | DOP0 oper     -> s=oper
-    | VAR _         -> false
-    | DOP1(_,c)     -> occur_rec c 
-    | DOP2(_,c1,c2) -> (occur_rec c1) or (occur_rec c2)
-    | DLAM(_,c)     -> occur_rec c
-    | DLAMV(_,v)    -> array_exists occur_rec v
-    | _             -> false
-  in 
-  occur_rec 
-
-let occur_var s = 
-  let rec occur_rec = function
-    | DOPN(_,cl)    -> array_exists occur_rec cl
-    | DOPL(_,cl)    -> List.exists occur_rec cl
-    | VAR id        -> s=id
-    | DOP1(_,c)     -> occur_rec c 
-    | DOP2(_,c1,c2) -> (occur_rec c1) or (occur_rec c2)
-    | DLAM(_,c)     -> occur_rec c
-    | DLAMV(_,v)    -> array_exists occur_rec v
-    | _             -> false
-  in 
-  occur_rec 
-
-let occur_oper s = 
-  let rec occur_rec = function
-    | DOPN(oper,cl)    -> s=oper or (array_exists occur_rec cl)
-    | DOPL(oper,cl)    -> s=oper or (List.exists occur_rec cl)
-    | VAR _            -> false
-    | DOP0 oper        -> s=oper
-    | DOP1(oper,c)     -> s=oper or occur_rec c 
-    | DOP2(oper,c1,c2) -> s=oper or (occur_rec c1) or (occur_rec c2)
-    | DLAM(_,c)        -> occur_rec c
-    | DLAMV(_,v)       -> array_exists occur_rec v
-    | _                -> false
-  in 
-  occur_rec 
-
-let process_opers_of_term p f l constr = 
-  let rec filtrec acc = function
-    | DOP0 oper        -> if p oper then ((f oper)::acc) else acc
-    | VAR _            -> acc
-    | DOP1(oper,c)     -> let newacc = filtrec acc c in
-                          if p oper then ((f oper)::newacc) else newacc
-    | DOP2(oper,c1,c2) -> let newacc = filtrec (filtrec acc c1) c2 in
-                          if p oper then ((f oper)::newacc) else newacc
-    | DOPN(oper,cl)    -> let newacc = (Array.fold_left filtrec acc cl) in
-                          if p oper then ((f oper)::newacc) else newacc
-    | DOPL(oper,cl)    -> let newacc = (List.fold_left filtrec acc cl) in
-                          if p oper then ((f oper)::newacc) else newacc
-    | DLAM(_,c)        -> filtrec acc c
-    | DLAMV(_,v)       -> Array.fold_left filtrec acc v
-    | _                -> acc
-  in 
-  filtrec l constr
 
 (* Returns the list of global variables in a term *)
 
@@ -352,42 +276,6 @@ let global_vars_set constr =
   in 
   filtrec Idset.empty constr
 
-(* alpha equality for generic terms : checks first if M and M' are equal,
-   otherwise checks equality forgetting the name annotation of DLAM and DLAMV*)
-
-let rec eq_term m m' =
-     (m == m') 
-  or (m = m')
-  or (match (m,m') with
-	| (DOP1(oper1,c1),DOP1(oper2,c2)) ->
-            oper1 = oper2 & eq_term c1 c2
-	| (DOP2(oper1,c1,t1),DOP2(oper2,c2,t2)) ->
-            oper1 = oper2 & eq_term c1 c2 & eq_term t1 t2
-	| (DOPN(oper1,cl1),DOPN(oper2,cl2)) ->
-            oper1 = oper2 & array_for_all2 eq_term cl1 cl2
-	| (DOPL(oper1,cl1),DOPL(oper2,cl2)) ->
-            oper1 = oper2 & List.for_all2 eq_term cl1 cl2
-	| (DLAM(_,c1),DLAM(_,c2)) -> eq_term c1 c2
-	| (DLAMV(_,cl1),DLAMV(_,cl2)) -> array_for_all2 eq_term cl1 cl2
-	| _ -> false)
-
-(* (dependent M N) is true iff M is eq_term with a subterm of N 
-   M is appropriately lifted through abstractions of N *)
-let dependent =
-  let rec deprec m = function t ->
-       (eq_term m t)
-    or (match t with
-	  | VAR _       -> false
-	  | DOP1(_,c)   -> deprec m c
-	  | DOP2(_,c,t) -> deprec m c or deprec m t
-	  | DOPN(_,cl)  -> array_exists (deprec m) cl
-	  | DOPL(_,cl)  -> List.exists (deprec m) cl
-	  | DLAM(_,c)   -> deprec (lift1 m) c
-	  | DLAMV(_,v)  -> array_exists (deprec (lift1 m)) v
-	  | _ -> false)
-  in 
-  deprec
-
 (* (thin_val sigma) removes identity substitutions from sigma *)
 
 let rec thin_val = function
@@ -398,6 +286,8 @@ let rec thin_val = function
 
 (* (replace_vars sigma M) applies substitution sigma to term M *)
 let replace_vars var_alist = 
+  let var_alist =
+    List.map (fun (str,c) -> (str,make_substituend c)) var_alist in
   let var_alist = thin_val var_alist in 
   let rec substrec n = function
     | (VAR(x) as c)    ->
@@ -414,54 +304,22 @@ let replace_vars var_alist =
   in 
   if var_alist = [] then (function x -> x) else substrec 0
 
-let subst_varn str n = replace_vars [(str,make_substituend (Rel n))]
+let subst_varn str n = replace_vars [(str, (Rel n))]
 
 (* (subst_var str t) substitute (VAR str) by (Rel 1) in t *)
 let subst_var str = subst_varn str 1
 
+(* [Rel (n+m);...;Rel(n+1)] *)
 
-(* renames different  ocurrences of (VAR id) in t with a fresh identifier
-   wrt. acc *)
-let rename_diff_occ  id acc t =
-  let rec rename_occ acc  = function
-    | (VAR(x)  as c) -> 
-	if x <> id then 
-	  acc,c
-        else 
-	  let nid = next_ident_away id acc in (nid::acc), (VAR nid)
-    | DOPN(oper,cl) -> 
-	let nacc,ncl = vrename_occ acc  cl in nacc,DOPN(oper, ncl)
-    | DOPL(oper,cl) -> 
-	let nacc,ncl = lrename_occ acc cl in nacc, DOPL(oper,ncl)
-    | DOP1(oper,c) ->
-	let nacc,nc = rename_occ acc c in nacc, DOP1(oper,nc)
-    | DOP2(oper,c1,c2) -> 
-	let nacc,nc1 = rename_occ acc c1 in
-        let nacc2,nc2 = rename_occ   nacc c2 in
-        nacc2, DOP2(oper,nc1,nc2) 
-    | DLAM(na,c) -> 
-	let nacc,nc = rename_occ acc c in (nacc, DLAM(na,nc))
-    | DLAMV(na,v) -> 
-	let nacc,nv = vrename_occ acc v in (nacc, DLAMV(na, nv))
-    | x -> acc,x
-  and lrename_occ acc = function
-    | [] -> acc,[]
-    | (t::lt) -> 
-	let nacc,nt = rename_occ acc t in
-        let nacc2,nlt = lrename_occ nacc lt
-        in nacc2,(nt::nlt)
-  and vrename_occ acc v = 
-    let nacc,nl = lrename_occ acc (Array.to_list v)
-    in nacc, Array.of_list nl
-  in 
-  rename_occ acc t
+let rel_vect n m = Array.init m (fun i -> Rel(n+m-i))
 
+let rel_list n m = 
+  let rec reln l p = 
+    if p>m then l else reln (Rel(n+p)::l) (p+1)
+  in 
+  reln [] 1
 
-let sAPP c n =
-  match c with 
-    | DLAM(na,m) -> subst1 n m
-    | _ -> invalid_arg "SAPP"
-	  
+(* Obsolète 
 let sAPPV c n =
   match c with
     | DLAMV(na,mV) -> Array.map (subst1 n) mV
@@ -480,22 +338,6 @@ let sAPPList constr cl =
   in 
   srec [] (constr,cl) 
 
-let sAPPVList constr cl = 
-  let rec srec stack = function
-    | (DLAM(_,c), (h::t)) -> srec (h::stack) (c,t)
-    | (DLAMV(_,c), [h])   -> Array.map (substl (h::stack)) c
-    | (_,             _)  -> failwith "SAPPVList"
-  in 
-  srec [] (constr,cl) 
-
-let sAPPViList i constr cl= 
-  let rec srec stack = function
-    | (DLAM(_,c), (h::t)) -> srec (h::stack) (c,t)
-    | (DLAMV(_,c), [h])   -> substl (h::stack) c.(i)
-    | (_,             _)  -> failwith "SAPPViList"
-  in 
-  srec [] (constr,cl)
-
 let under_dlams f = 
   let rec apprec = function 
     | DLAMV(na,c) -> DLAMV(na,Array.map f c)
@@ -504,19 +346,11 @@ let under_dlams f =
   in 
   apprec 
 
-
 let put_DLAMSV lna lc = 
   match lna with 
     | [] -> anomaly "put_DLAM"
     | na::lrest -> List.fold_left (fun c na -> DLAM(na,c)) (DLAMV(na,lc)) lrest
 
-let put_DLAMSV_subst lid lc = 
-  match lid with
-    | [] -> anomaly "put_DLAM"
-    | id::lrest ->  
-        List.fold_left (fun c id' -> DLAM(Name id',subst_var id' c)) 
-          (DLAMV(Name id,Array.map (subst_var id) lc)) lrest
-
 let rec decomp_DLAMV n = function 
   | DLAM(_,lc)  -> decomp_DLAMV (n-1) lc
   | DLAMV(_,lc) -> if n = 1 then lc else error "decomp_DLAMV 0"
@@ -537,50 +371,4 @@ let decomp_all_DLAMV_name constr =
     | _ -> assert false
   in 
   decomprec [] constr
-  
-
-(* [Rel (n+m);...;Rel(n+1)] *)
-
-let rel_vect n m = Array.init m (fun i -> Rel(n+m-i))
-
-let rel_list n m = 
-  let rec reln l p = 
-    if p>m then l else reln (Rel(n+p)::l) (p+1)
-  in 
-  reln [] 1
-
-let rec count_dlam = function
-  | DLAM (_,c) -> 1 + (count_dlam c)
-  | _ -> 0
-
-(* Hash-consing *)
-let comp_term t1 t2 =
-  match (t1,t2) with
-    | (DOP0 o1, DOP0 o2) -> o1==o2
-    | (DOP1(o1,t1), DOP1(o2,t2)) -> o1==o2 & t1==t2
-    | (DOP2(o1,t1,u1), DOP2(o2,t2,u2)) -> o1==o2 & t1==t2 & u1==u2
-    | (DOPN(o1,v1), DOPN(o2,v2)) ->
-        (o1==o2) & (Array.length v1 = Array.length v2)
-        & array_for_all2 (==) v1 v2
-    | (DOPL(o1,l1), DOPL(o2,l2)) ->
-        (o1==o2) & (List.length l1 = List.length l2)
-        & List.for_all2 (==) l1 l2
-    | (DLAM(x1,t1), DLAM(x2,t2)) -> x1==x2 & t1==t2
-    | (DLAMV(x1,v1), DLAMV(x2,v2)) ->
-        (x1==x2) & (Array.length v1 = Array.length v2)
-        & array_for_all2 (==) v1 v2
-    | (Rel i, Rel j) -> i=j
-    | (VAR x, VAR y) -> x==y
-    | _ -> false
-
-let hash_term (sh_rec,(sh_op,sh_na,sh_id)) t =
-  match t with
-    | DOP0 o -> DOP0 (sh_op o)
-    | DOP1(o,t) -> DOP1(sh_op o, sh_rec t)
-    | DOP2(o,t1,t2) -> DOP2(sh_op o, sh_rec t1, sh_rec t2)
-    | DOPN(o,v) -> DOPN(sh_op o, Array.map sh_rec v)
-    | DOPL(o,l) -> DOPL(sh_op o, List.map sh_rec l)
-    | DLAM(n,t) -> DLAM(sh_na n, sh_rec t)
-    | DLAMV(n,v) -> DLAMV(sh_na n, Array.map sh_rec v)
-    | Rel i -> t
-    | VAR x -> VAR (sh_id x) 
+*)  
diff --git a/kernel/generic.mli b/kernel/generic.mli
index 5f632a94ad..4f2afa9a0f 100644
--- a/kernel/generic.mli
+++ b/kernel/generic.mli
@@ -23,84 +23,91 @@ type 'oper term =
   | VAR of identifier
   | Rel of int
 
-val isRel  : 'a term -> bool
-val isVAR  : 'a term -> bool
 val free_rels : 'a term -> Intset.t
 
-exception FreeVar
-exception Occur
-
-val closedn : int -> 'a term -> unit
+(* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
 val closed0 : 'a term -> bool
-val noccurn : int -> 'a term -> bool
-val noccur_bet : int -> int -> 'a term -> bool
 
-(*s Lifts. [ELSHFT(l,n)] == lift of [n], then apply [lift l].
-  [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *)
+(* [noccurn n M] returns true iff [Rel n] does NOT occur in term [M]  *)
+val noccurn : int -> 'a term -> bool
 
-type lift_spec =
-  | ELID
-  | ELSHFT of lift_spec * int
-  | ELLFT of int * lift_spec
+(* [noccur_between n m M] returns true iff [Rel p] does NOT occur in term [M]
+  for n <= p < n+m *)
+val noccur_between : int -> int -> 'a term -> bool
 
-val el_shft : int -> lift_spec -> lift_spec
-val el_lift : lift_spec -> lift_spec
-val el_liftn :  int -> lift_spec -> lift_spec
-val reloc_rel: int -> lift_spec -> int
-val exliftn : lift_spec -> 'a term -> 'a term
+(* [liftn n k c] lifts by [n] indexes above [k] in [c] *)
 val liftn : int -> int -> 'a term -> 'a term
+
+(* [lift n c] lifts by [n] the positive indexes in [c] *)
 val lift : int -> 'a term -> 'a term
+
+(* [pop c] lifts by -1 the positive indexes in [c] *)
 val pop : 'a term -> 'a term
 
 (* [lift_context n ctxt] lifts terms in [ctxt] by [n] preserving
    (i.e. not lifting) the internal references between terms of [ctxt];
    more recent terms come first in [ctxt] *)
-
 val lift_context : int -> (name * 'a term) list -> (name * 'a term) list
 
-(*s Explicit substitutions of type ['a]. [ESID] = identity. 
+val substnl : 'a term list -> int -> 'a term -> 'a term
+val substl : 'a term list -> 'a term -> 'a term
+val subst1 : 'a term -> 'a term -> 'a term
+
+(* [global_vars c] returns the list of [id]'s occurring as [VAR id] in [c] *)
+val global_vars : 'a term -> identifier list
+
+val global_vars_set : 'a term -> Idset.t
+val subst_var : identifier -> 'a term -> 'a term
+val replace_vars : (identifier * 'a term) list -> 'a term -> 'a term
+
+(* [rel_list n m] and [rel_vect n m] compute [[Rel (n+m);...;Rel(n+1)]] *)
+val rel_vect : int -> int -> 'a term array
+val rel_list : int -> int -> 'a term list
+
+(*i************************************************************************i*)
+(*i Pour Closure *)
+(* Explicit substitutions of type ['a]. [ESID] = identity. 
   [CONS(t,S)] = $S.t$ i.e. parallel substitution. [SHIFT(n,S)] = 
   $(\uparrow n~o~S)$ i.e. terms in S are relocated with n vars. 
   [LIFT(n,S)] = $(\%n~S)$ stands for $((\uparrow n~o~S).n...1)$. *)
-
 type 'a subs =
   | ESID
   | CONS of 'a * 'a subs
   | SHIFT of int * 'a subs
   | LIFT of int * 'a subs
-
 val subs_cons  : 'a * 'a subs -> 'a subs
 val subs_lift  : 'a subs -> 'a subs
 val subs_shft  : int * 'a subs -> 'a subs
-val exp_rel    : int -> int -> 'a subs -> (int * 'a, int) union
 val expand_rel : int -> 'a subs -> (int * 'a, int) union
+(*
+val exp_rel    : int -> int -> 'a subs -> (int * 'a, int) union
+*)
+(*i*)
 
-type info = Closed | Open | Unknown
-type 'a substituend = { mutable sinfo : info; sit : 'a }
+(*i Pour Closure *)
+(*s Lifts. [ELSHFT(l,n)] == lift of [n], then apply [lift l].
+  [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *)
+type lift_spec =
+  | ELID
+  | ELSHFT of lift_spec * int
+  | ELLFT of int * lift_spec
+val el_shft : int -> lift_spec -> lift_spec
+val el_lift : lift_spec -> lift_spec
+val reloc_rel: int -> lift_spec -> int
+(*
+val exliftn : lift_spec -> 'a term -> 'a term
+val el_liftn :  int -> lift_spec -> lift_spec
+*)
+(*i*)
 
-val lift_substituend : int -> 'a term substituend -> 'a term
-val make_substituend : 'a term -> 'a term substituend
-val substn_many : 'a term substituend array -> int -> 'a term -> 'a term
-val substl : 'a term list -> 'a term -> 'a term
-val subst1 : 'a term -> 'a term -> 'a term
-val occur_opern : 'a -> 'a term -> bool
-val occur_oper0 : 'a -> 'a term -> bool
-val occur_var : identifier -> 'a term -> bool
-val occur_oper : 'a -> 'a term -> bool
-val process_opers_of_term : 
-  ('a -> bool) -> ('a -> 'b) -> 'b list -> 'a term -> 'b list
-val dependent : 'a term -> 'a term -> bool
+(*i À virer...
+exception FreeVar
+val closedn : int -> 'a term -> unit
+
+exception Occur
+type info = Closed | Open | Unknown
 val global_varsl : identifier list -> 'a term -> identifier list
-val global_vars : 'a term -> identifier list
-val global_vars_set : 'a term -> Idset.t
-val subst_var : identifier -> 'a term -> 'a term
 val subst_varn : identifier -> int -> 'a term -> 'a term
-val replace_vars : 
-  (identifier * 'a term substituend) list -> 'a term -> 'a term
-
-val rename_diff_occ : 
-  identifier -> identifier list ->'a term -> identifier list * 'a term 
-
 val sAPP : 'a term -> 'a term -> 'a term
 val sAPPV : 'a term -> 'a term -> 'a term array
 val sAPPVi : int -> 'a term -> 'a term -> 'a term
@@ -109,24 +116,17 @@ val sAPPList : 'a term -> 'a term list -> 'a term
 val sAPPVList : 'a term -> 'a term list-> 'a term array
 val sAPPViList : int -> 'a term -> 'a term list -> 'a term
 val under_dlams : ('a term -> 'a term) -> 'a term -> 'a term
-val eq_term : 'a term -> 'a term -> bool
-
 val put_DLAMSV : name list -> 'a term array -> 'a term
 val decomp_DLAMV : int -> 'a term -> 'a term array
 val decomp_DLAMV_name : int -> 'a term -> name list * 'a term array
 val decomp_all_DLAMV_name : 'a term -> name list * 'a term array
 val put_DLAMSV_subst : identifier list -> 'a term array -> 'a term
-
-(* [rel_list n m] and [rel_vect n m] compute [[Rel (n+m);...;Rel(n+1)]] *)
-val rel_vect : int -> int -> 'a term array
-val rel_list : int -> int -> 'a term list
-
 val count_dlam : 'a term -> int
 
-(*s For hash-consing. *)
-
+(*s For hash-consing. (déplacé dans term) *)
 val hash_term :
   ('a term -> 'a term)
   * (('a -> 'a) * (name -> name) * (identifier -> identifier))
   -> 'a term -> 'a term
 val comp_term : 'a term -> 'a term -> bool
+i*)
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 7a929b9fa3..5ec0e01b0b 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -22,7 +22,7 @@ let instantiate_constr ids c args =
   if is_id_inst ids args then
     c
   else
-    replace_vars (List.combine ids (List.map make_substituend args)) c
+    replace_vars (List.combine ids args) c
 
 let instantiate_type ids tty args =
   typed_app (fun c -> instantiate_constr ids c args) tty
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4dfeca8823..85a335ee8e 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -486,12 +486,19 @@ let reducible_mind_case = function
   | DOPN(MutConstruct _,_) | DOPN(CoFix _,_) -> true
   | _  -> false
 
+(*
 let contract_cofix = function
   | DOPN(CoFix(bodynum),bodyvect) ->
       let nbodies = (Array.length bodyvect) -1 in
       let make_Fi j = DOPN(CoFix(j),bodyvect) in
       sAPPViList bodynum (array_last bodyvect) (list_tabulate make_Fi nbodies)
   | _ -> assert false
+*)
+
+let contract_cofix (bodynum,(types,names,bodies as typedbodies)) =
+  let nbodies = Array.length bodies in
+  let make_Fi j = mkCoFix (nbodies-j-1,typedbodies) in
+  substl (list_tabulate make_Fi nbodies) bodies.(bodynum)
 
 let reduce_mind_case mia =
   match mia.mconstr with
@@ -500,19 +507,25 @@ let reduce_mind_case mia =
 	let real_cargs = list_lastn ncargs mia.mcargs in
         applist (mia.mlf.(i-1),real_cargs)
     | DOPN(CoFix _,_) as cofix ->
-	let cofix_def = contract_cofix cofix in
+	let cofix_def = contract_cofix (destCoFix cofix) in
 	mkMutCaseA mia.mci mia.mP (applist(cofix_def,mia.mcargs)) mia.mlf
     | _ -> assert false
 
 (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce
    Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *)
 
+(*
 let contract_fix = function 
   | DOPN(Fix(recindices,bodynum),bodyvect) -> 
       let nbodies = Array.length recindices in
       let make_Fi j = DOPN(Fix(recindices,j),bodyvect) in
       sAPPViList bodynum (array_last bodyvect) (list_tabulate make_Fi nbodies)
   | _ -> assert false
+*)
+let contract_fix ((recindices,bodynum),(types,names,bodies as typedbodies)) =
+  let nbodies = Array.length recindices in
+  let make_Fi j = mkFix ((recindices,nbodies-j-1),typedbodies) in
+  substl (list_tabulate make_Fi nbodies) bodies.(bodynum)
 
 let fix_recarg fix stack =
   match fix with 
@@ -537,7 +550,7 @@ let reduce_fix whfun fix stack =
                let stack' = list_assign stack recargnum (applist recarg') in
 	       (match recarg'hd with
                   | DOPN(MutConstruct _,_) -> 
-		      (true,(contract_fix fix,stack'))
+		      (true,(contract_fix (destFix fix),stack'))
 		  | _ -> (false,(fix,stack'))))
     | _ -> assert false
 
@@ -981,7 +994,7 @@ let instance s c =
 
 let hnf_prod_app env sigma t n =
   match whd_betadeltaiota env sigma t with
-    | DOP2(Prod,_,b) -> sAPP b n
+    | DOP2(Prod,_,DLAM(_,b)) -> subst1 n b
     | _ -> anomaly "hnf_prod_app: Need a product"
 
 let hnf_prod_appvect env sigma t nl = 
@@ -992,7 +1005,7 @@ let hnf_prod_applist env sigma t nl =
 				    
 let hnf_lam_app env sigma t n =
   match whd_betadeltaiota env sigma t with
-    | DOP2(Lambda,_,b) -> sAPP b n
+    | DOP2(Lambda,_,DLAM(_,b)) -> subst1 n b
     | _ -> anomaly "hnf_lam_app: Need an abstraction"
 
 let hnf_lam_appvect env sigma t nl = 
diff --git a/kernel/term.ml b/kernel/term.ml
index 3a58c92665..6b8e094b9a 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -153,7 +153,7 @@ let mkCast t1 t2 =
 (* Constructs the product (x:t1)t2 *)
 let mkProd x t1 t2 = (DOP2 (Prod,t1,(DLAM (x,t2))))
 
-(* non-dependant product t1 -> t2 *)
+(* non-dependent product t1 -> t2 *)
 let mkArrow t1 t2 = mkProd Anonymous t1 t2
 
 (* named product *)
@@ -215,15 +215,14 @@ let mkMutCaseA ci p c ac =
 
 (* Here, we assume the body already constructed *)
 let mkFixDlam recindxs i jtypsarray body =
-  let typsarray = Array.map incast_type jtypsarray in
+  let typsarray = (*Array.map incast_type*) jtypsarray in
   DOPN (Fix (recindxs,i),Array.append typsarray body)
 
-let mkFix recindxs i jtypsarray funnames bodies = 
-  let rec wholebody l = 
-    match l with 
-      | [h]    -> (DLAMV (h,bodies)) 
-      | (x::l) -> (DLAM  (x, wholebody l))
-      | [] -> anomaly "in Term.mkFix : empty list of funnames"
+let mkFix ((recindxs, i), (jtypsarray, funnames, bodies)) = 
+  let rec wholebody = function 
+    | [h]    -> (DLAMV (h,bodies)) 
+    | (x::l) -> (DLAM  (x, wholebody l))
+    | [] -> anomaly "in Term.mkFix : empty list of funnames"
   in 
   mkFixDlam recindxs i jtypsarray [|(wholebody funnames)|]
 
@@ -244,10 +243,10 @@ let mkFix recindxs i jtypsarray funnames bodies =
 *)
 (* Here, we assume the body already constructed *)
 let mkCoFixDlam i jtypsarray body =
-  let typsarray = Array.map incast_type jtypsarray in
+  let typsarray = (*Array.map incast_type*) jtypsarray in
   DOPN ((CoFix i),(Array.append typsarray body))
 
-let mkCoFix i jtypsarray funnames bodies = 
+let mkCoFix (i, (jtypsarray, funnames, bodies)) = 
   let rec wholebody l = 
     match l with 
       | [h]    -> (DLAMV (h,bodies))
@@ -387,6 +386,12 @@ let rec strip_all_casts t =
     | VAR _ as t -> t
     | Rel _ as t -> t
 
+(* Tests if a de Bruijn index *)
+let isRel = function Rel _ -> true | _ -> false
+
+(* Tests if a variable *)
+let isVar = function VAR _ -> true | _ -> false
+
 (* Destructs the product (x:t1)t2 *)
 let destProd = function 
   | DOP2 (Prod, t1, (DLAM (x,t2))) -> (x,t1,t2) 
@@ -525,13 +530,13 @@ let destGralFix a =
 let destFix = function 
   | DOPN (Fix (recindxs,i),a) -> 
       let (types,funnames,bodies) = destGralFix a in 
-      (recindxs,i,Array.map out_fixcast types,funnames,bodies)
+      ((recindxs,i),((*Array.map out_fixcast *) types,funnames,bodies))
   | _ -> invalid_arg "destFix"
 	
 let destCoFix = function 
   | DOPN ((CoFix i),a) ->
       let (types,funnames,bodies) = destGralFix a in
-      (i,Array.map out_fixcast types,funnames,bodies)
+      (i,((*Array.map out_fixcast *) types,funnames,bodies))
   | _ -> invalid_arg "destCoFix"
 
 (* Provisoire, le temps de maitriser les cast *)
@@ -551,7 +556,7 @@ let destUntypedCoFix = function
 
 type binder_kind = BProd | BLambda
 
-type fix_kind = RFix of int array * int | RCofix of int
+type fix_kind = RFix of (int array * int) | RCofix of int
 
 type 'ctxt reference =
   | RConst of section_path * 'ctxt
@@ -565,6 +570,8 @@ type existential = int * constr array
 type constant = section_path * constr array
 type constructor = constructor_path * constr array
 type inductive = inductive_path * constr array
+type fixpoint = (int array * int) * (constr array * name list * constr array)
+type cofixpoint = int * (constr array * name list * constr array)
 
 (******************)
 (* Term analysis  *)
@@ -586,9 +593,8 @@ type kindOfTerm =
   | IsMutInd       of inductive
   | IsMutConstruct of constructor
   | IsMutCase      of case_info * constr * constr * constr array
-  | IsFix          of int array * int * constr array * name list * constr array
-  | IsCoFix        of int * constr array * name list * constr array
-
+  | IsFix          of fixpoint
+  | IsCoFix        of cofixpoint
 
 (* Discriminates which kind of term is it.  
 
@@ -616,11 +622,11 @@ let kind_of_term c =
     | DOPN (MutCase ci,v)                  -> 
 	IsMutCase (ci,v.(0),v.(1),Array.sub v 2 (Array.length v - 2))
     | DOPN ((Fix (recindxs,i),a))           ->  
-      	let (types,funnames,bodies) = destGralFix a in
-	IsFix (recindxs,i,types,funnames,bodies)
+      	let typedbodies = destGralFix a in
+	IsFix ((recindxs,i),typedbodies)
     | DOPN ((CoFix i),a)                    ->  
-      	let (types,funnames,bodies) = destGralFix a in
-      	IsCoFix (i,types,funnames,bodies)
+      	let typedbodies = destGralFix a in
+      	IsCoFix (i,typedbodies)
     | _ -> errorlabstrm "Term.kind_of_term" [< 'sTR "ill-formed constr" >]
 
 (***************************)
@@ -711,7 +717,7 @@ let rec to_prod n lam =
 
 let prod_app t n =
   match strip_outer_cast t with
-    | DOP2(Prod,_,b) -> sAPP b n
+    | DOP2(Prod,_,DLAM(na,b)) -> subst1 n b
     | _ ->
 	errorlabstrm "prod_app"
 	  [< 'sTR"Needed a product, but didn't find one" ; 'fNL >]
@@ -969,7 +975,7 @@ let rec decomp_app c =
     | c -> (c,[])
 
 (* strips head casts and flattens head applications *)
-let strip_head_cast = function
+let rec strip_head_cast = function
   | DOPN(AppL,cl) -> 
       let rec collapse_rec = function
 	| (DOPN(AppL,cl),l2) -> collapse_rec(array_hd cl, array_app_tl cl l2)
@@ -978,11 +984,41 @@ let strip_head_cast = function
 	| (f,l) -> let v = Array.of_list (f::l) in DOPN(AppL,v)
       in 
       collapse_rec(array_hd cl, array_app_tl cl [])
+  | DOP2(Cast,c,t) -> strip_head_cast c
   | c -> c
 
+(* Various occurs checks *)
+
+let occur_opern s = 
+  let rec occur_rec = function
+    | DOPN(oper,cl) -> s=oper or (array_exists occur_rec cl)
+    | DOPL(oper,cl) -> s=oper or (List.exists occur_rec cl)
+    | VAR _         -> false
+    | DOP1(_,c)     -> occur_rec c 
+    | DOP2(_,c1,c2) -> (occur_rec c1) or (occur_rec c2)
+    | DLAM(_,c)     -> occur_rec c
+    | DLAMV(_,v)    -> array_exists occur_rec v
+    | _             -> false
+  in 
+  occur_rec 
+
 (* (occur_const (s:section_path) c) -> true if constant s occurs in c,
  * false otherwise *)
 let occur_const s = occur_opern (Const s)
+let occur_evar ev = occur_opern (Evar ev)
+
+let occur_var s = 
+  let rec occur_rec = function
+    | DOPN(_,cl)    -> array_exists occur_rec cl
+    | DOPL(_,cl)    -> List.exists occur_rec cl
+    | VAR id        -> s=id
+    | DOP1(_,c)     -> occur_rec c 
+    | DOP2(_,c1,c2) -> (occur_rec c1) or (occur_rec c2)
+    | DLAM(_,c)     -> occur_rec c
+    | DLAMV(_,v)    -> array_exists occur_rec v
+    | _             -> false
+  in 
+  occur_rec 
 
 (* let sigma be a finite function mapping sections paths to 
    constants represented as (identifier list * constr) option.
@@ -1010,9 +1046,7 @@ let replace_consts const_alist =
                  if List.length hyps <> Array.length cl then
                    anomaly "found a constant with a bad number of args"
                  else
-      	       	   replace_vars
-      	       	     (List.combine hyps 
-			(array_map_to_list make_substituend cl')) body
+      	       	   replace_vars (List.combine hyps (Array.to_list cl')) body
              | None -> anomaly ("a constant which was never"^
       	       	       		" supposed to appear has just appeared")
 	 with Not_found -> DOPN(Const sp,cl'))
@@ -1048,10 +1082,9 @@ let whd_castapp x = applist(whd_castapp_stack x [])
 
 (* alpha conversion : ignore print names and casts *)
 let rec eq_constr_rec m n = 
+  (m == n) or
   (m = n) or
   match (strip_head_cast m,strip_head_cast n) with
-    | (DOP2(Cast,c1,_),c2) 	       -> eq_constr_rec c1 c2
-    | (c1,DOP2(Cast,c2,_))              -> eq_constr_rec c1 c2
     | (Rel p1,Rel p2)                   -> p1=p2
     | (DOPN(oper1,cl1),DOPN(oper2,cl2)) ->
         oper1=oper2 & array_for_all2 eq_constr_rec cl1 cl2
@@ -1067,10 +1100,9 @@ let rec eq_constr_rec m n =
 let eq_constr = eq_constr_rec
 
 let rec eq_constr_with_meta_rec m n=
+  (m == n) or
   (m=n) or 
   (match (strip_head_cast m,strip_head_cast n) with
-     | (DOP2(Cast,c1,_),c2) 	       -> eq_constr_rec c1 c2
-     | (c1,DOP2(Cast,c2,_))              -> eq_constr_rec c1 c2
      | (Rel p1,Rel p2)                   -> p1=p2
      | (DOPN(oper1,cl1),DOPN(oper2,cl2)) ->
          oper1=oper2 & array_for_all2 eq_constr_rec cl1 cl2
@@ -1083,6 +1115,24 @@ let rec eq_constr_with_meta_rec m n=
       	 array_for_all2 eq_constr_rec cl1 cl2
      | _ -> false)
 
+(* (dependent M N) is true iff M is eq_term with a subterm of N 
+   M is appropriately lifted through abstractions of N *)
+
+let dependent =
+  let rec deprec m t =
+    (eq_constr m t)
+    or (match t with
+	  | VAR _       -> false
+	  | DOP1(_,c)   -> deprec m c
+	  | DOP2(_,c,t) -> deprec m c or deprec m t
+	  | DOPN(_,cl)  -> array_exists (deprec m) cl
+	  | DOPL(_,cl)  -> List.exists (deprec m) cl
+	  | DLAM(_,c)   -> deprec (lift 1 m) c
+	  | DLAMV(_,v)  -> array_exists (deprec (lift 1 m)) v
+	  | _ -> false)
+  in 
+  deprec
+
 (* On reduit une serie d'eta-redex de tete ou rien du tout  *)
 (* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *)
 (* Remplace 2 versions précédentes buggées                  *)
@@ -1330,6 +1380,37 @@ let occur_existential =
 (* hash-consing functions  *)                         
 (***************************)
 
+let comp_term t1 t2 =
+  match (t1,t2) with
+    | (DOP0 o1, DOP0 o2) -> o1==o2
+    | (DOP1(o1,t1), DOP1(o2,t2)) -> o1==o2 & t1==t2
+    | (DOP2(o1,t1,u1), DOP2(o2,t2,u2)) -> o1==o2 & t1==t2 & u1==u2
+    | (DOPN(o1,v1), DOPN(o2,v2)) ->
+        (o1==o2) & (Array.length v1 = Array.length v2)
+        & array_for_all2 (==) v1 v2
+    | (DOPL(o1,l1), DOPL(o2,l2)) ->
+        (o1==o2) & (List.length l1 = List.length l2)
+        & List.for_all2 (==) l1 l2
+    | (DLAM(x1,t1), DLAM(x2,t2)) -> x1==x2 & t1==t2
+    | (DLAMV(x1,v1), DLAMV(x2,v2)) ->
+        (x1==x2) & (Array.length v1 = Array.length v2)
+        & array_for_all2 (==) v1 v2
+    | (Rel i, Rel j) -> i=j
+    | (VAR x, VAR y) -> x==y
+    | _ -> false
+
+let hash_term (sh_rec,(sh_op,sh_na,sh_id)) t =
+  match t with
+    | DOP0 o -> DOP0 (sh_op o)
+    | DOP1(o,t) -> DOP1(sh_op o, sh_rec t)
+    | DOP2(o,t1,t2) -> DOP2(sh_op o, sh_rec t1, sh_rec t2)
+    | DOPN(o,v) -> DOPN(sh_op o, Array.map sh_rec v)
+    | DOPL(o,l) -> DOPL(sh_op o, List.map sh_rec l)
+    | DLAM(n,t) -> DLAM(sh_na n, sh_rec t)
+    | DLAMV(n,v) -> DLAMV(sh_na n, Array.map sh_rec v)
+    | Rel i -> t
+    | VAR x -> VAR (sh_id x) 
+
 module Hsorts =
   Hashcons.Make(
     struct
diff --git a/kernel/term.mli b/kernel/term.mli
index 7320b8be89..cc5a8954d0 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -76,7 +76,7 @@ val outcast_type : constr -> typed_type
 (**********************************************************************)
 type binder_kind = BProd | BLambda
 
-type fix_kind = RFix of int array * int | RCofix of int
+type fix_kind = RFix of (int array * int) | RCofix of int
 
 type 'ctxt reference =
   | RConst of section_path * 'ctxt
@@ -96,6 +96,9 @@ type existential = int * constr array
 type constant = section_path * constr array
 type constructor = constructor_path * constr array
 type inductive = inductive_path * constr array
+type fixpoint = (int array * int) * (constr array * name list * constr array)
+type cofixpoint = int * (constr array * name list * constr array)
+
 
 type kindOfTerm =
   | IsRel          of int
@@ -113,8 +116,8 @@ type kindOfTerm =
   | IsMutInd       of inductive
   | IsMutConstruct of constructor
   | IsMutCase      of case_info * constr * constr * constr array
-  | IsFix          of int array * int * constr array * name list * constr array
-  | IsCoFix        of int * constr array * name list * constr array
+  | IsFix          of fixpoint
+  | IsCoFix        of cofixpoint
 
 (* Discriminates which kind of term is it.  
   Note that there is no cases for [DLAM] and [DLAMV].  These terms do not
@@ -212,7 +215,7 @@ val mkMutCaseA : case_info -> constr -> constr -> constr array -> constr
       [typarray = [|t1,...tn|]]
       [funnames = [f1,.....fn]]
       [bodies   = [b1,.....bn]]
-   then [ mkFix recindxs i typarray funnames bodies]
+   then [ mkFix ((recindxs,i),typarray, funnames, bodies) ]
    constructs the $i$th function of the block  
 
     [Fixpoint f1 [ctx1] = b1
@@ -222,17 +225,15 @@ val mkMutCaseA : case_info -> constr -> constr -> constr array -> constr
 
    \noindent where the lenght of the $j$th context is $ij$.
 *)
-val mkFix : int array -> int -> typed_type array -> name list 
-  -> constr array -> constr
+val mkFix : fixpoint -> constr
 
 (* Similarly, but we assume the body already constructed *)
-val mkFixDlam : int array -> int -> typed_type array
-  -> constr array -> constr 
+val mkFixDlam : int array -> int -> constr array -> constr array -> constr 
 
 (* If [typarray = [|t1,...tn|]]
       [funnames = [f1,.....fn]]
       [bodies   = [b1,.....bn]] \par\noindent
-   then [mkCoFix i typsarray funnames bodies]
+   then [mkCoFix (i, (typsarray, funnames, bodies))]
    constructs the ith function of the block  
    
     [CoFixpoint f1 = b1
@@ -240,11 +241,10 @@ val mkFixDlam : int array -> int -> typed_type array
      ...
      with       fn = bn.]
  *)
-val mkCoFix : int -> typed_type array -> name list 
-  -> constr array -> constr
+val mkCoFix : cofixpoint -> constr
 
 (* Similarly, but we assume the body already constructed *)
-val mkCoFixDlam : int -> typed_type array -> constr array -> constr
+val mkCoFixDlam : int -> constr array -> constr array -> constr
 
 
 (*s Term destructors. 
@@ -292,6 +292,12 @@ val strip_outer_cast : constr -> constr
 (* Special function, which keep the key casts under Fix and MutCase. *)
 val strip_all_casts : constr -> constr
 
+(* Tests if a de Bruijn index *)
+val isRel  : constr -> bool
+
+(* Tests if a variable *)
+val isVar  : constr -> bool
+
 (* Destructs the product $(x:t_1)t_2$ *)
 val destProd : constr -> name * constr * constr
 val hd_of_prod : constr -> constr
@@ -316,7 +322,7 @@ val args_of_const : constr -> constr array
 val destEvar : constr -> int * constr array
 val num_of_evar : constr -> int
 
-(* Destrucy an abstract term *)
+(* Destructs an abstract term *)
 val destAbst : constr -> section_path * constr array
 val path_of_abst : constr -> section_path
 val args_of_abst : constr -> constr array
@@ -343,11 +349,9 @@ val destCase : constr -> case_info * constr * constr * constr array
 *)
 val destGralFix : 
   constr array -> constr array * Names.name list * constr array
-val destFix : constr -> 
-  int array * int * typed_type array * Names.name list * constr array
+val destFix : constr -> fixpoint
 
-val destCoFix : 
-  constr -> int * typed_type array * Names.name list * constr array
+val destCoFix : constr -> cofixpoint
 
 (* Provisoire, le temps de maitriser les cast *)
 val destUntypedFix : 
@@ -534,6 +538,18 @@ val rel_vect : int -> int -> constr array
    in c, [false] otherwise *)
 val occur_const : section_path -> constr -> bool
 
+(* [(occur_evar ev c)] returns [true] if existential variable [ev] occurs 
+   in c, [false] otherwise *)
+val occur_evar : existential_key -> constr -> bool
+
+(* [(occur_var id c)] returns [true] if variable [id] occurs free
+   in c, [false] otherwise *)
+val occur_var : identifier -> 'a term -> bool
+
+(* [dependent M N] is true iff M is eq_constr with a subterm of N 
+   M is appropriately lifted through abstractions of N *)
+val dependent : constr -> constr -> bool
+
 (* strips head casts and flattens head applications *)
 val strip_head_cast : constr -> constr
 val whd_castapp_stack : constr -> constr list -> constr * constr list
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 1a6c1d885f..e227111d0d 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -351,6 +351,7 @@ let apply_rel_list env sigma nocheck argjl funj =
  which may contain the CoFix variables. These occurrences of CoFix variables
  are not considered *)
 
+exception Occur
 let noccur_with_meta n m term = 
   let rec occur_rec n = function
     | Rel p -> if n<=p & p<n+m then raise Occur
@@ -629,30 +630,19 @@ nvect is [|n1;..;nk|] which gives for each recursive definition
 the inductive-decreasing index 
 the function checks the convertibility of ti with Ai *)
 
-let check_fix env sigma = function
-  | DOPN(Fix(nvect,j),vargs) -> 
-      let nbfix = let nv = Array.length vargs in 
-      if nv < 2 then error "Ill-formed recursive definition" else nv-1 in
-      let varit = Array.sub vargs 0 nbfix in
-      let ldef = array_last vargs in
-      let ln = Array.length nvect 
-      and la = Array.length varit in
-      if ln <> la then 
-	error "Ill-formed fix term"
-      else 
-	let (lna,vdefs) = decomp_DLAMV_name ln ldef in 
-	let vlna = Array.of_list lna in
-	let check_type i = 
-	  try
-	    let _ = 
-	      check_subterm_rec_meta env sigma nvect nvect.(i) vdefs.(i) in 
-	    ()
-	  with UserError (s,str) ->
-	    error_ill_formed_rec_body CCI env str lna i vdefs 
-	in
-	for i = 0 to ln-1 do check_type i done 
-
-  | _ -> assert false
+let check_fix env sigma ((nvect,bodynum),(types,names,bodies)) =
+  let nbfix = Array.length bodies in 
+  if nbfix = 0
+    or Array.length nvect <> nbfix 
+    or Array.length types <> nbfix
+    or List.length names <> nbfix
+  then error "Ill-formed fix term";
+  for i = 0 to nbfix - 1 do
+    try
+      let _ = check_subterm_rec_meta env sigma nvect nvect.(i) bodies.(i) in ()
+    with UserError (s,str) ->
+      error_ill_formed_rec_body	CCI env str (List.rev names) i bodies
+  done 
 
 (* Co-fixpoints. *)
 
@@ -733,28 +723,18 @@ let check_guard_rec_meta env sigma nbfix def deftype =
             else 
 	      error "Recursive call in the type of an abstraction"
 	      
-	| (DOPN(CoFix(j),vargs),l) -> 
-          if  (List.for_all (noccur_with_meta n nbfix) l)
-          then 
-            let nbfix = let nv = Array.length vargs in 
-            if nv < 2 then
-              error "Ill-formed recursive definition" 
-            else 
-	      nv-1 
-	    in
-            let varit = Array.sub vargs 0 nbfix in
-            let ldef = array_last vargs in
-            let la = Array.length varit in
-            let (lna,vdefs) = decomp_DLAMV_name la ldef in
-            let vlna = Array.of_list lna 
-            in 
-	    if (array_for_all (noccur_with_meta n nbfix) varit) then
-              (array_for_all (check_rec_call alreadygrd (n+1) vlra) vdefs)
-              &&
-              (List.for_all (check_rec_call alreadygrd (n+1) vlra) l) 
-            else 
-	      error "Recursive call in the type of a declaration"
-	  else error "Unguarded recursive call"
+	| (DOPN(CoFix(j),vargs) as cofix,l) ->
+            if (List.for_all (noccur_with_meta n nbfix) l)
+            then 
+	      let (j,(varit,lna,vdefs)) = destFix cofix in
+              let nbfix = Array.length vdefs in
+	      if (array_for_all (noccur_with_meta n nbfix) varit) then
+		(array_for_all (check_rec_call alreadygrd (n+1) vlra) vdefs)
+		&&
+		(List.for_all (check_rec_call alreadygrd (n+1) vlra) l) 
+              else 
+		error "Recursive call in the type of a declaration"
+	    else error "Unguarded recursive call"
 
 	| (DOPN(MutCase _,_) as mc,l) -> 
             let (_,p,c,vrest) = destCase mc in
@@ -777,6 +757,17 @@ let check_guard_rec_meta env sigma nbfix def deftype =
 (* The  function which checks that the whole block of definitions 
    satisfies the guarded condition *)
 
+let check_cofix env sigma (bodynum,(types,names,bodies)) = 
+  let nbfix = Array.length bodies in 
+  for i = 0 to nbfix-1 do
+    try 
+      let _ = 
+	check_guard_rec_meta env sigma nbfix bodies.(i) types.(i) in 
+      ()
+    with UserError (s,str) -> 
+      error_ill_formed_rec_body CCI env str (List.rev names) i bodies
+  done
+(*
 let check_cofix env sigma f = 
   match f with
     | DOPN(CoFix(j),vargs) -> 
@@ -801,7 +792,7 @@ let check_cofix env sigma f =
 	in
 	for i = 0 to nbfix-1 do check_type i done
     | _ -> assert false
-
+*)
 
 (* Checks the type of a (co)fixpoint.
    Fix and CoFix are typed the same way; only the guard condition differs. *)
@@ -831,10 +822,10 @@ let control_only_guard env sigma =
     | VAR _         -> ()
     | DOP0(_)       -> ()
     | DOPN(CoFix(_),cl) as cofix ->
-	check_cofix env sigma cofix; 
+	check_cofix env sigma (destCoFix cofix); 
 	Array.iter control_rec cl
     | DOPN(Fix(_),cl) as fix  -> 
-	check_fix env sigma fix; 
+	check_fix env sigma (destFix fix); 
         Array.iter control_rec cl
     | DOPN(_,cl)    -> Array.iter control_rec cl
     | DOPL(_,cl)    -> List.iter control_rec cl
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 7ab2404f8c..3d2074c977 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -67,8 +67,8 @@ val apply_rel_list :
   env -> 'a evar_map -> bool -> unsafe_judgment list -> unsafe_judgment
     -> unsafe_judgment * constraints
 
-val check_fix : env -> 'a evar_map -> constr -> unit
-val check_cofix : env -> 'a evar_map -> constr -> unit
+val check_fix : env -> 'a evar_map -> fixpoint -> unit
+val check_cofix : env -> 'a evar_map -> cofixpoint -> unit
 val control_only_guard : env -> 'a evar_map -> constr -> unit
 
 val type_fixpoint : env -> 'a evar_map -> name list -> typed_type array