Passage de la structure DOPN, DOP2, ... Ã une structure exprimant directement les constructions; disparition du type oper mais nouveau type global_reference

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

2 files changed, 1123 insertions, 1332 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index e6c5fa4b51..38e3f5bfe1 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -12,6 +12,7 @@ open Univ
 
 type existential_key = int
 
+(* This defines Cases annotations *)
 type pattern_source = DefaultPat of int | RegularPat
 type case_style = PrintLet | PrintIf | PrintCases
 type case_printing =
@@ -19,38 +20,10 @@ type case_printing =
     * case_style option * pattern_source array
 type case_info = int array * case_printing
 
-type 'a oper = 
-  (* DOP0 *)
-  | Meta of int
-  | Sort of 'a
-  (* DOP2 *)
-  | Cast | Prod | Lambda
-  (* DOPN *)
-  | AppL | Const of section_path
-  | Evar of existential_key
-  | MutInd of inductive_path
-  | MutConstruct of constructor_path
-  | MutCase of case_info
-  | Fix of int array * int
-  | CoFix of int
-
-  | XTRA of string
-      (* an extra slot, for putting in whatever sort of
-         operator we need for whatever sort of application *)
-
 (* Sorts. *)
 
 type contents = Pos | Null
 
-let contents_of_str = function
-  | "Pos" -> Pos
-  | "Null" -> Null
-  | _ -> invalid_arg "contents_of_str"
-
-let str_of_contents = function
-  | Pos -> "Pos"
-  | Null -> "Null"
-
 type sorts =
   | Prop of contents                      (* proposition types *)
   | Type of universe
@@ -63,35 +36,718 @@ let print_sort = function
   | Prop Null -> [< 'sTR "Prop" >]
   | Type _ -> [< 'sTR "Type" >]
 
+
 (********************************************************************)
-(*           Generic syntax of terms with de Bruijn indexes         *)
+(*       Constructions as implemented                               *)
 (********************************************************************)
 
-type constr =
-  | DOP0 of sorts oper                      (* atomic terms *)
-  | DOP1 of sorts oper * constr             (* operator of arity 1 *)
-  | DOP2 of sorts oper * constr * constr    (* operator of arity 2 *)
-  | DOPN of sorts oper * constr array       (* operator of variadic arity *)
-  | DLAM of name * constr                   (* deBruijn binder on one term *)
-  | DLAMV of name * constr array            (* deBruijn binder on many terms *)
-  | CLam of name * constr * constr
-  | CPrd of name * constr * constr
-  | CLet of name * constr * constr * constr
-  | VAR of identifier                       (* named variable *)
-  | Rel of int                              (* variable as deBruijn index *)
-
-and
-  (*
-    typed_type = sorts judge
-  *)
-  typed_type = constr
+(* I would like the internal representation of constr hidden in a
+module but ocaml does not allow then to export Internal.kind_of_term
+as kind_of_term with the same constructors as Internal.kind_of_term !! *)
 
-type flat_arity = (name * constr) list * sorts
+(* What is intended ...
 
-type 'a judge = { body : constr; typ : 'a }
+module type InternalSig = sig
+
+type constr
+type existential = existential_key * 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 kind_of_term =
+  | IsRel          of int
+  | IsMeta         of int
+  | IsVar          of identifier
+  | IsXtra         of string
+  | IsSort         of sorts
+  | IsCast         of constr * constr
+  | IsProd         of name * constr * constr
+  | IsLambda       of name * constr * constr
+  | IsLetIn        of name * constr * constr * constr
+  | IsAppL         of constr * constr array
+  | IsEvar         of existential
+  | IsConst        of constant
+  | IsMutInd       of inductive
+  | IsMutConstruct of constructor
+  | IsMutCase      of case_info * constr * constr * constr array
+  | IsFix          of fixpoint
+  | IsCoFix        of cofixpoint
+
+val mkRel : int -> constr
+val mkMeta : int -> constr
+val mkVar : identifier -> constr
+val mkXtra : string -> constr
+val mkSort : sorts -> constr
+val mkCast : constr * constr -> constr
+val mkProd : name * constr * constr -> constr
+val mkLambda : name * constr * constr -> constr
+val mkLetIn : name * constr * constr * constr -> constr
+val mkAppL : constr * constr array -> constr
+val mkEvar : existential -> constr
+val mkConst : constant -> constr
+val mkMutInd : inductive -> constr
+val mkMutConstruct : constructor -> constr
+val mkMutCase : case_info * constr * constr * constr array -> constr
+val mkFix : fixpoint -> constr
+val mkCoFix : cofixpoint -> constr
+
+val kind_of_term : constr -> kind_of_term
+
+val hcons_term : 
+  (sorts -> sorts) * (section_path -> section_path) *
+  (name -> name) * (identifier -> identifier) * (string -> string)
+  -> constr -> constr
+end
+
+END of intended signature of internal constr 
+*)
+
+(*
+module Internal : InternalSig =
+struct
+*)
+
+type constr = kind_of_term
+
+and existential = existential_key * constr array
+and constant = section_path * constr array
+and constructor = constructor_path * constr array
+and inductive = inductive_path * constr array
+and fixpoint = (int array * int) * (constr array * name list * constr array)
+and cofixpoint = int * (constr array * name list * constr array)
+
+and kind_of_term =
+  | IsRel          of int
+  | IsMeta         of int
+  | IsVar          of identifier
+  | IsXtra         of string
+  | IsSort         of sorts
+  | IsCast         of constr * constr
+  | IsProd         of name * constr * constr
+  | IsLambda       of name * constr * constr
+  | IsLetIn        of name * constr * constr * constr
+  | IsAppL         of constr * constr array
+  | IsEvar         of existential
+  | IsConst        of constant
+  | IsMutInd       of inductive
+  | IsMutConstruct of constructor
+  | IsMutCase      of case_info * constr * constr * constr array
+  | IsFix          of fixpoint
+  | IsCoFix        of cofixpoint
+
+(***************************)
+(* hash-consing functions  *)                         
+(***************************)
+
+let comp_term t1 t2 =
+  match t1, t2 with
+  | IsRel n1, IsRel n2 -> n1 = n2
+  | IsMeta m1, IsMeta m2 -> m1 = m2
+  | IsVar id1, IsVar id2 -> id1 == id2
+  | IsSort s1, IsSort s2 -> s1 == s2
+  | IsXtra s1, IsXtra s2 -> s1 == s2
+  | IsCast (c1,t1), IsCast (c2,t2) -> c1 == c2 & t1 == t2
+  | IsProd (n1,t1,c1), IsProd (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2
+  | IsLambda (n1,t1,c1), IsLambda (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2
+  | IsLetIn (n1,b1,t1,c1), IsLetIn (n2,b2,t2,c2) ->
+      n1 == n2 & b1 == b2 & t1 == t2 & c1 == c2
+  | IsAppL (c1,l1), IsAppL (c2,l2) -> c1 == c2 & array_for_all2 (==) l1 l2
+  | IsEvar (e1,l1), IsEvar (e2,l2) -> e1 = e2 & array_for_all2 (==) l1 l2
+  | IsConst (c1,l1), IsConst (c2,l2) -> c1 == c2 & array_for_all2 (==) l1 l2
+  | IsMutInd (c1,l1), IsMutInd (c2,l2) -> c1 == c2 & array_for_all2 (==) l1 l2
+  | IsMutConstruct (c1,l1), IsMutConstruct (c2,l2) ->
+      c1 == c2 & array_for_all2 (==) l1 l2
+  | IsMutCase (ci1,p1,c1,bl1), IsMutCase (ci2,p2,c2,bl2) ->
+      ci1 == ci2 & p1 == p2 & c1 == c2 & array_for_all2 (==) bl1 bl2
+  | IsFix (ln1,(tl1,lna1,bl1)), IsFix (ln2,(tl2,lna2,bl2)) ->
+      lna1 == lna2 & ln1 = ln2
+      & array_for_all2 (==) tl1 tl2 & array_for_all2 (==) bl1 bl2
+  | IsCoFix(ln1,(tl1,lna1,bl1)), IsCoFix(ln2,(tl2,lna2,bl2)) ->
+      lna1 == lna2 & ln1 = ln2
+      & array_for_all2 (==) tl1 tl2 & array_for_all2 (==) bl1 bl2
+  | _ -> false
+
+let hash_term (sh_rec,(sh_sort,sh_sp,sh_na,sh_id,sh_str)) t =
+  match t with
+  | IsRel _ | IsMeta _ -> t
+  | IsVar x -> IsVar (sh_id x)
+  | IsSort s -> IsSort (sh_sort s)
+  | IsXtra s -> IsXtra (sh_str s)
+  | IsCast (c,t) -> IsCast (sh_rec c, sh_rec t)
+  | IsProd (na,t,c) -> IsProd (sh_na na, sh_rec t, sh_rec c)
+  | IsLambda (na,t,c) -> IsLambda (sh_na na, sh_rec t, sh_rec c)
+  | IsLetIn (na,b,t,c) -> IsLetIn (sh_na na, sh_rec b, sh_rec t, sh_rec c)
+  | IsAppL (c,l) -> IsAppL (sh_rec c, Array.map sh_rec l)
+  | IsEvar (e,l) -> IsEvar (e, Array.map sh_rec l)
+  | IsConst (c,l) -> IsConst (sh_sp c, Array.map sh_rec l)
+  | IsMutInd ((sp,i),l) -> IsMutInd ((sh_sp sp,i), Array.map sh_rec l)
+  | IsMutConstruct (((sp,i),j),l) ->
+      IsMutConstruct (((sh_sp sp,i),j), Array.map sh_rec l)
+  | IsMutCase (ci,p,c,bl) -> (* TO DO: extract ind_sp *)
+      IsMutCase (ci, sh_rec p, sh_rec c, Array.map sh_rec bl)
+  | IsFix (ln,(tl,lna,bl)) ->
+      IsFix (ln,(Array.map sh_rec tl,List.map sh_na lna,Array.map sh_rec bl))
+  | IsCoFix(ln,(tl,lna,bl)) ->
+      IsCoFix (ln,(Array.map sh_rec tl,List.map sh_na lna,Array.map sh_rec bl))
+
+module Hconstr =
+  Hashcons.Make(
+    struct
+      type t = constr
+      type u = (constr -> constr) *
+               ((sorts -> sorts) * (section_path -> section_path)
+		* (name -> name) * (identifier -> identifier)
+		* (string -> string))
+      let hash_sub = hash_term
+      let equal = comp_term
+      let hash = Hashtbl.hash
+    end)
+
+let hcons_term (hsorts,hsp,hname,hident,hstr) =
+  Hashcons.recursive_hcons Hconstr.f (hsorts,hsp,hname,hident,hstr)
+
+(* Constructs a DeBrujin index with number n *)
+let mkRel   n = IsRel n
+
+(* Constructs an existential variable named "?n" *)
+let mkMeta  n =  IsMeta n
+
+(* Constructs a Variable named id *)
+let mkVar id = IsVar id
+
+(* Construct an XTRA term (XTRA is an extra slot for whatever you want) *)
+let mkXtra s = IsXtra s
+
+(* Construct a type *)
+let mkSort s = IsSort s
+(* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *)
+(* (that means t2 is declared as the type of t1) *)
+let mkCast (t1,t2) =
+  match t1 with
+    | IsCast (t,_) -> IsCast (t,t2)
+    | _ -> IsCast (t1,t2)
+
+(* Constructs the product (x:t1)t2 *)
+let mkProd (x,t1,t2) = IsProd (x,t1,t2)
+
+(* Constructs the abstraction [x:t1]t2 *)
+let mkLambda (x,t1,t2) = IsLambda (x,t1,t2)
+
+(* Constructs [x=c_1:t]c_2 *)
+let mkLetIn (x,c1,t,c2) = IsLetIn (x,c1,t,c2)
+
+(* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *)
+(* We ensure applicative terms have at most one arguments and the
+   function is not itself an applicative term *)
+let mkAppL (f, a) = 
+  if a=[||] then f else
+    match f with
+      | IsAppL (g, cl) -> IsAppL (g, Array.append cl a)
+      | _ -> IsAppL (f, a)
+
+
+(* Constructs a constant *) 
+(* The array of terms correspond to the variables introduced in the section *)
+let mkConst c = IsConst c
+
+(* Constructs an existential variable *)
+let mkEvar e = IsEvar e
+
+(* Constructs the ith (co)inductive type of the block named sp *)
+(* The array of terms correspond to the variables introduced in the section *)
+let mkMutInd m = IsMutInd m
+
+(* Constructs the jth constructor of the ith (co)inductive type of the 
+   block named sp. The array of terms correspond to the variables
+   introduced in the section *)
+let mkMutConstruct c = IsMutConstruct c
+
+(* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
+let mkMutCase (ci, p, c, ac) = IsMutCase (ci, p, c, ac)
+
+let mkFix fix = IsFix fix
+
+let mkCoFix cofix = IsCoFix cofix
+
+let kind_of_term c = c
 
 (*
-type typed_term = typed_type judge
+end
+END of expected but not allowed module (second variant) *)
+
+(***********************************************************************)
+(*    kind_of_term = constructions as seen by the user                 *)
+(***********************************************************************)
+
+(*
+type constr = Internal.constr
+type existential = Internal.existential
+type constant = Internal.constant
+type constructor = Internal.constructor
+type inductive = Internal.inductive
+type fixpoint = Internal.fixpoint
+type cofixpoint = Internal.cofixpoint
+
+type kind_of_term = Internal.kindOfTerm
+
+open Internal
+
+END of expected re-export of Internal module *)
+
+(* User view of [constr]. For [IsAppL], it is ensured there is at
+   least one argument and the function is not itself an applicative
+   term *)
+
+let kind_of_term = kind_of_term
+
+
+(* En vue d'un kind_of_type : constr -> hnftype ??? *)
+type hnftype =
+  | HnfSort   of sorts
+  | HnfProd   of name * constr * constr
+  | HnfAtom   of constr
+  | HnfMutInd of inductive * constr array
+
+(***********************************************************************)
+(*   kind of global references                                         *)
+(***********************************************************************)
+
+type global_reference =
+  | ConstRef of section_path
+  | IndRef of inductive_path
+  | ConstructRef of constructor_path
+
+(**********************************************************************)
+(*          Non primitive term destructors                            *)
+(**********************************************************************)
+
+(* Destructor operations : partial functions 
+   Raise invalid_arg "dest*" if the const has not the expected form *)
+
+(* Destructs a DeBrujin index *)
+let destRel c = match kind_of_term c with
+  | IsRel n -> n
+  | _ -> invalid_arg "destRel"
+
+(* Destructs an existential variable *)
+let destMeta c = match kind_of_term c with
+  | IsMeta n -> n
+  | _ -> invalid_arg "destMeta"
+
+let isMeta c = match kind_of_term c with IsMeta _ -> true | _ -> false
+
+(* Destructs a variable *)
+let destVar c = match kind_of_term c with
+  | IsVar id -> id
+  | _ -> invalid_arg "destVar"
+
+(* Destructs an XTRA *)
+let destXtra c = match kind_of_term c with
+  | IsXtra s -> s
+  | _ -> invalid_arg "destXtra"
+
+(* Destructs a type *)
+let isSort c = match kind_of_term c with
+  | IsSort s -> true
+  | _ -> false
+
+let destSort c = match kind_of_term c with
+  | IsSort s -> s
+  | _ -> invalid_arg "destSort"
+
+let rec isprop c = match kind_of_term c with
+  | IsSort (Prop _) -> true
+  | IsCast (c,_) -> isprop c
+  | _ -> false
+
+let rec is_Prop c = match kind_of_term c with
+  | IsSort (Prop Null) -> true
+  | IsCast (c,_) -> is_Prop c
+  | _ -> false
+
+let rec is_Set c = match kind_of_term c with
+  | IsSort (Prop Pos) -> true
+  | IsCast (c,_) -> is_Set c
+  | _ -> false
+
+let rec is_Type c = match kind_of_term c with
+  | IsSort (Type _) -> true
+  | IsCast (c,_) -> is_Type c
+  | _ -> false
+
+let isType = function
+  | Type _ -> true
+  | _ -> false
+
+let is_small = function
+  | Prop _ -> true
+  | _ -> false
+
+let iskind c = isprop c or is_Type c
+
+let same_kind c1 c2 = (isprop c1 & isprop c2) or (is_Type c1 & is_Type c2)
+
+(* Destructs a casted term *)
+let destCast c = match kind_of_term c with 
+  | IsCast (t1, t2) -> (t1,t2)
+  | _ -> invalid_arg "destCast"
+
+let isCast c = match kind_of_term c with IsCast (_,_) -> true | _ -> false
+
+(* Tests if a de Bruijn index *)
+let isRel c = match kind_of_term c with IsRel _ -> true | _ -> false
+
+(* Tests if a variable *)
+let isVar c = match kind_of_term c with IsVar _ -> true | _ -> false
+
+(* Destructs the product (x:t1)t2 *)
+let destProd c = match kind_of_term c with 
+  | IsProd (x,t1,t2) -> (x,t1,t2) 
+  | _ -> invalid_arg "destProd"
+
+(* Destructs the abstraction [x:t1]t2 *)
+let destLambda c = match kind_of_term c with 
+  | IsLambda (x,t1,t2) -> (x,t1,t2) 
+  | _ -> invalid_arg "destLambda"
+
+(* Destructs the let [x:=b:t1]t2 *)
+let destLetIn c = match kind_of_term c with 
+  | IsLetIn (x,b,t1,t2) -> (x,b,t1,t2) 
+  | _ -> invalid_arg "destProd"
+
+(* Destructs an application *)
+let destApplication c = match kind_of_term c with
+  | IsAppL (f,a) -> (f, a)
+  | _ -> invalid_arg "destApplication"
+
+let isAppL c = match kind_of_term c with IsAppL _ -> true | _ -> false
+
+(* Destructs a constant *)
+let destConst c = match kind_of_term c with
+  | IsConst (sp, a as r) -> r
+  | _ -> invalid_arg "destConst"
+
+let path_of_const c = match kind_of_term c with
+  | IsConst (sp,_) -> sp
+  | _ -> anomaly "path_of_const called with bad args"
+
+let args_of_const c = match kind_of_term c with
+  | IsConst (_,args) -> args
+  | _ -> anomaly "args_of_const called with bad args"
+
+let isConst c = match kind_of_term c with IsConst _ -> true | _ -> false
+
+(* Destructs an existential variable *)
+let destEvar c = match kind_of_term c with
+  | IsEvar (sp, a as r) -> r
+  | _ -> invalid_arg "destEvar"
+
+let num_of_evar c = match kind_of_term c with
+  | IsEvar (n, _) -> n
+  | _ -> anomaly "num_of_evar called with bad args"
+
+(* Destructs a (co)inductive type named sp *)
+let destMutInd c = match kind_of_term c with
+  | IsMutInd (sp, a as r) -> r
+  | _ -> invalid_arg "destMutInd"
+	
+let op_of_mind c = match kind_of_term c with
+  | IsMutInd (ind_sp,_) -> ind_sp
+  | _ -> anomaly "op_of_mind called with bad args"
+
+let args_of_mind c = match kind_of_term c with
+  | IsMutInd (_,args) -> args
+  | _ -> anomaly "args_of_mind called with bad args"
+
+(* Destructs a constructor *)
+let destMutConstruct c = match kind_of_term c with
+  | IsMutConstruct (sp, a as r) -> r
+  | _ -> invalid_arg "dest"
+
+let op_of_mconstr c = match kind_of_term c with
+  | IsMutConstruct (sp,_) -> sp
+  | _ -> anomaly "op_of_mconstr called with bad args"
+
+let args_of_mconstr c = match kind_of_term c with
+  | IsMutConstruct (_,args) -> args
+  | _ -> anomaly "args_of_mconstr called with bad args"
+
+let isMutConstruct c = match kind_of_term c with
+    IsMutCase _ -> true | _ -> false
+
+(* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
+let destCase c = match kind_of_term c with
+  | IsMutCase (ci,p,c,v) -> (ci,p,c,v)
+  | _ -> anomaly "destCase"
+
+let destFix c = match kind_of_term c with 
+  | IsFix ((recindxs,i),(types,funnames,bodies) as fix) -> fix
+  | _ -> invalid_arg "destFix"
+	
+let destCoFix c = match kind_of_term c with 
+  | IsCoFix (i,(types,funnames,bodies) as cofix) -> cofix
+  | _ -> invalid_arg "destCoFix"
+
+(****************************************************************************)
+(*              Functions to recur through subterms                         *)
+(****************************************************************************)
+
+(* [fold_constr f acc c] folds [f] on the immediate subterms of [c]
+   starting from [acc] and proceeding from left to right according to
+   the usual representation of the constructions; it is not recursive *)
+
+let fold_constr f acc c = match kind_of_term c with
+  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> acc
+  | IsCast (c,t) -> f (f acc c) t
+  | IsProd (_,t,c) -> f (f acc t) c
+  | IsLambda (_,t,c) -> f (f acc t) c
+  | IsLetIn (_,b,t,c) -> f (f (f acc b) t) c
+  | IsAppL (c,l) -> Array.fold_left f (f acc c) l
+  | IsEvar (_,l) -> Array.fold_left f acc l
+  | IsConst (_,l) -> Array.fold_left f acc l
+  | IsMutInd (_,l) -> Array.fold_left f acc l
+  | IsMutConstruct (_,l) -> Array.fold_left f acc l
+  | IsMutCase (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
+  | IsFix (_,(tl,_,bl)) ->
+      array_fold_left2 (fun acc b t -> f (f acc b) t) acc bl tl
+  | IsCoFix (_,(tl,_,bl)) ->
+      array_fold_left2 (fun acc b t -> f (f acc b) t) acc bl tl
+
+(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
+   subterms of [c] starting from [acc] and proceeding from left to
+   right according to the usual representation of the constructions as
+   [fold_constr] but it carries an extra data [n] (typically a lift
+   index) which is processed by [g] (which typically add 1 to [n]) at
+   each binder traversal; it is not recursive *)
+
+let fold_constr_with_binders g f n acc c = match kind_of_term c with
+  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> acc
+  | IsCast (c,t) -> f n (f n acc c) t
+  | IsProd (_,t,c) -> f (g n) (f n acc t) c
+  | IsLambda (_,t,c) -> f (g n) (f n acc t) c
+  | IsLetIn (_,b,t,c) -> f (g n) (f n (f n acc b) t) c
+  | IsAppL (c,l) -> Array.fold_left (f n) (f n acc c) l
+  | IsEvar (_,l) -> Array.fold_left (f n) acc l
+  | IsConst (_,l) -> Array.fold_left (f n) acc l
+  | IsMutInd (_,l) -> Array.fold_left (f n) acc l
+  | IsMutConstruct (_,l) -> Array.fold_left (f n) acc l
+  | IsMutCase (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
+  | IsFix (_,(tl,_,bl)) -> 
+      let n' = iterate g (Array.length tl) n in
+      array_fold_left2 (fun acc b t -> f n (f n' acc b) t) acc bl tl
+  | IsCoFix (_,(tl,_,bl)) ->
+      let n' = iterate g (Array.length tl) n in
+      array_fold_left2 (fun acc b t -> f n (f n' acc b) t) acc bl tl
+
+(* [iter_constr f c] iters [f] on the immediate subterms of [c]; it is
+   not recursive and the order with which subterms are processed is
+   not specified *)
+
+let iter_constr f c = match kind_of_term c with
+  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> ()
+  | IsCast (c,t) -> f c; f t
+  | IsProd (_,t,c) -> f t; f c
+  | IsLambda (_,t,c) -> f t; f c
+  | IsLetIn (_,b,t,c) -> f b; f t; f c
+  | IsAppL (c,l) -> f c; Array.iter f l
+  | IsEvar (_,l) -> Array.iter f l
+  | IsConst (_,l) -> Array.iter f l
+  | IsMutInd (_,l) -> Array.iter f l
+  | IsMutConstruct (_,l) -> Array.iter f l
+  | IsMutCase (_,p,c,bl) -> f p; f c; Array.iter f bl
+  | IsFix (_,(tl,_,bl)) -> Array.iter f tl; Array.iter f bl
+  | IsCoFix (_,(tl,_,bl)) -> Array.iter f tl; Array.iter f bl
+
+(* [iter_constr_with_binders g f n c] iters [f n] on the immediate
+   subterms of [c]; it carries an extra data [n] (typically a lift
+   index) which is processed by [g] (which typically add 1 to [n]) at
+   each binder traversal; it is not recursive and the order with which
+   subterms are processed is not specified *)
+
+let iter_constr_with_binders g f n c = match kind_of_term c with
+  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> ()
+  | IsCast (c,t) -> f n c; f n t
+  | IsProd (_,t,c) -> f n t; f (g n) c
+  | IsLambda (_,t,c) -> f n t; f (g n) c
+  | IsLetIn (_,b,t,c) -> f n b; f n t; f (g n) c
+  | IsAppL (c,l) -> f n c; Array.iter (f n) l
+  | IsEvar (_,l) -> Array.iter (f n) l
+  | IsConst (_,l) -> Array.iter (f n) l
+  | IsMutInd (_,l) -> Array.iter (f n) l
+  | IsMutConstruct (_,l) -> Array.iter (f n) l
+  | IsMutCase (_,p,c,bl) -> f n p; f n c; Array.iter (f n) bl
+  | IsFix (_,(tl,_,bl)) -> 
+      Array.iter (f n) tl; Array.iter (f (iterate g (Array.length tl) n)) bl
+  | IsCoFix (_,(tl,_,bl)) ->
+      Array.iter (f n) tl; Array.iter (f (iterate g (Array.length tl) n)) bl
+
+(* [map_constr f c] maps [f] on the immediate subterms of [c]; it is
+   not recursive and the order with which subterms are processed is
+   not specified *)
+
+let map_constr f c = match kind_of_term c with
+  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> c
+  | IsCast (c,t) -> mkCast (f c, f t)
+  | IsProd (na,t,c) -> mkProd (na, f t, f c)
+  | IsLambda (na,t,c) -> mkLambda (na, f t, f c)
+  | IsLetIn (na,b,t,c) -> mkLetIn (na, f b, f t, f c)
+  | IsAppL (c,l) -> mkAppL (f c, Array.map f l)
+  | IsEvar (e,l) -> mkEvar (e, Array.map f l)
+  | IsConst (c,l) -> mkConst (c, Array.map f l)
+  | IsMutInd (c,l) -> mkMutInd (c, Array.map f l)
+  | IsMutConstruct (c,l) -> mkMutConstruct (c, Array.map f l)
+  | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f p, f c, Array.map f bl)
+  | IsFix (ln,(tl,lna,bl)) -> mkFix (ln,(Array.map f tl,lna,Array.map f bl))
+  | IsCoFix(ln,(tl,lna,bl)) -> mkCoFix (ln,(Array.map f tl,lna,Array.map f bl))
+
+(* [map_constr_with_binders g f n c] maps [f n] on the immediate
+   subterms of [c]; it carries an extra data [n] (typically a lift
+   index) which is processed by [g] (which typically add 1 to [n]) at
+   each binder traversal; it is not recursive and the order with which
+   subterms are processed is not specified *)
+
+let map_constr_with_binders g f l c = match kind_of_term c with
+  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> c
+  | IsCast (c,t) -> mkCast (f l c, f l t)
+  | IsProd (na,t,c) -> mkProd (na, f l t, f (g l) c)
+  | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g l) c)
+  | IsLetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g l) c)
+  | IsAppL (c,al) -> mkAppL (f l c, Array.map (f l) al)
+  | IsEvar (e,al) -> mkEvar (e, Array.map (f l) al)
+  | IsConst (c,al) -> mkConst (c, Array.map (f l) al)
+  | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al)
+  | IsMutConstruct (c,al) -> mkMutConstruct (c, Array.map (f l) al)
+  | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f l p, f l c, Array.map (f l) bl)
+  | IsFix (ln,(tl,lna,bl)) ->
+      let l' = iterate g (Array.length tl) l in
+      mkFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl))
+  | IsCoFix(ln,(tl,lna,bl)) ->
+      let l' = iterate g (Array.length tl) l in
+      mkCoFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl))
+
+(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
+   subterms of [c]; it carries an extra data [l] (typically a name
+   list) which is processed by [g na] (which typically cons [na] to
+   [l]) at each binder traversal (with name [na]); it is not recursive
+   and the order with which subterms are processed is not specified *)
+
+let map_constr_with_named_binders g f l c = match kind_of_term c with
+  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> c
+  | IsCast (c,t) -> mkCast (f l c, f l t)
+  | IsProd (na,t,c) -> mkProd (na, f l t, f (g na l) c)
+  | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c)
+  | IsLetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c)
+  | IsAppL (c,al) -> mkAppL (f l c, Array.map (f l) al)
+  | IsEvar (e,al) -> mkEvar (e, Array.map (f l) al)
+  | IsConst (c,al) -> mkConst (c, Array.map (f l) al)
+  | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al)
+  | IsMutConstruct (c,al) -> mkMutConstruct (c, Array.map (f l) al)
+  | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f l p, f l c, Array.map (f l) bl)
+  | IsFix (ln,(tl,lna,bl)) ->
+      let l' = List.fold_right g lna l in
+      mkFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl))
+  | IsCoFix(ln,(tl,lna,bl)) ->
+      let l' = List.fold_right g lna l in
+      mkCoFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl))
+
+(* [map_constr_with_binders_left_to_right g f n c] maps [f n] on the
+   immediate subterms of [c]; it carries an extra data [n] (typically
+   a lift index) which is processed by [g] (which typically add 1 to
+   [n]) at each binder traversal; the subterms are processed from left
+   to right according to the usual representation of the constructions
+   (this may matter if [f] does a side-effect); it is not recursive;
+   in fact, the usual representation of the constructions is at the
+   time being almost those of the ML representation (except for
+   (co-)fixpoint) *)
+
+(* Ocaml does not guarantee Array.map is LR (even if so), then we rewrite it *)
+let array_map_left f a =
+  let l = Array.length a in
+  if l = 0 then [||] else begin
+    let r = Array.create l (f a.(0)) in
+    for i = 1 to l - 1 do
+      r.(i) <- f a.(i)
+    done;
+    r
+  end
+
+let array_map_left_pair f a g b =
+  let l = Array.length a in
+  if l = 0 then [||],[||] else begin
+    let r = Array.create l (f a.(0)) in
+    let s = Array.create l (g b.(0)) in
+    for i = 1 to l - 1 do
+      r.(i) <- f a.(i);
+      s.(i) <- g b.(i)
+    done;
+    r, s
+  end
+
+let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
+  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> c
+  | IsCast (c,t) -> let c' = f l c in mkCast (c', f l t)
+  | IsProd (na,t,c) -> let t' = f l t in mkProd (na, t', f (g l) c)
+  | IsLambda (na,t,c) -> let t' = f l t in mkLambda (na, t', f (g l) c)
+  | IsLetIn (na,b,t,c) ->
+      let b' = f l b in let t' = f l t in mkLetIn (na, b', t', f (g l) c)
+  | IsAppL (c,al) -> 
+      let c' = f l c in mkAppL (c', array_map_left (f l) al)
+  | IsEvar (e,al) -> mkEvar (e, array_map_left (f l) al)
+  | IsConst (c,al) -> mkConst (c, array_map_left (f l) al)
+  | IsMutInd (c,al) -> mkMutInd (c, array_map_left (f l) al)
+  | IsMutConstruct (c,al) -> mkMutConstruct (c, array_map_left (f l) al)
+  | IsMutCase (ci,p,c,bl) ->
+      let p' = f l p in let c' = f l c in
+      mkMutCase (ci, p', c', array_map_left (f l) bl)
+  | IsFix (ln,(tl,lna,bl)) ->
+      let l' = iterate g (Array.length tl) l in
+      let tl', bl' = array_map_left_pair (f l) tl (f l') bl in
+      mkFix (ln,(tl',lna,bl'))
+  | IsCoFix(ln,(tl,lna,bl)) ->
+      let l' = iterate g (Array.length tl) l in
+      let tl', bl' = array_map_left_pair (f l) tl (f l') bl in
+      mkCoFix (ln,(tl',lna,bl'))
+
+(* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare
+   the immediate subterms of [c1] of [c2] if needed; Cast's, binders
+   name and Cases annotations are not taken into account *)
+
+let compare_constr f c1 c2 =
+  match kind_of_term c1, kind_of_term c2 with
+  | IsRel n1, IsRel n2 -> n1 = n2
+  | IsMeta m1, IsMeta m2 -> m1 = m2
+  | IsVar id1, IsVar id2 -> id1 = id2
+  | IsSort s1, IsSort s2 -> s1 = s2
+  | IsXtra s1, IsXtra s2 -> s1 = s2
+  | IsCast (c1,_), _ -> f c1 c2
+  | _, IsCast (c2,_) -> f c1 c2
+  | IsProd (_,t1,c1), IsProd (_,t2,c2) -> f t1 t2 & f c1 c2
+  | IsLambda (_,t1,c1), IsLambda (_,t2,c2) -> f t1 t2 & f c1 c2
+  | IsLetIn (_,b1,t1,c1), IsLetIn (_,b2,t2,c2) -> f b1 b2 & f t1 t2 & f c1 c2
+  | IsAppL (c1,l1), IsAppL (c2,l2) -> f c1 c2 & array_for_all2 f l1 l2
+  | IsEvar (e1,l1), IsEvar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2
+  | IsConst (c1,l1), IsConst (c2,l2) -> c1 = c2 & array_for_all2 f l1 l2
+  | IsMutInd (c1,l1), IsMutInd (c2,l2) -> c1 = c2 & array_for_all2 f l1 l2
+  | IsMutConstruct (c1,l1), IsMutConstruct (c2,l2) ->
+      c1 = c2 & array_for_all2 f l1 l2
+  | IsMutCase (_,p1,c1,bl1), IsMutCase (_,p2,c2,bl2) ->
+      f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2
+  | IsFix (ln1,(tl1,_,bl1)), IsFix (ln2,(tl2,_,bl2)) ->
+      ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2
+  | IsCoFix(ln1,(tl1,_,bl1)), IsCoFix(ln2,(tl2,_,bl2)) ->
+      ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2
+  | _ -> false
+
+(***************************************************************************)
+(*     Type of assumptions                                                 *)
+(***************************************************************************)
+
+(*
+type 'a judge = { body : constr; typ : 'a }
+type typed_type = sorts judge
 
 let make_typed t s = { body = t; typ = s }
 let make_typed_lazy t f = { body = t; typ = f s }
@@ -101,16 +757,16 @@ let typed_app f tt = { body = f tt.body; typ = tt.typ }
 let body_of_type ty = ty.body
 let level_of_type t = (t.typ : sorts)
 
-let incast_type tty = DOP2 (Cast, tty.body, (DOP0 (Sort tty.typ)))
+let incast_type tty = mkCast (tty.body, mkSort tty.typ)
 
-let outcast_type = function
-   DOP2 (Cast, b, DOP0 (Sort s)) -> {body=b; typ=s}
+let outcast_type c = kind_of_term c with
+  | IsCast (b, s) when isSort s -> {body=b; typ=destSort s}
   | _ -> anomaly "outcast_type: Not an in-casted type judgement"
 
 let typed_combine f g t u = { f t.body u.body ; g t.typ u.typ}
 *)
 
-type typed_term = typed_type judge
+type typed_type = constr
 
 let make_typed t s = t
 let make_typed_lazy t f = t
@@ -128,6 +784,8 @@ let typed_combine f g t u = f t u
 type var_declaration = identifier * constr option * typed_type
 type rel_declaration = name * constr option * typed_type
 
+
+
 (****************************************************************************)
 (*              Functions for dealing with constr terms                     *)
 (****************************************************************************)
@@ -143,18 +801,9 @@ exception Occur
    occurs in M, returns () otherwise *)
 
 let closedn = 
-  let rec closed_rec n = function
-    | Rel(m)        -> if m>n then raise FreeVar
-    | VAR _         -> ()
-    | DOPN(_,cl)    -> Array.iter (closed_rec n) cl
-    | DOP2(_,c1,c2) -> closed_rec n c1; closed_rec n c2
-    | DOP1(_,c)     -> closed_rec n c
-    | DLAM(_,c)     -> closed_rec (n+1) c
-    | DLAMV(_,v)    -> Array.iter (closed_rec (n+1)) v
-    | CLam (_,t,c)   -> closed_rec n t; closed_rec (n+1) c
-    | CPrd (_,t,c)   -> closed_rec n t; closed_rec (n+1) c
-    | CLet (_,b,t,c) -> closed_rec n b; closed_rec n t; closed_rec (n+1) c
-    | _             -> ()
+  let rec closed_rec n c = match kind_of_term c with
+    | IsRel m -> if m>n then raise FreeVar
+    | _ -> iter_constr_with_binders succ closed_rec n c
   in 
   closed_rec
 
@@ -166,36 +815,18 @@ let closed0 term =
 (* returns the list of free debruijn indices in a term *)
 
 let free_rels m = 
-  let rec frec depth acc = function
-    | Rel n         -> if n >= depth then Intset.add (n-depth+1) acc else acc
-    | DOPN(_,cl)    -> Array.fold_left (frec depth) acc cl
-    | DOP2(_,c1,c2) -> frec depth (frec depth acc c1) c2
-    | DOP1(_,c)     -> frec depth acc c
-    | DLAM(_,c)     -> frec (depth+1) acc c
-    | DLAMV(_,cl)   -> Array.fold_left (frec (depth+1)) acc cl
-    | CLam (_,t,c)   -> frec (depth+1) (frec depth acc t) c
-    | CPrd (_,t,c)   -> frec (depth+1) (frec depth acc t) c
-    | CLet (_,b,t,c) -> frec (depth+1) (frec depth (frec depth acc b) t) c
-    | VAR _         -> acc
-    | DOP0 _        -> acc
+  let rec frec depth acc c = match kind_of_term c with
+    | IsRel n       -> if n >= depth then Intset.add (n-depth+1) acc else acc
+    | _ -> fold_constr_with_binders succ frec depth acc c
   in 
   frec 1 Intset.empty m
 
 (* (noccurn n M) returns true iff (Rel n) does NOT occur in term M  *)
 
 let noccurn n term = 
-  let rec occur_rec n = function
-    | Rel(m)        -> if m = n then raise Occur
-    | VAR _         -> ()
-    | DOPN(_,cl)    -> Array.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 t; occur_rec (n+1) c
-    | CPrd (_,t,c)   -> occur_rec n t; occur_rec (n+1) c
-    | CLet (_,b,t,c) -> occur_rec n b; occur_rec n t; occur_rec (n+1) c
-    | _             -> ()
+  let rec occur_rec n c = match kind_of_term c with
+    | IsRel m -> if m = n then raise Occur
+    | _ -> iter_constr_with_binders succ occur_rec n c
   in 
   try occur_rec n term; true with Occur -> false
 
@@ -203,18 +834,9 @@ let noccurn n term =
   for n <= p < n+m *)
 
 let noccur_between n m term = 
-  let rec occur_rec n = function
-    | Rel(p)        -> if n<=p && p<n+m then raise Occur
-    | VAR _         -> ()
-    | DOPN(_,cl)    -> Array.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 t; occur_rec (n+1) c
-    | CPrd (_,t,c)   -> occur_rec n t; occur_rec (n+1) c
-    | CLet (_,b,t,c) -> occur_rec n b; occur_rec n t; occur_rec (n+1) c
-    | _             -> ()
+  let rec occur_rec n c = match kind_of_term c with
+    | IsRel(p) -> if n<=p && p<n+m then raise Occur
+    | _        -> iter_constr_with_binders succ occur_rec n c
   in 
   try occur_rec n term; true with Occur -> false
 
@@ -226,25 +848,16 @@ let noccur_between n m term =
  are not considered *)
 
 let noccur_with_meta n m term = 
-  let rec occur_rec n = function
-    | Rel p -> if n<=p & p<n+m then raise Occur
-    | VAR _ -> ()
-    | DOPN(AppL,cl) ->
-	(match cl.(0) with
-           | DOP2 (Cast,DOP0 (Meta _),_) -> ()
-           | DOP0 (Meta _) -> ()
-	   | _ -> Array.iter (occur_rec n) cl)
-    | DOPN(Evar _, _) -> ()
-    | DOPN(op,cl) -> Array.iter (occur_rec n) cl
-    | DOP0(_) -> ()
-    | 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 t; occur_rec (n+1) c
-    | CPrd (_,t,c)   -> occur_rec n t; occur_rec (n+1) c
-    | CLet (_,b,t,c) -> occur_rec n b; occur_rec n t; occur_rec (n+1) c
-  in 
+  let rec occur_rec n c = match kind_of_term c with
+    | IsRel p -> if n<=p & p<n+m then raise Occur
+    | IsAppL(f,cl) ->
+	(match kind_of_term f with
+           | IsCast (c,_) when isMeta c -> ()
+           | IsMeta _ -> ()
+	   | _ -> iter_constr_with_binders succ occur_rec n c)
+    | IsEvar (_, _) -> ()
+    | _ -> iter_constr_with_binders succ occur_rec n c
+  in
   try (occur_rec n term; true) with Occur -> false
 
 
@@ -282,17 +895,9 @@ let rec reloc_rel n = function
 
 
 (* The generic lifting function *)
-let rec exliftn el = function
-  | Rel i            -> Rel(reloc_rel i el)
-  | DOPN(oper,cl)    -> DOPN(oper, Array.map (exliftn el) cl)
-  | DOP1(oper,c)     -> DOP1(oper, exliftn el c)
-  | DOP2(oper,c1,c2) -> DOP2(oper, exliftn el c1, exliftn el c2)
-  | DLAM(na,c)       -> DLAM(na, exliftn (el_lift el) c)
-  | DLAMV(na,v)      -> DLAMV(na, Array.map (exliftn (el_lift el)) v)
-  | CLam (n,t,c)   -> CLam (n, exliftn el t, exliftn (el_lift el) c)  
-  | CPrd (n,t,c)   -> CPrd (n, exliftn el t, exliftn (el_lift el) c)
-  | CLet (n,b,t,c) -> CLet (n,exliftn el b,exliftn el t,exliftn (el_lift el) c)
-  | x                -> x
+let rec exliftn el c = match kind_of_term c with
+  | IsRel i -> mkRel(reloc_rel i el)
+  | _ -> map_constr_with_binders el_lift exliftn el c
 
 (* Lifting the binding depth across k bindings *)
 
@@ -334,25 +939,15 @@ let make_substituend c = { sinfo=Unknown; sit=c }
 
 let substn_many lamv n =
   let lv = Array.length lamv in 
-  let rec substrec depth = function 
-    | Rel k as x     ->
+  let rec substrec depth c = match kind_of_term c with
+    | IsRel k     ->
         if k<=depth then 
-	  x
+	  c
         else if k-depth <= lv then
           lift_substituend depth lamv.(k-depth-1)
         else 
-	  Rel (k-lv)
-    | VAR id           -> VAR id
-    | DOPN(oper,cl)    -> DOPN(oper,Array.map (substrec depth) cl)
-    | DOP1(oper,c)     -> DOP1(oper,substrec depth c)
-    | DOP2(oper,c1,c2) -> DOP2(oper,substrec depth c1,substrec depth c2)
-    | DLAM(na,c)       -> DLAM(na,substrec (depth+1) c)
-    | DLAMV(na,v)      -> DLAMV(na,Array.map (substrec (depth+1)) v)
-    | CLam (n,t,c)   -> CLam (n, substrec depth t, substrec (depth+1) c)  
-    | CPrd (n,t,c)   -> CPrd (n, substrec depth t, substrec (depth+1) c)
-    | CLet (n,b,t,c) -> CLet (n, substrec depth b, substrec depth t, 
-			      substrec (depth+1) c)
-    | x                -> x
+	  mkRel (k-lv)
+    | _ -> map_constr_with_binders succ substrec depth c
   in 
   substrec n
 
@@ -366,8 +961,8 @@ let subst1 lam = substl [lam]
 
 let rec thin_val = function
   | [] -> []
-  | (((id,{sit=VAR id'}) as s)::tl) -> 
-      if id = id' then thin_val tl else s::(thin_val tl)
+  | (((id,{ sit = v }) as s)::tl) when isVar v -> 
+      if id = destVar v then thin_val tl else s::(thin_val tl)
   | h::tl -> h::(thin_val tl)
 
 (* (replace_vars sigma M) applies substitution sigma to term M *)
@@ -375,30 +970,21 @@ 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)    ->
+  let rec substrec n c = match kind_of_term c with
+    | IsVar x ->
         (try lift_substituend n (List.assoc x var_alist)
          with Not_found -> c)
-	
-    | DOPN(oper,cl)    -> DOPN(oper,Array.map (substrec n) cl)
-    | DOP1(oper,c)     -> DOP1(oper,substrec n c)
-    | DOP2(oper,c1,c2) -> DOP2(oper,substrec n c1,substrec n c2)
-    | DLAM(na,c)       -> DLAM(na,substrec (n+1) c)
-    | DLAMV(na,v)      -> DLAMV(na,Array.map (substrec (n+1)) v)
-    | CLam (na,t,c)     -> CLam (na, substrec n t, substrec (n+1) c)  
-    | CPrd (na,t,c)     -> CPrd (na, substrec n t, substrec (n+1) c)
-    | CLet (na,b,t,c)   -> CLet (na,substrec n b,substrec n t,substrec (n+1) c)
-    | x                -> x
+    | _ -> map_constr_with_binders succ substrec n c
   in 
   if var_alist = [] then (function x -> x) else substrec 0
 
 (* (subst_var str t) substitute (VAR str) by (Rel 1) in t *)
-let subst_var str = replace_vars [(str, Rel 1)]
+let subst_var str = replace_vars [(str, mkRel 1)]
 
 (* (subst_vars [id1;...;idn] t) substitute (VAR idj) by (Rel j) in t *)
 let subst_vars vars =
   let _,subst =
-    List.fold_left (fun (n,l) var -> ((n+1),(var,Rel n)::l)) (1,[]) vars
+    List.fold_left (fun (n,l) var -> ((n+1),(var,mkRel n)::l)) (1,[]) vars
   in replace_vars (List.rev subst)
 
 (*********************)
@@ -406,22 +992,22 @@ let subst_vars vars =
 (*********************)
 
 (* Constructs a DeBrujin index with number n *)
-let mkRel   n = (Rel n)
+let mkRel = mkRel
 
 (* Constructs an existential variable named "?n" *)
-let mkMeta  n =  DOP0 (Meta n)
+let mkMeta = mkMeta
 
 (* Constructs a Variable named id *)
-let mkVar id = VAR id
+let mkVar = mkVar
 
 (* Construct an XTRA term (XTRA is an extra slot for whatever you want) *)
-let mkXtra s = (DOP0 (XTRA s))
+let mkXtra = mkXtra
 
 (* Construct a type *)
-let mkSort s = DOP0 (Sort s)
-let mkProp   = DOP0 (Sort mk_Prop)
-let mkSet    = DOP0 (Sort mk_Set)
-let mkType u = DOP0 (Sort (Type u))
+let mkSort   = mkSort
+let mkProp   = mkSort mk_Prop
+let mkSet    = mkSort mk_Set
+let mkType u = mkSort (Type u)
 
 let prop = Prop Null
 and spec = Prop Pos
@@ -429,33 +1015,22 @@ and types = Type dummy_univ
 and type_0 = Type prop_univ
 and type_1 = Type prop_univ_univ
 
-(* Construct an implicit (see implicit arguments in the RefMan) *)
-(* let mkImplicit = DOP0 Implicit*)
-
-let implicit_univ = make_path ["Implicit"] (id_of_string "dummy") OBJ
-let implicit_sort = Type { u_sp = implicit_univ ; u_num = 0}
-let mkImplicit = DOP0 (Sort implicit_sort)
-
-
 (* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *)
 (* (that means t2 is declared as the type of t1) *)
-let mkCast (t1,t2) =
-  match t1 with
-    | DOP2(Cast,t,_) -> DOP2(Cast,t,t2)
-    | _ -> (DOP2 (Cast,t1,t2))
+let mkCast = mkCast
 
 (* Constructs the product (x:t1)t2 *)
-let mkProd (x,t1,t2) = CPrd (x,t1,t2)
+let mkProd = mkProd
 let mkNamedProd id typ c = mkProd (Name id, typ, subst_var id c)
 let mkProd_string   s t c = mkProd (Name (id_of_string s), t, c)
 
 (* Constructs the abstraction [x:t1]t2 *)
-let mkLambda (x,t1,t2) = CLam (x,t1,t2)
+let mkLambda = mkLambda
 let mkNamedLambda id typ c = mkLambda (Name id, typ, subst_var id c)
 let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
 
 (* Constructs [x=c_1:t]c_2 *)
-let mkLetIn (x,c1,t,c2) = CLet (x,c1,t,c2)
+let mkLetIn = mkLetIn
 let mkNamedLetIn id c1 t c2 = mkLetIn (Name id, c1, t, subst_var id c2)
 
 (* Constructs either [(x:t)c] or [[x=b:t]c] *)
@@ -495,36 +1070,42 @@ let mkNamedProd_wo_LetIn (id,body,t) c =
 let mkArrow t1 t2 = mkProd (Anonymous, t1, t2)
 
 (* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *)
-let mkAppL (f, a) = DOPN (AppL, Array.append [|f|] a)
-let mkAppList l = DOPN (AppL, Array.of_list l)
-let mkAppA v = DOPN (AppL, v)
+(* We ensure applicative terms have at most one arguments and the
+   function is not itself an applicative term *)
+let mkAppL = mkAppL
+
+let mkAppList = function
+  | f::l -> mkAppL (f, Array.of_list l)
+  | _ -> anomaly "mkAppList received an empty list"
+
+let mkAppA v =
+  let l = Array.length v in
+  if l=0 then anomaly "mkAppA received an empty array"
+  else mkAppL (v.(0), Array.sub v 1 (Array.length v -1))
 
 (* Constructs a constant *) 
 (* The array of terms correspond to the variables introduced in the section *)
-let mkConst (sp,a) = DOPN (Const  sp, a)
+let mkConst = mkConst
 
 (* Constructs an existential variable *)
-let mkEvar (n,a) = DOPN (Evar n, a)
+let mkEvar = mkEvar
 
 (* Constructs the ith (co)inductive type of the block named sp *)
 (* The array of terms correspond to the variables introduced in the section *)
-let mkMutInd (ind_sp,l) = DOPN (MutInd ind_sp, l)
+let mkMutInd = mkMutInd
 
 (* Constructs the jth constructor of the ith (co)inductive type of the 
    block named sp. The array of terms correspond to the variables
    introduced in the section *)
-let mkMutConstruct (cstr_sp,l) =  DOPN (MutConstruct cstr_sp,l)
+let mkMutConstruct = mkMutConstruct
 
 (* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
-let mkMutCaseL (ci, p, c, ac) = 
-  DOPN (MutCase ci, Array.append [|p;c|] (Array.of_list ac))
-let mkMutCase (ci, p, c, ac) = 
-  DOPN (MutCase ci, Array.append [|p;c|] ac)
+let mkMutCase = mkMutCase
+let mkMutCaseL (ci, p, c, ac) = mkMutCase (ci, p, c, Array.of_list ac)
 
 (* If recindxs = [|i1,...in|] 
       typarray = [|t1,...tn|]
       funnames = [f1,.....fn]
-      bodies   = [b1,.....bn]
    then    
 
       mkFix recindxs i typarray funnames bodies
@@ -539,18 +1120,7 @@ let mkMutCase (ci, p, c, ac) =
    where the lenght of the jth context is ij.
 *)
 
-(* Here, we assume the body already constructed *)
-let mkFixDlam recindxs i jtypsarray body =
-  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 = 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)|]
+let mkFix = mkFix
 
 (* If typarray = [|t1,...tn|]
       funnames = [f1,.....fn]
@@ -565,379 +1135,27 @@ let mkFix ((recindxs, i), (jtypsarray, funnames, bodies)) =
     with       f2 = b2
     ...
     with       fn = bn.
-
 *)
-(* Here, we assume the body already constructed *)
-let mkCoFixDlam i jtypsarray body =
-  let typsarray = (*Array.map incast_type*) jtypsarray in
-  DOPN ((CoFix i),(Array.append typsarray body))
-
-let mkCoFix (i, (jtypsarray, funnames, bodies)) = 
-  let rec wholebody l = 
-    match l with 
-      | [h]    -> (DLAMV (h,bodies))
-      | (x::l) -> (DLAM  (x, wholebody l))
-      | [] -> anomaly "in Term.mkCoFix : empty list of funnames"
-  in 
-  mkCoFixDlam i jtypsarray [|(wholebody funnames)|]
-
-(********************)
-(* Term destructors *)
-(********************)
-
-(* Destructor operations : partial functions 
-   Raise invalid_arg "dest*" if the const has not the expected form *)
-
-(* Destructs a DeBrujin index *)
-let destRel = function
-  | (Rel n) -> n
-  | _ -> invalid_arg "destRel"
-
-(* Destructs an existential variable *)
-let destMeta = function
-  | (DOP0 (Meta n)) -> n
-  | _ -> invalid_arg "destMeta"
-
-
-(* Destructs a variable *)
-let destVar = function
-  | (VAR id) -> id
-  | _ -> invalid_arg "destVar"
-
-(* Destructs an XTRA *)
-let destXtra = function
-  | DOP0 (XTRA s) -> s
-  | _ -> invalid_arg "destXtra"
-
-(* Destructs a type *)
-let isSort = function
-  | (DOP0 (Sort s)) -> true
-  | _ -> false
-
-let destSort = function
-  | (DOP0 (Sort s)) -> s
-  | _ -> invalid_arg "destSort"
-
-let rec isprop = function
-  | DOP0(Sort(Prop _)) -> true
-  | DOP2(Cast,c,_) -> isprop c
-  | _ -> false
-
-let rec is_Prop = function
-  | DOP0(Sort(Prop Null)) -> true
-  | DOP2(Cast,c,_) -> is_Prop c
-  | _ -> false
-
-let rec is_Set = function
-  | DOP0(Sort(Prop Pos)) -> true
-  | DOP2(Cast,c,_) -> is_Set c
-  | _ -> false
-
-let rec is_Type = function
-  | DOP0(Sort(Type _)) -> true
-  | DOP2(Cast,c,_) -> is_Type c
-  | _ -> false
-
-let isType = function
-  | Type _ -> true
-  | _ -> false
-
-let is_small = function
-  | Prop _ -> true
-  | _ -> false
-
-let iskind c = isprop c or is_Type c
-
-let is_existential_oper = function
-  | Evar _ -> true
-  | _ -> false
-
-let same_kind c1 c2 = (isprop c1 & isprop c2) or (is_Type c1 & is_Type c2)
-
-let rec contents_of_kind = function
-  | DOP0(Sort(Prop cts)) -> cts
-  | DOP0(Sort(Type _)) -> Pos
-  | DOP2(Cast,c,t) -> contents_of_kind c
-  | _ -> invalid_arg "contents_of_kind"
-
-(* Destructs a casted term *)
-let destCast = function 
-  | DOP2 (Cast, t1, t2) -> (t1,t2)
-  | _ -> invalid_arg "destCast"
-
-let isCast = function DOP2(Cast,_,_) -> true | _ -> false
-
-let rec strip_outer_cast = function
-  | DOP2(Cast,c,_) -> strip_outer_cast c
-  | c -> c
+let mkCoFix = mkCoFix
 
+(* Construct an implicit *)
+let implicit_univ = make_path ["Implicit"] (id_of_string "dummy") OBJ
+let implicit_sort = Type { u_sp = implicit_univ ; u_num = 0}
+let mkImplicit = mkSort implicit_sort
 
+let rec strip_outer_cast c = match kind_of_term c with
+  | IsCast (c,_) -> strip_outer_cast c
+  | _ -> c
 
 (* Fonction spéciale qui laisse les cast clés sous les Fix ou les MutCase *)
 
-let under_outer_cast f = function
-  | DOP2 (Cast,b,t) -> DOP2 (Cast,f b,f t)
-  | c -> f c
-
-let rec under_casts f = function
-  | DOP2 (Cast,c,t) -> DOP2 (Cast,under_casts f c, t)
-  | c               -> f c
-
-let rec strip_all_casts t = 
-  match t with
-    | DOP2 (Cast, b, _) -> strip_all_casts b
-    | DOP0 _ as t -> t
-    (* Cas ad hoc *)
-    | DOPN(Fix _ as f,v) -> 
-	let n = Array.length v in
-	let ts = Array.sub v 0 (n-1) in
-	let b = v.(n-1) in 
-	DOPN(f, Array.append 
-	       (Array.map strip_all_casts ts)
-	       [|under_outer_cast strip_all_casts b|])
-    | DOPN(CoFix _ as f,v) -> 
-	let n = Array.length v in
-	let ts = Array.sub v 0 (n-1) in
-	let b = v.(n-1) in 
-	DOPN(f, Array.append 
-	       (Array.map strip_all_casts ts)
-	       [|under_outer_cast strip_all_casts b|])
-    | DOP1(oper,c) -> DOP1(oper,strip_all_casts c)
-    | DOP2(oper,c1,c2) -> DOP2(oper,strip_all_casts c1,strip_all_casts c2)
-    | DOPN(oper,cl) -> DOPN(oper,Array.map strip_all_casts cl)
-    | DLAM(na,c) -> DLAM(na,strip_all_casts c)
-    | DLAMV(na,c) -> DLAMV(na,Array.map (under_outer_cast strip_all_casts) c)
-    | CLam (n,t,c)   -> CLam (n, strip_all_casts t, strip_all_casts c)  
-    | CPrd (n,t,c)   -> CPrd (n, strip_all_casts t, strip_all_casts c)
-    | CLet (n,b,t,c) -> CLet (n, strip_all_casts b, strip_all_casts t,
-			      strip_all_casts c)
-    | 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 
-  | CPrd (x,t1,t2) -> (x,t1,t2) 
-  | _ -> invalid_arg "destProd"
-
-let rec hd_of_prod prod =
-  match strip_outer_cast prod with
-    | CPrd (n,c,t') -> hd_of_prod t'
-    | t -> t
-
-let hd_is_constructor t  =  
-  let is_constructor =  function
-    | DOPN(MutConstruct((sp,tyi),i),cl)-> true 
-    | _ ->false
-  in
-  match t with 
-    | DOPN(AppL,v) -> is_constructor v.(0)
-    | c -> is_constructor c
-
-(* Destructs the abstraction [x:t1]t2 *)
-let destLambda = function 
-  | CLam (x,t1,t2) -> (x,t1,t2) 
-  | _ -> invalid_arg "destLambda"
-
-(* Destructs the let [x:=b:t1]t2 *)
-let destLetIn = function 
-  | CLet (x,b,t1,t2) -> (x,b,t1,t2) 
-  | _ -> invalid_arg "destProd"
-
-(* Destructs an application *)
-let destAppL = function 
-  | (DOPN (AppL,a)) -> a
-  | _ -> invalid_arg "destAppL"
-
-let destApplication =  function
-  | (DOPN (AppL,a)) when Array.length a <> 0 -> (a.(0), array_tl a)
-  | _ -> invalid_arg "destApplication"
-
-let args_app  = function
-  | DOPN(AppL,cl) -> if Array.length cl >1  then array_tl cl else [||]
-  | c -> [||]
-
-let hd_app  = function
-  | DOPN(AppL,cl) -> cl.(0)
-  | c -> c
-
-(* Destructs a constant *)
-let destConst = function
-  | DOPN (Const sp, a) -> (sp, a)
-  | _ -> invalid_arg "destConst"
-
-let path_of_const = function
-  | DOPN (Const sp,_) -> sp
-  | _ -> anomaly "path_of_const called with bad args"
-
-let args_of_const = function
-  | DOPN (Const _,args) -> args
-  | _ -> anomaly "args_of_const called with bad args"
-
-(* Destructs an existential variable *)
-let destEvar = function
-  | DOPN (Evar n, a) -> (n,a)
-  | _ -> invalid_arg "destEvar"
-
-let num_of_evar = function
-  | DOPN (Evar n, _) -> n
-  | _ -> anomaly "num_of_evar called with bad args"
-
-(* Destructs a (co)inductive type named sp *)
-let destMutInd = function
-  | DOPN (MutInd ind_sp, l) -> (ind_sp,l)
-  | _ -> invalid_arg "destMutInd"
-	
-let op_of_mind = function
-  | DOPN(MutInd ind_sp,_) -> ind_sp
-  | _ -> anomaly "op_of_mind called with bad args"
-
-let args_of_mind = function
-  | DOPN(MutInd _,args) -> args
-  | _ -> anomaly "args_of_mind called with bad args"
-
-(* Destructs a constructor *)
-let destMutConstruct = function
-  | DOPN (MutConstruct cstr_sp,l) -> (cstr_sp,l)
-  | _ -> invalid_arg "dest"
-
-let op_of_mconstr = function
-  | DOPN(MutConstruct (spi,c),_) -> (spi,c)
-  | _ -> anomaly "op_of_mconstr called with bad args"
-
-let args_of_mconstr = function
-  | DOPN(MutConstruct _,args) -> args
-  | _ -> anomaly "args_of_mconstr called with bad args"
-
-(* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
-let destCase = function
-  | DOPN (MutCase ci,v) -> (ci,v.(0),v.(1),Array.sub v 2 (Array.length v - 2))
-  | _ -> anomaly "destCase"
-
-(* Destructs the ith function of the block  
-    Fixpoint f1 [ctx1] = b1
-    with     f2 [ctx2] = b2
-    ...
-    with     fn [ctxn] = bn.
-
-   where the lenght of the jth context is ij.
-*)
-
-let destGralFix a =
-  let nbofdefs = Array.length a in
-  let types    = Array.sub a 0 (nbofdefs-1) in
-  let dlambody = a.(nbofdefs-1) in 
-  let rec destbody l c = 
-    match c with 
-      | DLAMV (h,bodies) -> (List.rev (h::l), bodies) 
-      | DLAM  (x,t)      -> destbody (x::l) t 
-      | _ -> invalid_arg "destGralFix" 
-  in 
-  let funnames,bodies = destbody [] dlambody in 
-  (types,funnames,bodies)
-
-let destFix = function 
-  | DOPN (Fix (recindxs,i),a) -> 
-      let (types,funnames,bodies) = destGralFix a in 
-      ((recindxs,i),(types,funnames,bodies))
-  | _ -> invalid_arg "destFix"
-	
-let destCoFix = function 
-  | DOPN ((CoFix i),a) ->
-      let (types,funnames,bodies) = destGralFix a in
-      (i,(types,funnames,bodies))
-  | _ -> invalid_arg "destCoFix"
-
-(**********************************************************************)
-
-type binder_kind = BProd | BLambda | BLetIn
-
-type fix_kind = RFix of (int array * int) | RCoFix of int
+let under_outer_cast f c =  match kind_of_term c with
+  | IsCast (b,t) -> mkCast (f b,f t)
+  | _ -> f c
 
-type 'ctxt reference =
-  | RConst of section_path * 'ctxt
-  | RInd of inductive_path * 'ctxt
-  | RConstruct of constructor_path * 'ctxt
-  | RVar of identifier
-  | REVar of int * 'ctxt
-
-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  *)
-(******************)
-
-type hnftype =
-  | HnfSort   of sorts
-  | HnfProd   of name * constr * constr
-  | HnfAtom   of constr
-  | HnfMutInd of inductive * constr array
-
-type kindOfTerm = 
-  | IsRel          of int
-  | IsMeta         of int
-  | IsVar          of identifier
-  | IsXtra         of string
-  | IsSort         of sorts
-  | IsCast         of constr * constr
-  | IsProd         of name * constr * constr
-  | IsLambda       of name * constr * constr
-  | IsLetIn        of name * constr * constr * constr
-  | IsAppL         of constr * constr array
-  | IsEvar         of existential
-  | IsConst        of constant
-  | IsMutInd       of inductive
-  | IsMutConstruct of constructor
-  | IsMutCase      of case_info * constr * constr * 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
-   make sense alone, but they must be preceeded by the application of
-   an operator. *)
-
-let kind_of_term c = 
-  match c with
-    | Rel n                                -> IsRel n
-    | VAR id                               -> IsVar id 
-    | DOP0 (Meta n)                        -> IsMeta n
-    | DOP0 (Sort s)                        -> IsSort s
-    | DOP0 (XTRA s)                        -> IsXtra s
-    | DOP2 (Cast, t1, t2)                  -> IsCast (t1,t2)
-    | CPrd (x,t1,t2)                       -> IsProd (x,t1,t2) 
-    | CLam (x,t1,t2)                       -> IsLambda (x,t1,t2)
-    | CLet (x,b,t1,t2)                     -> IsLetIn (x,b,t1,t2)
-    | DOPN (AppL,a) when Array.length a <> 0 -> IsAppL (a.(0), array_tl a)
-    | DOPN (Const sp, a)                   -> IsConst (sp,a)
-    | DOPN (Evar sp, a)                    -> IsEvar (sp,a)
-    | DOPN (MutInd ind_sp, l)              -> IsMutInd (ind_sp,l)
-    | DOPN (MutConstruct cstr_sp,l)        -> IsMutConstruct (cstr_sp,l)
-    | DOPN (MutCase ci,v)                  -> 
-	IsMutCase (ci,v.(0),v.(1),Array.sub v 2 (Array.length v - 2))
-    | DOPN ((Fix (recindxs,i),a))           ->  
-      	let typedbodies = destGralFix a in
-	IsFix ((recindxs,i),typedbodies)
-    | DOPN ((CoFix i),a)                    ->  
-      	let typedbodies = destGralFix a in
-      	IsCoFix (i,typedbodies)
-    | _ -> errorlabstrm "Term.kind_of_term" [< 'sTR "ill-formed constr" >]
-
-let isMeta = function DOP0(Meta _) -> true | _ -> false
-let isConst = function DOPN(Const _,_) -> true | _ -> false
-let isMutConstruct = function DOPN(MutCase _,_) -> true | _ -> false
-let isAppL = function DOPN(AppL,_) -> true | _ -> false
+let rec under_casts f c = match kind_of_term c with
+  | IsCast (c,t) -> mkCast (under_casts f c, t)
+  | _            -> f c
 
 (***************************)
 (* Other term constructors *)
@@ -958,7 +1176,7 @@ let lam_it = List.fold_left (fun c (n,t)  -> mkLambda (n, t, c))
 let prodn n env b =
   let rec prodrec = function
     | (0, env, b)        -> b
-    | (n, ((v,t)::l), b) -> prodrec (n-1,  l, CPrd (v,t,b))
+    | (n, ((v,t)::l), b) -> prodrec (n-1,  l, mkProd (v,t,b))
     | _ -> assert false
   in 
   prodrec (n,env,b)
@@ -967,34 +1185,18 @@ let prodn n env b =
 let lamn n env b =
   let rec lamrec = function
     | (0, env, b)        -> b
-    | (n, ((v,t)::l), b) -> lamrec (n-1,  l, CLam (v,t,b))
+    | (n, ((v,t)::l), b) -> lamrec (n-1,  l, mkLambda (v,t,b))
     | _ -> assert false
   in 
   lamrec (n,env,b)
 
-let rec applist = function
-  | (f,[]) -> f
-  | (DOPN(AppL,cl),l2) -> 
-      let c = array_hd cl in 
-       if isAppL c then 
-	 applist(c,array_app_tl cl l2)
-       else 
-	 DOPN(AppL,Array.append cl (Array.of_list l2))
-  | (f,l) -> DOPN(AppL,Array.of_list(f::l))
-
-and applistc f l = applist(f,l)
-
-let rec appvect = function
-  | (f, [||]) -> f
-  | (DOPN(AppL,cl), v) ->
-      let c = array_hd cl in 
-      if isAppL c then
-	appvect (c, Array.append (array_tl cl) v)
-      else 
-	DOPN(AppL, Array.append cl v)
-  | (f,v) -> DOPN(AppL, array_cons f v)
+let applist (f,l) = mkAppL (f, Array.of_list l)
+
+let applistc f l = mkAppL (f, Array.of_list l)
+
+let appvect = mkAppL
 	    
-and appvectc f l = appvect (f,l)
+let appvectc f l = mkAppL (f,l)
 		     
 (* to_lambda n (x1:T1)...(xn:Tn)(xn+1:Tn+1)...(xn+j:Tn+j)T =
  * [x1:T1]...[xn:Tn](xn+1:Tn+1)...(xn+j:Tn+j)T *)
@@ -1002,18 +1204,18 @@ let rec to_lambda n prod =
   if n = 0 then 
     prod 
   else 
-    match prod with 
-      | CPrd(na,ty,bd) -> CLam(na,ty,to_lambda (n-1) bd)
-      | DOP2(Cast,c,_) -> to_lambda n c
+    match kind_of_term prod with 
+      | IsProd (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd)
+      | IsCast (c,_) -> to_lambda n c
       | _   -> errorlabstrm "to_lambda" [<>]                      
 
 let rec to_prod n lam =
   if n=0 then 
     lam
   else   
-    match lam with 
-      | CLam(na,ty,bd) -> CPrd(na,ty,to_prod (n-1) bd)
-      | DOP2(Cast,c,_) -> to_prod n c
+    match kind_of_term lam with 
+      | IsLambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd)
+      | IsCast (c,_) -> to_prod n c
       | _   -> errorlabstrm "to_prod" [<>]                      
 	    
 (* pseudo-reduction rule:
@@ -1021,8 +1223,8 @@ let rec to_prod n lam =
  * with an strip_outer_cast on the first argument to produce a product *)
 
 let prod_app t n =
-  match strip_outer_cast t with
-    | CPrd (_,_,b) -> subst1 n b
+  match kind_of_term (strip_outer_cast t) with
+    | IsProd (_,_,b) -> subst1 n b
     | _ ->
 	errorlabstrm "prod_app"
 	  [< 'sTR"Needed a product, but didn't find one" ; 'fNL >]
@@ -1039,6 +1241,8 @@ let prod_applist t nL = List.fold_left prod_app t nL
 (* Other term destructors        *)
 (*********************************)
 
+type flat_arity = (name * constr) list * sorts
+
 (* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
    ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
 let destArity = 
@@ -1061,20 +1265,26 @@ let rec isArity c =
 (* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
    ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
 let decompose_prod = 
-  let rec prodec_rec l = function
-    | CPrd(x,t,c)    -> prodec_rec ((x,t)::l) c
-    | DOP2(Cast,c,_) -> prodec_rec l c
-    | c              -> l,c
+  let rec prodec_rec l c = match kind_of_term c with
+    | IsProd (x,t,c) -> prodec_rec ((x,t)::l) c
+    | IsCast (c,_)   -> prodec_rec l c
+    | _              -> l,c
   in 
   prodec_rec []
 
+let rec hd_of_prod prod =
+  match kind_of_term prod with
+    | IsProd (n,c,t') -> hd_of_prod t'
+    | IsCast (c,_) -> hd_of_prod c
+    | _ -> prod
+
 (* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair
    ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)
 let decompose_lam = 
-  let rec lamdec_rec l = function
-    | CLam (x,t,c)    -> lamdec_rec ((x,t)::l) c
-    | DOP2 (Cast,c,_) -> lamdec_rec l c
-    | c              -> l,c
+  let rec lamdec_rec l c = match kind_of_term c with
+    | IsLambda (x,t,c) -> lamdec_rec ((x,t)::l) c
+    | IsCast (c,_)     -> lamdec_rec l c
+    | _                -> l,c
   in 
   lamdec_rec []
 
@@ -1084,10 +1294,10 @@ let decompose_prod_n n =
   if n < 0 then error "decompose_prod_n: integer parameter must be positive";
   let rec prodec_rec l n c = 
     if n=0 then l,c 
-    else match c with 
-      | CPrd (x,t,c)    -> prodec_rec ((x,t)::l) (n-1) c
-      | DOP2 (Cast,c,_) -> prodec_rec l n c
-      | c -> error "decompose_prod_n: not enough products"
+    else match kind_of_term c with 
+      | IsProd (x,t,c) -> prodec_rec ((x,t)::l) (n-1) c
+      | IsCast (c,_)   -> prodec_rec l n c
+      | _ -> error "decompose_prod_n: not enough products"
   in 
   prodec_rec [] n 
 
@@ -1097,28 +1307,28 @@ let decompose_lam_n n =
   if n < 0 then error "decompose_lam_n: integer parameter must be positive";
   let rec lamdec_rec l n c = 
     if n=0 then l,c 
-    else match c with 
-      | CLam (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c
-      | DOP2 (Cast,c,_)           -> lamdec_rec l n c
-      | c -> error "decompose_lam_n: not enough abstractions"
+    else match kind_of_term c with 
+      | IsLambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c
+      | IsCast (c,_)     -> lamdec_rec l n c
+      | _ -> error "decompose_lam_n: not enough abstractions"
   in 
   lamdec_rec [] n 
 
 (* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
  * gives n (casts are ignored) *)
 let nb_lam = 
-  let rec nbrec n = function
-    | CLam (_,_,c) -> nbrec (n+1) c
-    | DOP2(Cast,c,_) -> nbrec n c
+  let rec nbrec n c = match kind_of_term c with
+    | IsLambda (_,_,c) -> nbrec (n+1) c
+    | IsCast (c,_) -> nbrec n c
     | _ -> n
   in 
   nbrec 0
     
 (* similar to nb_lam, but gives the number of products instead *)
 let nb_prod = 
-  let rec nbrec n = function
-    | CPrd (_,_,c) -> nbrec (n+1) c
-    | DOP2(Cast,c,_) -> nbrec n c
+  let rec nbrec n c = match kind_of_term c with
+    | IsProd (_,_,c) -> nbrec (n+1) c
+    | IsCast (c,_) -> nbrec n c
     | _ -> n
   in 
   nbrec 0
@@ -1138,89 +1348,57 @@ let le_kind_implicit k1 k2 =
 (* Flattening and unflattening of embedded applications and casts *)
 (******************************************************************)
 
-(* N.B.: does NOT collapse AppLs ! *)
-let ensure_appl = function
-  | DOPN(AppL,_) as t -> t
-  | t -> DOPN(AppL,[|t|])
-
-(* unflattens application lists *)
-let rec telescope_appl = function
-  | DOPN(AppL,cl) ->
-      array_fold_left_from 1 (fun c e -> DOPN(AppL,[|c;e|])) (array_hd cl) cl
-  | c -> c
-
 (* flattens application lists *)
-let rec collapse_appl = function
-  | DOPN(AppL,cl) -> 
-      let rec collapse_rec = function
-	| (DOPN(AppL,cl),l2) -> collapse_rec(array_hd cl,array_app_tl cl l2)
-	| (DOP2(Cast,DOPN(AppL,cl),t),l) -> collapse_rec(DOPN(AppL,cl),l)
-	| (f,[]) -> f
-	| (f,l) -> let v = Array.of_list (f::l) in DOPN(AppL,v)
+let rec collapse_appl c = match kind_of_term c with
+  | IsAppL (f,cl) -> 
+      let rec collapse_rec f cl2 = match kind_of_term f with
+	| IsAppL (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
+	| IsCast (c,_) when isAppL c -> collapse_rec c cl2
+	| _ -> if cl2 = [||] then f else mkAppL (f,cl2)
       in 
-      collapse_rec (array_hd cl, array_list_of_tl cl)
-  | c -> c
+      collapse_rec f cl
+  | _ -> c
 
 let rec decomp_app c =
-  match collapse_appl c with
-    | DOPN(AppL,cl) -> (array_hd cl, array_list_of_tl cl)
-    | DOP2(Cast,c,t) -> decomp_app c
-    | c -> (c,[])
+  match kind_of_term (collapse_appl c) with
+    | IsAppL (f,cl) -> (f, Array.to_list cl)
+    | IsCast (c,t) -> decomp_app c
+    | _ -> (c,[])
 
 (* strips head casts and flattens head applications *)
-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)
-	| (DOP2(Cast,c,t),l) -> collapse_rec(c,l)
-	| (f,[]) -> f
-	| (f,l) -> let v = Array.of_list (f::l) in DOPN(AppL,v)
+let rec strip_head_cast c = match kind_of_term c with
+  | IsAppL (f,cl) -> 
+      let rec collapse_rec f cl2 = match kind_of_term f with
+	| IsAppL (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
+	| IsCast (c,_) -> collapse_rec c cl2
+	| _ -> if cl2 = [||] then f else mkAppL (f,cl2)
       in 
-      collapse_rec(array_hd cl, array_app_tl cl [])
-  | DOP2(Cast,c,t) -> strip_head_cast c
-  | c -> c
+      collapse_rec f cl
+  | IsCast (c,t) -> strip_head_cast c
+  | _ -> c
 
 (* Returns the list of global variables in a term *)
 
-let global_varsl l constr = 
-  let rec filtrec acc = function
-    | VAR id           -> id::acc
-    | DOP1(oper,c)     -> filtrec acc c
-    | DOP2(oper,c1,c2) -> filtrec (filtrec acc c1) c2
-    | DOPN(oper,cl)    -> Array.fold_left filtrec acc cl
-    | DLAM(_,c)        -> filtrec acc c
-    | DLAMV(_,v)       -> Array.fold_left filtrec acc v
-    | CLam (_,t,c)     -> filtrec (filtrec acc t) c
-    | CPrd (_,t,c)     -> filtrec (filtrec acc t) c
-    | CLet (_,b,t,c)   -> filtrec (filtrec (filtrec acc b) t) c
-    | _                -> acc
-  in 
-  filtrec l constr
+let rec global_varsl l constr = match kind_of_term constr with
+  | IsVar id -> id::l
+  | _        -> fold_constr global_varsl l constr
 
 let global_vars constr = global_varsl [] constr
 
 let global_vars_set constr = 
-  let rec filtrec acc = function
-    | VAR id           -> Idset.add id acc
-    | DOP1(oper,c)     -> filtrec acc c
-    | DOP2(oper,c1,c2) -> filtrec (filtrec acc c1) c2
-    | DOPN(oper,cl)    -> Array.fold_left filtrec acc cl
-    | DLAM(_,c)        -> filtrec acc c
-    | DLAMV(_,v)       -> Array.fold_left filtrec acc v
-    | CLam (_,t,c)     -> filtrec (filtrec acc t) c
-    | CPrd (_,t,c)     -> filtrec (filtrec acc t) c
-    | CLet (_,b,t,c)   -> filtrec (filtrec (filtrec acc b) t) c
-    | _                -> acc
+  let rec filtrec acc c = match kind_of_term c with
+    | IsVar id -> Idset.add id acc
+    | _        -> fold_constr filtrec acc c
   in 
   filtrec Idset.empty constr
 
 (* [Rel (n+m);...;Rel(n+1)] *)
 
-let rel_vect n m = Array.init m (fun i -> Rel(n+m-i))
+let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
 
 let rel_list n m = 
   let rec reln l p = 
-    if p>m then l else reln (Rel(n+p)::l) (p+1)
+    if p>m then l else reln (mkRel(n+p)::l) (p+1)
   in 
   reln [] 1
 
@@ -1228,190 +1406,81 @@ let rel_list n m =
 
 (* Various occurs checks *)
 
-let occur_opern s = 
-  let rec occur_rec = function
-    | DOPN(oper,cl) -> s=oper or (array_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
-    | CLam (_,t,c)   -> occur_rec t or occur_rec c
-    | CPrd (_,t,c)   -> occur_rec t or occur_rec c
-    | CLet (_,b,t,c) -> occur_rec b or occur_rec t or occur_rec c
-    | _             -> 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
-    | 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
-    | CLam (_,t,c)   -> occur_rec t or occur_rec c
-    | CPrd (_,t,c)   -> occur_rec t or occur_rec c
-    | CLet (_,b,t,c) -> occur_rec b or occur_rec t or occur_rec c
-    | _             -> false
+let occur_const s c = 
+  let rec occur_rec c = match kind_of_term c with
+    | IsConst (sp,_) when sp=s -> raise Occur
+    | _ -> iter_constr occur_rec c
   in 
-  occur_rec 
-
-(* let sigma be a finite function mapping sections paths to 
-   constants represented as (identifier list * constr) option.
-   (replace_consts sigma M) unfold_one_id the constants from sigma in term M
-
-   - if (sp,NONE) is in sigma then the constant should not appear in
-   term M otherwise replace_consts raises an anomaly ;
+  try occur_rec c; false with Occur -> true
 
-   - if (sp,SOME (idl,c)), then the constant sp is replaced by
-   c in which the variables given by idl are replaced by the arguments
-   of (Const sp), if the number of variables and arguments are not equal
-   an anomaly is raised ;
-
-   - if no (sp,_) appears in sigma, then sp is not unfolded.
-
-*)
-let replace_consts const_alist =
-  let rec substrec = function
-    | DOPN(Const sp,cl) as c ->
-	let cl' = Array.map substrec cl in
-	(try
-	   match List.assoc sp const_alist with
-	     | Some (hyps,body) ->
-                 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.to_list cl')) body
-             | None -> anomaly ("a constant which was never"^
-      	       	       		" supposed to appear has just appeared")
-	 with Not_found -> DOPN(Const sp,cl'))
-
-    | DOP1(i,c)         -> DOP1(i,substrec c)
-    | DOPN(oper,cl)     -> DOPN(oper,Array.map substrec cl)
-    | DOP2(oper,c1,c2)  -> DOP2(oper,substrec c1,substrec c2)
-    | DLAM(na,c)        -> DLAM(na,substrec c)
-    | DLAMV(na,v)       -> DLAMV(na,Array.map substrec v)
-    | CLam (na,t,c)     -> CLam (na, substrec t, substrec c)  
-    | CPrd (na,t,c)     -> CPrd (na, substrec t, substrec c)
-    | CLet (na,b,t,c)   -> CLet (na, substrec b, substrec t, substrec c)
-    | x                 -> x
+let occur_evar n c = 
+  let rec occur_rec c = match kind_of_term c with
+    | IsEvar (sp,_) when sp=n -> raise Occur
+    | _ -> iter_constr occur_rec c
   in 
-  if const_alist = [] then function x -> x else substrec
+  try occur_rec c; false with Occur -> true
 
-let whd_castapp_stack = 
-  let rec whrec x stack = match x with
-    | DOPN(AppL,cl)  -> whrec (array_hd cl) (array_app_tl cl stack)
-    | DOP2(Cast,c,_) -> whrec c stack
-    | x              -> x,stack
+let occur_var s c = 
+  let rec occur_rec c = match kind_of_term c with
+    | IsVar id when id=s -> raise Occur
+    | _ -> iter_constr occur_rec c
   in 
-  whrec
-
-(* whd flattens embedded applications
-   (whd_castapp ((((a b) c d) e f g) h)) -> (a b c d e f g h)
-   even if some casts exist in ((((a b) c d) e f g) h))
- *)
-let whd_castapp x = applist(whd_castapp_stack x [])
-
+  try occur_rec c; false with Occur -> true
 
 (***************************************)
 (*  alpha and eta conversion functions *)                         
 (***************************************)
 
 (* 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
-    | (Rel p1,Rel p2)                   -> p1=p2
-    | (DOPN(oper1,cl1),DOPN(oper2,cl2)) ->
-        oper1=oper2 & array_for_all2 eq_constr_rec cl1 cl2
-    | (DOP0 oper1,DOP0 oper2)           -> oper1=oper2
-    | (DOP1(i,c1),DOP1(j,c2))           -> (i=j) & eq_constr_rec c1 c2
-    | (DOP2(i,c1,c1'),DOP2(j,c2,c2'))   ->
-      	(i=j) & eq_constr_rec c1 c2 & eq_constr_rec c1' c2'
-    | (DLAM(_,c1),DLAM(_,c2)) 	       -> eq_constr_rec c1 c2
-    | (DLAMV(_,cl1),DLAMV(_,cl2))       -> 
-      	array_for_all2 eq_constr_rec cl1 cl2
-    | CLam(_,t1,c1), CLam(_,t2,c2) -> eq_constr_rec t1 t2 & eq_constr_rec c1 c2
-    | CPrd(_,t1,c1), CPrd(_,t2,c2) -> eq_constr_rec t1 t2 & eq_constr_rec c1 c2
-    | CLet(_,b1,t1,c1), CLet (_,b2,t2,c2) -> 
-	eq_constr_rec b1 b2 & eq_constr_rec t1 t2 & eq_constr_rec c1 c2
-    | _ -> false
-
-let eq_constr = eq_constr_rec
+let rec eq_constr m n = 
+  (m = n) or   (* Rem: ocaml '=' includes '==' *)
+  compare_constr eq_constr m n
 
 (* (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 dependent m t =
   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
-       | DLAM(_,c)   -> deprec (lift 1 m) c
-       | DLAMV(_,v)  -> array_exists (deprec (lift 1 m)) v
-       | CLam (_,t,c)   -> deprec m t or deprec (lift 1 m) c
-       | CPrd (_,t,c)   -> deprec m t or deprec (lift 1 m) c
-       | CLet (_,b,t,c) -> deprec m b or deprec m t or deprec (lift 1 m) c
-       | _ -> false)
+    if (eq_constr m t) then
+      raise Occur
+    else
+      iter_constr_with_binders (lift 1) deprec m t
   in 
-  deprec
+  try deprec m t; false with Occur -> true
 
 (* On reduit une serie d'eta-redex de tete ou rien du tout  *)
 (* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *)
 (* Remplace 2 versions précédentes buggées                  *)
 
 let rec eta_reduce_head c =
-  match c with
-    | CLam (_,c1,c') ->
-	(match eta_reduce_head c' with
-           | DOPN(AppL,cl) ->
+  match kind_of_term c with
+    | IsLambda (_,c1,c') ->
+	(match kind_of_term (eta_reduce_head c') with
+           | IsAppL (f,cl) ->
                let lastn = (Array.length cl) - 1 in 
                if lastn < 1 then anomaly "application without arguments"
                else
-                 (match cl.(lastn) with
-                    | Rel 1 ->
-                        let c' =
-                          if lastn = 1 then cl.(0) 
-			  else DOPN(AppL,Array.sub cl 0 lastn)
-                        in
-                        if (not ((dependent (mkRel 1) c'))) 
+                 (match kind_of_term cl.(lastn) with
+                    | IsRel 1 ->
+			let c' =
+                          if lastn = 1 then f
+			  else mkAppL (f, Array.sub cl 0 lastn)
+			in
+			if not (dependent (mkRel 1) c')
                         then lift (-1) c'
                         else c
-                    | _     -> c)
+                    | _   -> c)
            | _ -> c)
     | _ -> c
 
 (* alpha-eta conversion : ignore print names and casts *)
-
 let eta_eq_constr =
   let rec aux t1 t2 =
     let t1 = eta_reduce_head (strip_head_cast t1)
     and t2 = eta_reduce_head (strip_head_cast t2) in
-    t1=t2 or match (t1,t2) with
-    | (DOP2(Cast,c1,_),c2) -> aux c1 c2
-    | (c1,DOP2(Cast,c2,_)) -> aux c1 c2
-    | (Rel p1,Rel p2)                   -> p1=p2
-    | (DOPN(op1,cl1),DOPN(op2,cl2)) -> op1=op2 & array_for_all2 aux cl1 cl2
-    | (DOP0 oper1,DOP0 oper2)           -> oper1=oper2
-    | (DOP1(i,c1),DOP1(j,c2)) -> (i=j) & aux c1 c2
-    | (DOP2(i,c1,c1'),DOP2(j,c2,c2')) -> (i=j) & aux c1 c2 & aux c1' c2'
-    | (DLAM(_,c1),DLAM(_,c2)) -> aux c1 c2
-    | (DLAMV(_,cl1),DLAMV(_,cl2)) -> array_for_all2 aux cl1 cl2
-    | CLam(_,t1,c1), CLam(_,t2,c2) -> aux t1 t2 & aux c1 c2
-    | CPrd(_,t1,c1), CPrd(_,t2,c2) -> aux t1 t2 & aux c1 c2
-    | CLet(_,b1,t1,c1), CLet (_,b2,t2,c2) -> aux b1 b2 & aux t1 t2 & aux c1 c2
-    | _ -> false
+    t1=t2 or compare_constr aux t1 t2
   in aux
 
 
@@ -1438,34 +1507,36 @@ let rec rename_bound_var l c =
 
 (* First utilities for avoiding telescope computation for subst_term *)
 
-let prefix_application k (c : constr) (t : constr) = 
-  match (whd_castapp c,whd_castapp t) with
-    | ((DOPN(AppL,cl1)),DOPN(AppL,cl2)) ->
+let prefix_application (k,c) (t : constr) = 
+  let c' = strip_head_cast c and t' = strip_head_cast t in
+  match kind_of_term c', kind_of_term t' with
+    | IsAppL (f1,cl1), IsAppL (f2,cl2) ->
 	let l1 = Array.length cl1
 	and l2 = Array.length cl2 in
 	if l1 <= l2
-	   && eq_constr (DOPN(AppL,cl1)) (DOPN(AppL,Array.sub cl2 0 l1)) then
-	  Some(DOPN(AppL, array_cons (Rel k) (Array.sub cl2 l1 (l2 - l1))))
+	   && eq_constr c' (mkAppL (f2, Array.sub cl2 0 l1)) then
+	  Some (mkAppL (mkRel k, Array.sub cl2 l1 (l2 - l1)))
 	else 
 	  None
-    | (_,_) -> None
+    | _ -> None
 
-let prefix_application_eta k (c : constr) (t : constr) = 
-  match (whd_castapp c,whd_castapp t) with
-    | ((DOPN(AppL,cl1)),DOPN(AppL,cl2)) ->
+let prefix_application_eta (k,c) (t : constr) =
+  let c' = strip_head_cast c and t' = strip_head_cast t in
+  match kind_of_term c', kind_of_term t' with
+    | IsAppL (f1,cl1), IsAppL (f2,cl2) ->
 	let l1 = Array.length cl1
 	and l2 = Array.length cl2 in
 	if l1 <= l2 &&
-           eta_eq_constr (DOPN(AppL,cl1)) (DOPN(AppL,Array.sub cl2 0 l1)) then
-          Some(DOPN(AppL,array_cons (Rel k) (Array.sub cl2 l1 (l2 - l1))))
+           eta_eq_constr  c' (mkAppL (f2, Array.sub cl2 0 l1)) then
+	  Some (mkAppL (mkRel k, Array.sub cl2 l1 (l2 - l1)))
 	else 
 	  None
   | (_,_) -> None
 
 let sort_increasing_snd = 
   Sort.list 
-    (fun x y -> match x,y with 
-	 (_,Rel m),(_,Rel n) -> m < n
+    (fun (_,x) (_,y) -> match kind_of_term x, kind_of_term y with 
+       | IsRel m, IsRel n -> m < n
        | _ -> assert false)
 
 (* Recognizing occurrences of a given (closed) subterm in a term for Pattern :
@@ -1473,26 +1544,18 @@ let sort_increasing_snd =
    term [c] in a term [t] *)
 
 let subst_term_gen eq_fun c t = 
-  let rec substrec k c t =
-    match prefix_application k c t with
+  let rec substrec (k,c as kc) t =
+    match prefix_application kc t with
       | Some x -> x
       | None ->
-    (if eq_fun t c then Rel(k) else match t with
-       | DOPN(Const sp,cl) -> t
-       | DOPN(MutInd (x_0,x_1),cl) -> t
-       | DOPN(MutConstruct (x_0,x_1),cl) -> t
-       | DOPN(oper,tl)     -> DOPN(oper,Array.map (substrec k c) tl)
-       | DOP1(i,t)         -> DOP1(i,substrec k c t)
-       | DOP2(oper,c1,c2)  -> DOP2(oper,substrec k c c1,substrec k c c2)
-       | DLAM(na,t)        -> DLAM(na,substrec (k+1) (lift 1 c) t)
-       | DLAMV(na,v) -> DLAMV(na,Array.map (substrec (k+1) (lift 1 c)) v)
-       | CLam(na,t,c2) -> CLam(na,substrec k c t,substrec (k+1) (lift 1 c) c2) 
-       | CPrd(na,t,c2) -> CPrd(na,substrec k c t,substrec (k+1) (lift 1 c) c2) 
-       | CLet(na,b,t,c2) -> CLet(na,substrec k c b,substrec k c t,
-				substrec (k+1) (lift 1 c) c2)
-       | _ -> t)
+    (if eq_fun t c then mkRel k else match kind_of_term t with
+       | IsConst _ | IsMutInd _ | IsMutConstruct _ -> t
+       | _ ->
+	   map_constr_with_binders
+	     (fun (k,c) -> (k+1,lift 1 c))
+	     substrec kc t)
   in 
-  substrec 1 c t
+  substrec (1,c) t
 
 let subst_term = subst_term_gen eq_constr
 let subst_term_eta = subst_term_gen eta_eq_constr
@@ -1505,78 +1568,38 @@ let subst_term_eta = subst_term_gen eta_eq_constr
 (* Bogué ? Pourquoi pas de lift en passant sous un lieur ?? *)
 (* Et puis meta doit fusionner avec Evar *)
 let rec subst_meta bl c = 
-  match c with
-    | DOP0(Meta(i)) -> List.assoc i bl
-    | DOP1(op,c') -> DOP1(op, subst_meta bl c')
-    | DOP2(op,c'1, c'2) -> DOP2(op, subst_meta bl c'1, subst_meta bl c'2)
-    | DOPN(op, c') -> DOPN(op, Array.map (subst_meta bl) c')
-    | DLAM(x,c') -> DLAM(x, subst_meta bl c')
-    | CLam(na,t,c) -> CLam(na,subst_meta bl t,subst_meta bl c) 
-    | CPrd(na,t,c) -> CPrd(na,subst_meta bl t,subst_meta bl c) 
-    | CLet(na,b,t,c) -> CLet(na,subst_meta bl b,subst_meta bl t,
-			     subst_meta bl c)
-    | _ -> c
+  match kind_of_term c with
+    | IsMeta i -> List.assoc i bl
+    | _ -> map_constr (subst_meta bl) c
 
 (* Substitute only a list of locations locs, the empty list is
    interpreted as substitute all, if 0 is in the list then no
-   substitution is done the list may contain only negative occurrences
+   substitution is done. The list may contain only negative occurrences
    that will not be substituted. *)
 
 let subst_term_occ_gen locs occ c t =
+  let maxocc = List.fold_right max locs 0 in
   let pos = ref occ in
+  let check = ref true in
   let except = List.for_all (fun n -> n<0) locs in
-  let rec substcheck k c t =
-    if except or List.exists (function u -> u >= !pos) locs then
-      substrec k c t
-    else 
-      t
-  and substrec k c t =
+  let rec substrec (k,c as kc) t =
+    if (not except) & (!pos > maxocc) then t
+    else
     if eq_constr t c then
       let r = 
 	if except then 
-	  if List.mem (- !pos) locs then t else (Rel k)
+	  if List.mem (- !pos) locs then t else (mkRel k)
 	else 
-	  if List.mem !pos locs then (Rel k) else t
+	  if List.mem !pos locs then (mkRel k) else t
       in incr pos; r
     else
-      match t with
-	| DOPN((Const _ | MutConstruct _ | MutInd _), _) -> t
-	| DOPN(i,cl) -> 
-	    let cl' =
-	      Array.fold_left (fun lfd f -> substcheck k c f :: lfd) [] cl
-            in 
-	    DOPN(i,Array.of_list (List.rev cl'))
-	| DOP2(i,t1,t2) -> 
-	    let t1' = substrec k c t1 in
-            let t2' = substcheck k c t2 in
-            DOP2(i,t1',t2')
-	| DOP1(i,t) -> 
-	    DOP1(i,substrec k c t)
-	| DLAM(n,t) -> 
-            DLAM(n,substcheck (k+1) (lift 1 c) t)
-	| DLAMV(n,cl) -> 
-	     let cl' =   
-               Array.fold_left 
-		 (fun lfd f -> substcheck (k+1) (lift 1 c) f ::lfd)
-		 [] cl
-             in 
-	     DLAMV(n,Array.of_list (List.rev cl'))
-	| CLam(na,t,c2) ->
-	    let t' = substrec k c t in
-            let c2' = substcheck (k+1) (lift 1 c) c2 in
-	    CLam(na,t',c2')
-	| CPrd(na,t,c2) ->
-	    let t' = substrec k c t in
-            let c2' = substcheck (k+1) (lift 1 c) c2 in
-	    CPrd(na,t',c2')
-	| CLet(na,b,t,c2) ->
-	    let b' = substrec k c b in
-	    let t' = substrec k c t in
-            let c2' = substcheck (k+1) (lift 1 c) c2 in
-	    CLet(na,b',t',c2')
-	| DOP0 _ | VAR _ | Rel _ -> t
+      match kind_of_term t with
+	| IsConst _ | IsMutConstruct _ | IsMutInd _ -> t
+	| _ ->
+	    map_constr_with_binders_left_to_right
+	      (fun (k,c) -> (k+1,lift 1 c)) substrec kc t
   in
-  let t' = substcheck 1 c t in
+  let t' = substrec (1,c) t in
   (!pos, t')
 
 let subst_term_occ locs c t = 
@@ -1609,67 +1632,34 @@ let subst_term_occ_decl locs c (id,bodyopt,typ as d) =
 (* occurs check functions  *)                         
 (***************************)
 
-let rec occur_meta = function
-  | CPrd(_,t,c)      -> (occur_meta t) or (occur_meta c)
-  | CLam(_,t,c)      -> (occur_meta t) or (occur_meta c)
-  | CLet(_,b,t,c)    -> (occur_meta b) or (occur_meta t) or (occur_meta c)
-  | DOPN(_,cl)        -> (array_exists occur_meta cl)
-  | DOP2(Cast,c,t)    -> occur_meta c or occur_meta t
-  | DOP0(Meta(_))     -> true
-  | _                 -> false
-
-let occur_existential = 
-  let rec occrec = function
-    | DOPN(Evar _,_) -> true
-    | DOPN(_,cl) -> array_exists occrec cl
-    | DOP2(_,c1,c2) -> occrec c1 or occrec c2
-    | DOP1(_,c) -> occrec c
-    | DLAM(_,c) -> occrec c
-    | DLAMV(_,cl) -> array_exists occrec cl
-    | CPrd(_,t,c)   -> (occrec t) or (occrec c)
-    | CLam(_,t,c)   -> (occrec t) or (occrec c)
-    | CLet(_,b,t,c) -> (occrec b) or (occrec t) or (occrec c)
-    | _ -> false
-  in 
-  occrec
+let occur_meta c =
+  let rec occrec c = match kind_of_term c with
+    | IsMeta _ -> raise Occur
+    | _ -> iter_constr occrec c
+  in try occrec c; false with Occur -> true
 
-(***************************)
-(* hash-consing functions  *)                         
-(***************************)
+let occur_existential c = 
+  let rec occrec c = match kind_of_term c with
+    | IsEvar _ -> raise Occur
+    | _ -> iter_constr occrec c
+  in try occrec c; false with Occur -> true
 
-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
-    | (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
-    | CLam(x1,t1,c1), CLam(x2,t2,c2) ->	(x1==x2) & (t1==t2) & (c1==c2)
-    | CPrd(x1,t1,c1), CPrd(x2,t2,c2) ->	(x1==x2) & (t1==t2) & (c1==c2)
-    | CLet(x1,b1,t1,c1), CLet (x2,b2,t2,c2) ->
-	(x1==x2) & (b1==b2) & (t1==t2) & (c1==c2)
-    | (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)
-    | DLAM(n,t) -> DLAM(sh_na n, sh_rec t)
-    | DLAMV(n,v) -> DLAMV(sh_na n, Array.map sh_rec v)
-    | CLam (n,t,c)   -> CLam (sh_na n, sh_rec t, sh_rec c)  
-    | CPrd (n,t,c)   -> CPrd (sh_na n, sh_rec t, sh_rec c)
-    | CLet (n,b,t,c) -> CLet (sh_na n, sh_rec b, sh_rec t, sh_rec c)
-    | Rel i -> t
-    | VAR x -> VAR (sh_id x) 
+
+module Htype =
+  Hashcons.Make(
+    struct
+      type t = typed_type
+      type u = (constr -> constr) * (sorts -> sorts)
+(*
+      let hash_sub (hc,hs) j = {body=hc j.body; typ=hs j.typ}
+      let equal j1 j2 = j1.body==j2.body & j1.typ==j2.typ
+*)
+(**)
+      let hash_sub (hc,hs) j = hc j
+      let equal j1 j2 = j1==j2
+(**)
+      let hash = Hashtbl.hash
+    end)
 
 module Hsorts =
   Hashcons.Make(
@@ -1688,68 +1678,6 @@ module Hsorts =
       let hash = Hashtbl.hash
     end)
 
-module Hoper =
-  Hashcons.Make(
-    struct
-      type t = sorts oper
-      type u = (sorts -> sorts)
-               * (section_path -> section_path) * (string -> string)
-      let hash_sub (hsort,hsp,hstr) = function
-	| XTRA s -> XTRA (hstr s)
-        | Sort s -> Sort (hsort s)
-        | Const sp -> Const (hsp sp)
-        | MutInd (sp,i) -> MutInd (hsp sp, i)
-        | MutConstruct ((sp,i),j) -> MutConstruct ((hsp sp,i),j)
-        | MutCase ci as t -> t (* TO DO: extract ind_sp *)
-        | t -> t
-      let equal o1 o2 =
-        match (o1,o2) with
-          | (XTRA s1, XTRA s2) -> s1==s2
-          | (Sort s1, Sort s2) -> s1==s2
-          | (Const sp1, Const sp2) -> sp1==sp2
-          | (MutInd (sp1,i1), MutInd (sp2,i2)) -> sp1==sp2 & i1=i2
-          | (MutConstruct((sp1,i1),j1), MutConstruct((sp2,i2),j2)) ->
-              sp1==sp2 & i1=i2 & j1=j2
-          | (MutCase ci1,MutCase ci2) -> ci1==ci2 (* A simplification ?? *)
-          | _ -> o1=o2
-      let hash = Hashtbl.hash
-    end)    
-
-module Hconstr =
-  Hashcons.Make(
-    struct
-      type t = constr
-      type u = (constr -> constr)
-               * ((sorts oper -> sorts oper) * (name -> name) 
-                  * (identifier -> identifier))
-      let hash_sub = hash_term
-      let equal = comp_term
-      let hash = Hashtbl.hash
-    end)
-
-let hcons_oper (hsorts,hsp,hstr) =
-  Hashcons.simple_hcons Hoper.f (hsorts,hsp,hstr)
-
-let hcons_term (hsorts,hsp,hname,hident,hstr) =
-  let hoper = hcons_oper (hsorts,hsp,hstr) in
-  Hashcons.recursive_hcons Hconstr.f (hoper,hname,hident)
-
-module Htype =
-  Hashcons.Make(
-    struct
-      type t = typed_type
-      type u = (constr -> constr) * (sorts -> sorts)
-(*
-      let hash_sub (hc,hs) j = {body=hc j.body; typ=hs j.typ}
-      let equal j1 j2 = j1.body==j2.body & j1.typ==j2.typ
-*)
-(**)
-      let hash_sub (hc,hs) j = hc j
-      let equal j1 j2 = j1==j2
-(**)
-      let hash = Hashtbl.hash
-    end)
-
 let hcons_constr (hspcci,hspfw,hname,hident,hstr) =
   let hsortscci = Hashcons.simple_hcons Hsorts.f hspcci in
   let hsortsfw = Hashcons.simple_hcons Hsorts.f hspfw in
@@ -1763,20 +1691,10 @@ let hcons1_constr c =
   let (hc,_,_) = hcons_constr hnames in
   hc c
 
-(* Puts off the casts *)
-let put_off_casts = strip_outer_cast
-
-(*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.of_list (List.tl (Array.to_list t)))
-         |_ -> None)
-  |_ -> None
-
 (* Abstract decomposition of constr to deal with generic functions *)
 
+type fix_kind = RFix of (int array * int) | RCoFix of int
+
 type constr_operator =
   | OpMeta of int
   | OpSort of sorts
@@ -1788,52 +1706,52 @@ type constr_operator =
   | OpMutConstruct of constructor_path
   | OpMutCase of case_info
   | OpRec of fix_kind * name list
-
-let splay_constr = function
-  | Rel n                         -> OpRel n, [||]
-  | VAR id                        -> OpVar id, [||] 
-  | DOP0 (Meta n)                 -> OpMeta n, [||]
-  | DOP0 (Sort s)                 -> OpSort s, [||]
-  | DOP2 (Cast, t1, t2)           -> OpCast, [|t1;t2|]
-  | CPrd (x, t1, t2)              -> OpProd x, [|t1;t2|]
-  | CLam (x, t1, t2)              -> OpLambda x, [|t1;t2|]
-  | CLet (x, b, t1, t2)           -> OpLetIn x, [|b;t1;t2|]
-  | DOPN (AppL,a)                 -> OpAppL, a
-  | DOPN (Const sp, a)            -> OpConst sp, a
-  | DOPN (Evar sp, a)             -> OpEvar sp, a
-  | DOPN (MutInd ind_sp, l)       -> OpMutInd ind_sp, l
-  | DOPN (MutConstruct cstr_sp,l) -> OpMutConstruct cstr_sp, l
-  | DOPN (MutCase ci,v)           -> OpMutCase ci, v
-  | DOPN ((Fix (f,i),a)) as c     ->
-      let (fi,(tl,lna,bl)) = destFix c in
-      OpRec (RFix fi,lna), Array.append tl bl
-  | DOPN ((CoFix i),a) as c       ->
-      let (fi,(tl,lna,bl)) = destCoFix c in
-      OpRec (RCoFix fi,lna), Array.append tl bl
-  | _ -> errorlabstrm "Term.splay_term" [< 'sTR "ill-formed constr" >]
+  | OpXtra of string
+
+let splay_constr c = match kind_of_term c with
+  | IsRel n                    -> OpRel n, [||]
+  | IsVar id                   -> OpVar id, [||] 
+  | IsMeta n                   -> OpMeta n, [||]
+  | IsSort s                   -> OpSort s, [||]
+  | IsCast (t1, t2)            -> OpCast, [|t1;t2|]
+  | IsProd (x, t1, t2)         -> OpProd x, [|t1;t2|]
+  | IsLambda (x, t1, t2)       -> OpLambda x, [|t1;t2|]
+  | IsLetIn (x, b, t1, t2)     -> OpLetIn x, [|b;t1;t2|]
+  | IsAppL (f,a)               -> OpAppL, Array.append [|f|] a
+  | IsConst (sp, a)            -> OpConst sp, a
+  | IsEvar (sp, a)             -> OpEvar sp, a
+  | IsMutInd (ind_sp, l)       -> OpMutInd ind_sp, l
+  | IsMutConstruct (cstr_sp,l) -> OpMutConstruct cstr_sp, l
+  | IsMutCase (ci,p,c,bl)      -> OpMutCase ci, Array.append [|p;c|] bl
+  | IsFix (fi,(tl,lna,bl))     -> OpRec (RFix fi,lna), Array.append tl bl
+  | IsCoFix (fi,(tl,lna,bl))   -> OpRec (RCoFix fi,lna), Array.append tl bl
+  | IsXtra s                   -> OpXtra s, [||]
 
 let gather_constr = function
-  | OpRel n, [||]  -> Rel n
-  | OpVar id, [||] -> VAR id
-  | OpMeta n, [||] -> DOP0 (Meta n)
-  | OpSort s, [||] -> DOP0 (Sort s)
-  | OpCast, [|t1;t2|]     -> DOP2 (Cast, t1, t2)
+  | OpRel n, [||]  -> mkRel n
+  | OpVar id, [||] -> mkVar id
+  | OpMeta n, [||] -> mkMeta n
+  | OpSort s, [||] -> mkSort s
+  | OpCast, [|t1;t2|]     -> mkCast (t1, t2)
   | OpProd x, [|t1;t2|]   -> mkProd (x, t1, t2)
   | OpLambda x, [|t1;t2|] -> mkLambda (x, t1, t2)
   | OpLetIn x, [|b;t1;t2|] -> mkLetIn (x, b, t1, t2)
-  | OpAppL, a     -> DOPN (AppL, a)
-  | OpConst sp, a -> DOPN (Const sp, a)
-  | OpEvar sp, a  -> DOPN (Evar sp, a) 
-  | OpMutInd ind_sp, l        -> DOPN (MutInd ind_sp, l) 
-  | OpMutConstruct cstr_sp, l -> DOPN (MutConstruct cstr_sp, l)
-  | OpMutCase ci,  v    -> DOPN (MutCase ci, v)   
+  | OpAppL, v     -> let f = v.(0) and a = array_tl v in mkAppL (f, a)
+  | OpConst sp, a -> mkConst (sp, a)
+  | OpEvar sp, a  -> mkEvar (sp, a) 
+  | OpMutInd ind_sp, l        -> mkMutInd (ind_sp, l) 
+  | OpMutConstruct cstr_sp, l -> mkMutConstruct (cstr_sp, l)
+  | OpMutCase ci,  v    ->
+      let p = v.(0) and c = v.(1) and bl = Array.sub v 2 (Array.length v -2)
+      in mkMutCase (ci, p, c, bl)   
   | OpRec (RFix fi,lna), a  ->
       let n = Array.length a / 2 in
       mkFix (fi,(Array.sub a 0 n, lna, Array.sub a n n))
   | OpRec (RCoFix i,lna), a ->
       let n = Array.length a / 2 in
       mkCoFix (i,(Array.sub a 0 n, lna, Array.sub a n n))
-  | _ -> errorlabstrm "Term.gather_term" [< 'sTR "ill-formed constr" >]
+  | OpXtra s, [||] -> mkXtra s
+  | _ -> errorlabstrm "Term.gather_term" [< 'sTR "ill-formed splayed constr">]
 
 let rec mycombine l1 l3 =
   match (l1, l3) with
@@ -1845,52 +1763,53 @@ let rec mysplit = function
     [] -> ([], [])
   | (x, _, z)::l -> let (rx, rz) = mysplit l in (x::rx, z::rz)
 
-let splay_constr_with_binders = function
-  | Rel n                         -> OpRel n, [], [||]
-  | VAR id                        -> OpVar id, [], [||] 
-  | DOP0 (Meta n)                 -> OpMeta n, [], [||]
-  | DOP0 (Sort s)                 -> OpSort s, [], [||]
-  | DOP2 (Cast, t1, t2)           -> OpCast, [], [|t1;t2|]
-  | CPrd (x, t1, t2)              -> OpProd x, [x,None,t1], [|t2|]
-  | CLam (x, t1, t2)              -> OpLambda x, [x,None,t1], [|t2|]
-  | CLet (x, b, t1, t2)           -> OpLetIn x, [x,Some b,t1], [|t2|]
-  | DOPN (AppL,a)                 -> OpAppL, [], a
-  | DOPN (Const sp, a)            -> OpConst sp, [], a
-  | DOPN (Evar sp, a)             -> OpEvar sp, [], a
-  | DOPN (MutInd ind_sp, l)       -> OpMutInd ind_sp, [], l
-  | DOPN (MutConstruct cstr_sp,l) -> OpMutConstruct cstr_sp, [], l
-  | DOPN (MutCase ci,v)           -> OpMutCase ci, [], v
-  | DOPN ((Fix (f,i),a)) as c     ->
-      let (fi,(tl,lna,bl)) = destFix c in
+let splay_constr_with_binders c = match kind_of_term c with
+  | IsRel n                    -> OpRel n, [], [||]
+  | IsVar id                   -> OpVar id, [], [||] 
+  | IsMeta n                   -> OpMeta n, [], [||]
+  | IsSort s                   -> OpSort s, [], [||]
+  | IsCast (t1, t2)            -> OpCast, [], [|t1;t2|]
+  | IsProd (x, t1, t2)         -> OpProd x, [x,None,t1], [|t2|]
+  | IsLambda (x, t1, t2)       -> OpLambda x, [x,None,t1], [|t2|]
+  | IsLetIn (x, b, t1, t2)     -> OpLetIn x, [x,Some b,t1], [|t2|]
+  | IsAppL (f,v)               -> OpAppL, [], Array.append [|f|] v
+  | IsConst (sp, a)            -> OpConst sp, [], a
+  | IsEvar (sp, a)             -> OpEvar sp, [], a
+  | IsMutInd (ind_sp, l)       -> OpMutInd ind_sp, [], l
+  | IsMutConstruct (cstr_sp,l) -> OpMutConstruct cstr_sp, [], l
+  | IsMutCase (ci,p,c,bl)      ->
+      let v = Array.append [|p;c|] bl in OpMutCase ci, [], v
+  | IsFix (fi,(tl,lna,bl)) ->
       let n = Array.length bl in
       let ctxt = mycombine
 		   (List.rev lna)
 		   (Array.to_list (Array.mapi lift tl)) in
       OpRec (RFix fi,lna), ctxt, bl
-  | DOPN ((CoFix i),a) as c       ->
-      let (fi,(tl,lna,bl)) = destCoFix c in
+  | IsCoFix (fi,(tl,lna,bl)) ->
       let n = Array.length bl in
       let ctxt = mycombine
 		   (List.rev lna)
 		   (Array.to_list (Array.mapi lift tl)) in
       OpRec (RCoFix fi,lna), ctxt, bl
-  | _ -> errorlabstrm "Term.splay_term" [< 'sTR "ill-formed constr" >]
+  | IsXtra s -> OpXtra s, [], [||]
 
 let gather_constr_with_binders = function
-  | OpRel n, [], [||]  -> Rel n
-  | OpVar id, [], [||] -> VAR id
-  | OpMeta n, [], [||] -> DOP0 (Meta n)
-  | OpSort s, [], [||] -> DOP0 (Sort s)
-  | OpCast, [], [|t1;t2|]     -> DOP2 (Cast, t1, t2)
+  | OpRel n, [], [||]  -> mkRel n
+  | OpVar id, [], [||] -> mkVar id
+  | OpMeta n, [], [||] -> mkMeta n
+  | OpSort s, [], [||] -> mkSort s
+  | OpCast, [], [|t1;t2|]     -> mkCast (t1, t2)
   | OpProd _, [x,None,t1], [|t2|]   -> mkProd (x, t1, t2)
   | OpLambda _, [x,None,t1], [|t2|] -> mkLambda (x, t1, t2)
   | OpLetIn _, [x,Some b,t1], [|t2|] -> mkLetIn (x, b, t1, t2)
-  | OpAppL, [], a     -> DOPN (AppL, a)
-  | OpConst sp, [], a -> DOPN (Const sp, a)
-  | OpEvar sp, [], a  -> DOPN (Evar sp, a) 
-  | OpMutInd ind_sp, [], l        -> DOPN (MutInd ind_sp, l) 
-  | OpMutConstruct cstr_sp, [], l -> DOPN (MutConstruct cstr_sp, l)
-  | OpMutCase ci, [], v    -> DOPN (MutCase ci, v)   
+  | OpAppL, [], v     -> let f = v.(0) and a = array_tl v in mkAppL (f, a)
+  | OpConst sp, [], a -> mkConst (sp, a)
+  | OpEvar sp, [], a  -> mkEvar (sp, a) 
+  | OpMutInd ind_sp, [], l        -> mkMutInd (ind_sp, l) 
+  | OpMutConstruct cstr_sp, [], l -> mkMutConstruct (cstr_sp, l)
+  | OpMutCase ci, [], v    ->
+      let p = v.(0) and c = v.(1) and bl = Array.sub v 2 (Array.length v -2)
+      in mkMutCase (ci, p, c, bl)   
   | OpRec (RFix fi,lna), ctxt, bl  ->
       let (lna, tl) = mysplit ctxt in
       let tl = Array.mapi (fun i -> lift (-i)) (Array.of_list tl) in
@@ -1899,7 +1818,8 @@ let gather_constr_with_binders = function
       let (lna, tl) = mysplit ctxt in
       let tl = Array.mapi (fun i -> lift (-i)) (Array.of_list tl) in
       mkCoFix (i,(tl, List.rev lna, bl))
-  | _ -> errorlabstrm "Term.gather_term" [< 'sTR "ill-formed constr" >]
+  | OpXtra s, [], [||] -> mkXtra s
+  | _  -> errorlabstrm "Term.gather_term" [< 'sTR "ill-formed splayed constr">]
 
 let generic_fold_left f acc bl tl =
   let acc =
@@ -1909,88 +1829,3 @@ let generic_fold_left f acc bl tl =
 	   | None -> f acc t
 	   | Some b -> f (f acc b) t) acc bl in
   Array.fold_left f acc tl
-
-let fold_constr f acc c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> acc
-  | IsCast (c,t) -> f (f acc c) t
-  | IsProd (_,t,c) -> f (f acc t) c
-  | IsLambda (_,t,c) -> f (f acc t) c
-  | IsLetIn (_,b,t,c) -> f (f (f acc b) t) c
-  | IsAppL (c,l) -> Array.fold_left f (f acc c) l
-  | IsEvar (_,l) -> Array.fold_left f acc l
-  | IsConst (_,l) -> Array.fold_left f acc l
-  | IsMutInd (_,l) -> Array.fold_left f acc l
-  | IsMutConstruct (_,l) -> Array.fold_left f acc l
-  | IsMutCase (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
-  | IsFix (_,(tl,_,bl)) -> Array.fold_left f (Array.fold_left f acc tl) bl
-  | IsCoFix (_,(tl,_,bl)) -> Array.fold_left f (Array.fold_left f acc tl) bl
-
-let fold_constr_with_binders g f n acc c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> acc
-  | IsCast (c,t) -> f n (f n acc c) t
-  | IsProd (_,t,c) -> f (g n) (f n acc t) c
-  | IsLambda (_,t,c) -> f (g n) (f n acc t) c
-  | IsLetIn (_,b,t,c) -> f (g n) (f n (f n acc b) t) c
-  | IsAppL (c,l) -> Array.fold_left (f n) (f n acc c) l
-  | IsEvar (_,l) -> Array.fold_left (f n) acc l
-  | IsConst (_,l) -> Array.fold_left (f n) acc l
-  | IsMutInd (_,l) -> Array.fold_left (f n) acc l
-  | IsMutConstruct (_,l) -> Array.fold_left (f n) acc l
-  | IsMutCase (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
-  | IsFix (_,(tl,_,bl)) -> 
-      let n' = iterate g (Array.length tl) n in
-      Array.fold_left (f n') (Array.fold_left (f n) acc tl) bl
-  | IsCoFix (_,(tl,_,bl)) ->
-      let n' = iterate g (Array.length tl) n in
-      Array.fold_left (f n') (Array.fold_left (f n) acc tl) bl
-
-let iter_constr_with_binders g f n c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> ()
-  | IsCast (c,t) -> f n c; f n t
-  | IsProd (_,t,c) -> f n t; f (g n) c
-  | IsLambda (_,t,c) -> f n t; f (g n) c
-  | IsLetIn (_,b,t,c) -> f n b; f n t; f (g n) c
-  | IsAppL (c,l) -> f n c; Array.iter (f n) l
-  | IsEvar (_,l) -> Array.iter (f n) l
-  | IsConst (_,l) -> Array.iter (f n) l
-  | IsMutInd (_,l) -> Array.iter (f n) l
-  | IsMutConstruct (_,l) -> Array.iter (f n) l
-  | IsMutCase (_,p,c,bl) -> f n p; f n c; Array.iter (f n) bl
-  | IsFix (_,(tl,_,bl)) -> 
-      Array.iter (f n) tl; Array.iter (f (iterate g (Array.length tl) n)) bl
-  | IsCoFix (_,(tl,_,bl)) ->
-      Array.iter (f n) tl; Array.iter (f (iterate g (Array.length tl) n)) bl
-
-let map_constr f c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> c
-  | IsCast (c,t) -> mkCast (f c, f t)
-  | IsProd (na,t,c) -> mkProd (na, f t, f c)
-  | IsLambda (na,t,c) -> mkLambda (na, f t, f c)
-  | IsLetIn (na,b,t,c) -> mkLetIn (na, f b, f t, f c)
-  | IsAppL (c,l) -> appvect (f c, Array.map f l)
-  | IsEvar (e,l) -> mkEvar (e, Array.map f l)
-  | IsConst (c,l) -> mkConst (c, Array.map f l)
-  | IsMutInd (c,l) -> mkMutInd (c, Array.map f l)
-  | IsMutConstruct (c,l) -> mkMutConstruct (c, Array.map f l)
-  | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f p, f c, Array.map f bl)
-  | IsFix (ln,(tl,lna,bl)) -> mkFix (ln,(Array.map f tl,lna,Array.map f bl))
-  | IsCoFix(ln,(tl,lna,bl)) -> mkCoFix (ln,(Array.map f tl,lna,Array.map f bl))
-
-let map_constr_with_binders g f l c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> c
-  | IsCast (c,t) -> mkCast (f l c, f l t)
-  | IsProd (na,t,c) -> mkProd (na, f l t, f (g na l) c)
-  | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c)
-  | IsLetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c)
-  | IsAppL (c,al) -> appvect (f l c, Array.map (f l) al)
-  | IsEvar (e,al) -> mkEvar (e, Array.map (f l) al)
-  | IsConst (c,al) -> mkConst (c, Array.map (f l) al)
-  | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al)
-  | IsMutConstruct (c,al) -> mkMutConstruct (c, Array.map (f l) al)
-  | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f l p, f l c, Array.map (f l) bl)
-  | IsFix (ln,(tl,lna,bl)) ->
-      let l' = List.fold_right g lna l in
-      mkFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl))
-  | IsCoFix(ln,(tl,lna,bl)) ->
-      let l' = List.fold_right g lna l in
-      mkCoFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl))
diff --git a/kernel/term.mli b/kernel/term.mli
index 5758942596..1994584af6 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -16,9 +16,6 @@ type sorts =
   | Prop of contents       (* Prop and Set *)
   | Type of Univ.universe  (* Type *)
 
-val str_of_contents : contents -> string
-val contents_of_str : string -> contents
-
 val mk_Set  : sorts
 val mk_Prop : sorts
 
@@ -38,6 +35,7 @@ type case_printing =
 (* the integer is the number of real args, needed for reduction *)
 type case_info = int array * case_printing
 
+(*
 type 'a oper = 
   | Meta of int
   | Sort of 'a
@@ -50,6 +48,7 @@ type 'a oper =
   | Fix of int array * int
   | CoFix of int
   | XTRA of string
+*)
 
 (*s The type [constr] of the terms of CCI
   is obtained by instanciating a generic notion of terms
@@ -85,16 +84,10 @@ type var_declaration = identifier * constr option * typed_type
 type rel_declaration = name * constr option * typed_type
 
 (**********************************************************************)
-type binder_kind = BProd | BLambda | BLetIn
-
-type fix_kind = RFix of (int array * int) | RCoFix of int
-
-type 'ctxt reference =
-  | RConst of section_path * 'ctxt
-  | RInd of inductive_path * 'ctxt
-  | RConstruct of constructor_path * 'ctxt
-  | RVar of identifier
-  | REVar of int * 'ctxt
+type global_reference =
+  | ConstRef of section_path
+  | IndRef of inductive_path
+  | ConstructRef of constructor_path
 
 (*s Functions for dealing with constr terms.
   The following functions are intended to simplify and to uniform the 
@@ -113,7 +106,7 @@ type fixpoint = (int array * int) * (constr array * name list * constr array)
 type cofixpoint = int * (constr array * name list * constr array)
 
 
-type kindOfTerm =
+type kind_of_term =
   | IsRel          of int
   | IsMeta         of int
   | IsVar          of identifier
@@ -132,12 +125,11 @@ type kindOfTerm =
   | 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
-  make sense alone, but they must be preceeded by the application of
-  an operator. *)
+(* User view of [constr]. For [IsAppL], it is ensured there is at
+   least one argument and the function is not itself an applicative
+   term *)
 
-val kind_of_term : constr -> kindOfTerm
+val kind_of_term : constr -> kind_of_term
 
 
 (*s Term constructors. *)
@@ -247,9 +239,6 @@ val mkMutCase : case_info * constr * constr * constr array -> constr
 *)
 val mkFix : fixpoint -> constr
 
-(* Similarly, but we assume the body already constructed *)
-val mkFixDlam : int array -> int -> constr array -> constr array -> constr 
-
 (* If [typarray = [|t1,...tn|]]
       [funnames = [f1,.....fn]]
       [bodies   = [b1,.....bn]] \par\noindent
@@ -263,10 +252,6 @@ val mkFixDlam : int array -> int -> constr array -> constr array -> constr
  *)
 val mkCoFix : cofixpoint -> constr
 
-(* Similarly, but we assume the body already constructed *)
-val mkCoFixDlam : int -> constr array -> constr array -> constr
-
-
 (*s Term destructors. 
    Destructor operations are partial functions and
    raise [invalid_arg "dest*"] if the term has not the expected form. *)
@@ -291,7 +276,6 @@ val destXtra : constr -> string
 (* Destructs a sort. [is_Prop] recognizes the sort \textsf{Prop}, whether 
    [isprop] recognizes both \textsf{Prop} and \textsf{Set}. *)
 val destSort : constr -> sorts
-val contents_of_kind : constr -> contents
 val is_Prop : constr -> bool
 val is_Set : constr -> bool
 val isprop : constr -> bool
@@ -299,8 +283,6 @@ val is_Type : constr -> bool
 val iskind : constr -> bool
 val isSort : constr -> bool
 
-val is_existential_oper : sorts oper -> bool
-
 val isType : sorts -> bool
 val is_small : sorts -> bool (* true for \textsf{Prop} and \textsf{Set} *)
 
@@ -312,9 +294,6 @@ val isCast : constr -> bool
    [strip_outer_cast] (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
 val strip_outer_cast : constr -> constr
 
-(* Special function, which keep the key casts under Fix and MutCase. *)
-val strip_all_casts : constr -> constr
-
 (* Apply a function letting Casted types in place *)
 val under_casts : (constr -> constr) -> constr -> constr
 
@@ -327,7 +306,9 @@ val isVar  : constr -> bool
 (* Destructs the product $(x:t_1)t_2$ *)
 val destProd : constr -> name * constr * constr
 val hd_of_prod : constr -> constr
+(*i
 val hd_is_constructor : constr -> bool
+i*)
 
 (* Destructs the abstraction $[x:t_1]t_2$ *)
 val destLambda : constr -> name * constr * constr
@@ -336,10 +317,11 @@ val destLambda : constr -> name * constr * constr
 val destLetIn : constr -> name * constr * constr * constr
 
 (* Destructs an application *)
-val destAppL : constr -> constr array
 val isAppL : constr -> bool
+(*i
 val hd_app : constr -> constr 
 val args_app : constr -> constr array
+i*)
 val destApplication : constr -> constr * constr array
 
 (* Destructs a constant *)
@@ -373,8 +355,6 @@ val destCase : constr -> case_info * constr * constr * constr array
     \mathit{with}     ~ f_n ~ [ctx_n] = b_n$,
    where the lenght of the $j$th context is $ij$.
 *)
-val destGralFix : 
-  constr array -> constr array * Names.name list * constr array
 val destFix : constr -> fixpoint
 
 val destCoFix : constr -> cofixpoint
@@ -446,89 +426,6 @@ val nb_lam : constr -> int
 (* similar to [nb_lam], but gives the number of products instead *)
 val nb_prod : constr -> int
 
-(*i*)(* Trop compliqué 
-(*s Various utility functions for implementing terms with bindings. *)
-
-val extract_lifted : int * constr -> constr
-val insert_lifted : constr -> int * constr
-
-(* If [l] is a list of pairs $(n:nat,x:constr)$, [env] is a stack of 
-   $(na:name,T:constr)$, then
-   [push_and_lift (id,c) env l] adds a component [(id,c)] to [env] 
-   and lifts [l] one step *)
-val push_and_lift :
-  name * constr -> (name * constr) list -> (int * constr) list 
-    -> (name * constr) list * (int * constr) list
-
-(* if [T] is not $(x_1:A_1)(x_2:A_2)....(x_n:A_n)T'$ 
-   then [(push_and_liftl n env T l)]
-   raises an error else it gives $([x1,A1 ; x2,A2 ; ... ; xn,An]@env,T',l')$
-   where $l'$ is [l] lifted [n] steps *)
-val push_and_liftl :
-  int -> (name * constr) list -> constr -> (int * constr) list
-    -> (name * constr) list * constr * (int * constr) list
-
-(* if $T$ is not $[x_1:A_1][x_2:A_2]....[x_n:A_n]T'$ then 
-   [(push_lam_and_liftl n env T l)]
-   raises an error else it gives $([x_1,A_1; x_2,A_2; ...; x_n,A_n]@env,T',l')$
-   where $l'$ is [l] lifted [n] steps *)
-val push_lam_and_liftl :
-  int -> (name * constr) list -> constr -> (int * constr) list
-    -> (name * constr) list * constr * (int * constr) list
-
-(* If [l] is a list of pairs $(n:nat,x:constr)$, [tlenv] is a stack of
-   $(na:name,T:constr)$, [B] is a constr, [na] a name, then
-   [(prod_and_pop ((na,T)::tlenv) B l)] gives $(tlenv, (na:T)B, l')$
-   where $l'$ is [l] lifted down one step *)
-val prod_and_pop :
-  (name * constr) list -> constr -> (int * constr) list
-    -> (name * constr) list * constr * (int * constr) list
-
-(* recusively applies [prod_and_pop] :
-   if [env] = $[na_1:T_1 ; na_2:T_2 ; ... ; na_n:T_n]@tlenv$ then
-   [(prod_and_popl n env T l)] gives $(tlenv,(na_n:T_n)...(na_1:T_1)T,l')$
-   where $l'$ is [l] lifted down [n] steps *)
-val prod_and_popl :
-  int -> (name * constr) list -> constr -> (int * constr) list
-    -> (name * constr) list * constr * (int * constr) list
-
-(* similar to [prod_and_pop], but gives $[na:T]B$ intead of $(na:T)B$ *)
-val lam_and_pop :
-  (name * constr) list -> constr -> (int * constr) list
-    -> (name * constr) list * constr * (int * constr) list
-
-(* similar to [prod_and_popl] but gives $[na_n:T_n]...[na_1:T_1]B$ instead of
-   $(na_n:T_n)...(na_1:T_1)B$ *)
-val lam_and_popl :
-  int -> (name * constr) list -> constr -> (int * constr) list
-    -> (name * constr) list * constr * (int * constr) list
-
-(* similar to [lamn_and_pop] but generates new names whenever the name is 
-   [Anonymous] *)
-val lam_and_pop_named :
-  (name * constr) list -> constr ->(int * constr) list ->identifier list 
-    -> (name * constr) list * constr * (int * constr) list * identifier list
-
-(* similar to [prod_and_popl] but gives $[na_n:T_n]...[na_1:T_1]B$ instead of
-   but it generates names whenever $na_i$ = [Anonymous] *)
-val lam_and_popl_named :
-  int ->  (name * constr) list -> constr ->  (int * constr) list 
-    -> (name * constr) list * constr * (int * constr) list 
-
-(* [lambda_ize n T endpt]
-   will pop off the first [n] products in [T], then stick in [endpt],
-   properly lifted, and then push back the products, but as lambda-
-   abstractions *)
-val lambda_ize : int ->'a oper term -> 'a oper term -> 'a oper term
-*)(*i*)
-
-(*s Flattening and unflattening of embedded applications and casts. *)
-
-(* if [c] is not an [AppL], it is transformed into [mkAppL [| c |]] *)
-val ensure_appl : constr -> constr
-
-(* unflattens application lists *)
-val telescope_appl : constr -> constr
 (* flattens application lists *)
 val collapse_appl : constr -> constr
 val decomp_app : constr -> constr * constr list
@@ -637,8 +534,6 @@ 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
-val whd_castapp : constr -> constr
 val rename_bound_var : identifier list -> constr -> constr
 val eta_reduce_head : constr -> constr
 val eq_constr : constr -> constr -> bool
@@ -650,9 +545,6 @@ val subst_term_occ : occs:int list -> what:constr -> where:constr -> constr
 val subst_term_occ_decl : occs:int list -> what:constr ->
       where:var_declaration -> var_declaration
 
-val replace_consts :
-  (section_path * (identifier list * constr) option) list -> constr -> constr
-
 (* [subst_meta bl c] substitutes the metavar $i$ by $c_i$ in [c] 
    for each binding $(i,c_i)$ in [bl],
    and raises [Not_found] if [c] contains a meta that is not in the 
@@ -660,6 +552,10 @@ val replace_consts :
 
 val subst_meta : (int * constr) list -> constr -> constr
 
+(*s Generic representation of constructions *)
+
+type fix_kind = RFix of (int array * int) | RCoFix of int
+
 type constr_operator =
   | OpMeta of int
   | OpSort of sorts
@@ -671,6 +567,7 @@ type constr_operator =
   | OpMutConstruct of constructor_path
   | OpMutCase of case_info
   | OpRec of fix_kind * Names.name list
+  | OpXtra of string
 
 val splay_constr : constr -> constr_operator * constr array
 val gather_constr : constr_operator * constr array -> constr
@@ -685,19 +582,78 @@ val generic_fold_left :
   ('a -> constr -> 'a) -> 'a -> (name * constr option * constr) list
       -> constr array -> 'a
 
+(*s Functionals working on the immediate subterm of a construction *)
+
+(* [fold_constr f acc c] folds [f] on the immediate subterms of [c]
+   starting from [acc] and proceeding from left to right according to
+   the usual representation of the constructions; it is not recursive *)
+
 val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a
 
+(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
+   subterms of [c] starting from [acc] and proceeding from left to
+   right according to the usual representation of the constructions as
+   [fold_constr] but it carries an extra data [n] (typically a lift
+   index) which is processed by [g] (which typically add 1 to [n]) at
+   each binder traversal; it is not recursive *)
+
 val fold_constr_with_binders :
   ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
 
+(* [iter_constr f c] iters [f] on the immediate subterms of [c]; it is
+   not recursive and the order with which subterms are processed is
+   not specified *)
+
+val iter_constr : (constr -> unit) -> constr -> unit
+
+(* [iter_constr_with_binders g f n c] iters [f n] on the immediate
+   subterms of [c]; it carries an extra data [n] (typically a lift
+   index) which is processed by [g] (which typically add 1 to [n]) at
+   each binder traversal; it is not recursive and the order with which
+   subterms are processed is not specified *)
+
 val iter_constr_with_binders :
   ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
 
+(* [map_constr f c] maps [f] on the immediate subterms of [c]; it is
+   not recursive and the order with which subterms are processed is
+   not specified *)
+
 val map_constr : (constr -> constr) -> constr -> constr
 
+(* [map_constr_with_binders g f n c] maps [f n] on the immediate
+   subterms of [c]; it carries an extra data [n] (typically a lift
+   index) which is processed by [g] (which typically add 1 to [n]) at
+   each binder traversal; it is not recursive and the order with which
+   subterms are processed is not specified *)
+
 val map_constr_with_binders :
+  ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
+
+(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
+   subterms of [c]; it carries an extra data [l] (typically a name
+   list) which is processed by [g na] (which typically cons [na] to
+   [l]) at each binder traversal (with name [na]); it is not recursive
+   and the order with which subterms are processed is not specified *)
+
+val map_constr_with_named_binders :
   (name -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
 
+(* [map_constr_with_binders_left_to_right g f n c] maps [f n] on the
+   immediate subterms of [c]; it carries an extra data [n] (typically
+   a lift index) which is processed by [g] (which typically add 1 to
+   [n]) at each binder traversal; the subterms are processed from left
+   to right according to the usual representation of the constructions
+   (this may matter if [f] does a side-effect); it is not recursive *)
+
+val map_constr_with_binders_left_to_right :
+  ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
+
+(* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare
+   the immediate subterms of [c1] of [c2] if needed; Cast's, binders
+   name and Cases annotations are not taken into account *)
+
+val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
 
 (*s Hash-consing functions for constr. *)