generic, term et evd

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

12 files changed, 2918 insertions, 0 deletions

diff --git a/kernel/environ.mli b/kernel/environ.mli
new file mode 100644
index 0000000000..24cd002826
--- /dev/null
+++ b/kernel/environ.mli
@@ -0,0 +1,20 @@
+
+(* $Id$ *)
+
+open Names
+open Term
+open Constant
+open Inductive
+
+type unsafe_env
+
+val push_var : identifier * constr -> unsafe_env -> unsafe_env
+val push_rel : name * constr -> unsafe_env -> unsafe_env
+
+val add_constant : constant -> unsafe_env -> unsafe_env
+val add_mind : mind -> unsafe_env -> unsafe_env
+
+
+val lookup_var : identifier -> unsafe_env -> constr
+val loopup_rel : int -> unsafe_env -> name * constr
+
diff --git a/kernel/evd.ml b/kernel/evd.ml
new file mode 100644
index 0000000000..77351ab9b7
--- /dev/null
+++ b/kernel/evd.ml
@@ -0,0 +1,64 @@
+
+(* $Id$ *)
+
+open Util
+open Names
+open Term
+open Sign
+
+(* The type of mappings for existential variables *)
+
+type evar_body =
+    EVAR_EMPTY | EVAR_DEFINED of constr
+
+type 'a evar_info = {
+  concl : constr;            (* the type of the evar ...          *)
+  hyps  : context;           (* ... under a certain signature     *)
+  body  : evar_body;         (* its definition                    *) 
+  info  : 'a option          (* any other necessary information   *)
+}         
+
+type 'a evar_map = 'a evar_info Spmap.t
+
+let mt_evd = Spmap.empty
+
+let toList evc = Spmap.fold (fun sp x acc -> (sp,x)::acc) evc []
+let dom evc = Spmap.fold (fun sp _ acc -> sp::acc) evc []
+let map evc k = Spmap.find k evc
+let rmv evc k = Spmap.remove k evc
+let remap evc k i = Spmap.add k i evc
+let in_dom evc k = Spmap.mem k evc
+
+let add_with_info evd sp newinfo = 
+  Spmap.add sp newinfo evd
+
+let add_noinfo evd sp sign typ = 
+  let newinfo = 
+    { concl = typ;
+      hyps  = sign;
+      body  = EVAR_EMPTY;
+      info  = None}
+  in 
+  Spmap.add sp newinfo evd
+
+let define evd sp body = 
+ let oldinfo = map evd sp in
+ let newinfo =
+   { concl = oldinfo.concl;
+     hyps  = oldinfo.hyps;
+     body  = EVAR_DEFINED body;
+     info  = oldinfo.info} 
+ in
+ match oldinfo.body with
+   | EVAR_EMPTY -> Spmap.add sp newinfo evd
+   | _ -> anomaly "cannot define an isevar twice"
+
+(* The list of non-instantiated existential declarations *)
+
+let non_instantiated sigma = 
+    let listsp = toList sigma in
+    List.fold_left 
+        (fun l ((sp,evd) as d) -> if evd.body = EVAR_EMPTY then (d::l) else l)
+        [] listsp
+
+let is_evar sigma sp = in_dom sigma sp
diff --git a/kernel/evd.mli b/kernel/evd.mli
new file mode 100644
index 0000000000..cb606941c0
--- /dev/null
+++ b/kernel/evd.mli
@@ -0,0 +1,37 @@
+
+(* $Id$ *)
+
+open Names
+open Term
+open Sign
+
+(* The type of mappings for existential variables *)
+
+type evar_body =
+  | EVAR_EMPTY 
+  | EVAR_DEFINED of constr
+
+type 'a evar_info = {
+  concl : constr;            (* the type of the evar ...                 *)
+  hyps  : context;           (* ... under a certain signature            *)
+  body  : evar_body;         (* its definition                           *) 
+  info  : 'a option          (* any other possible information necessary *)
+}         
+
+type 'a evar_map
+
+val dom    : 'c evar_map -> section_path list
+val map    : 'c evar_map -> section_path -> 'c evar_info
+val rmv    : 'c evar_map -> section_path -> 'c evar_map
+val remap  : 'c evar_map -> section_path -> 'c evar_info -> 'c evar_map
+val in_dom : 'c evar_map -> section_path -> bool
+val toList : 'c evar_map -> (section_path * 'c evar_info) list
+
+val mt_evd : 'c evar_map
+val add_with_info : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map
+val add_noinfo : 'a evar_map -> section_path -> context -> 
+                 constr -> 'a evar_map
+val define : 'a evar_map -> section_path -> constr -> 'a evar_map
+
+val non_instantiated : 'a evar_map -> (section_path * 'a evar_info) list
+val is_evar : 'a evar_map -> section_path -> bool
diff --git a/kernel/generic.ml b/kernel/generic.ml
new file mode 100644
index 0000000000..9adc53ce68
--- /dev/null
+++ b/kernel/generic.ml
@@ -0,0 +1,604 @@
+
+(* $Id$ *)
+
+open Util
+open Pp
+open Names
+
+(********************************************************************)
+(*           Generic syntax of terms with de Bruijn indexes         *)
+(********************************************************************)
+
+type 'oper term =
+  | DOP0 of 'oper                            (* atomic terms *)
+  | DOP1 of 'oper * 'oper term               (* operator of arity 1 *)
+  | DOP2 of 'oper * 'oper term * 'oper term  (* operator of arity 2 *)
+  | DOPN of 'oper * 'oper term array         (* operator of variadic arity *)
+  | DOPL of 'oper * 'oper term list          (* operator of variadic arity *)
+  | DLAM of name * 'oper term                (* deBruijn binder on one term*)
+  | DLAMV of name * 'oper term array         (* deBruijn binder on many terms*)
+  | VAR of identifier                        (* named variable *)
+  | Rel of int                               (* variable as deBruijn index *)
+
+exception FreeVar
+exception Occur
+
+let isRel = function Rel _ -> true | _ -> false
+let isVAR = function VAR _ -> true | _ -> false
+
+(* returns the list of free debruijn indices in a term *)
+
+let free_rels m = 
+  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
+    | DOPL(_,cl)    -> List.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
+    | VAR _         -> acc
+    | DOP0 _        -> acc
+  in 
+  frec 1 Intset.empty m
+
+(* (closedn n M) raises FreeVar if a variable of height greater than n
+   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
+    | DOPL(_,cl)    -> List.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
+    | _             -> ()
+  in 
+  closed_rec
+
+(* (closed M) is true iff M is a (deBruijn) closed term *)
+
+let closed0 term =
+  try closedn 0 term; true with FreeVar -> false
+
+(* (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
+    | DOPL(_,cl)    -> List.iter (occur_rec n) cl
+    | DOP1(_,c)     -> occur_rec n c
+    | DOP2(_,c1,c2) -> occur_rec n c1; occur_rec n c2
+    | DLAM(_,c)     -> occur_rec (n+1) c
+    | DLAMV(_,v)    -> Array.iter (occur_rec (n+1)) v
+    | _             -> ()
+  in 
+  try occur_rec n term; true with Occur -> false
+
+(* (noccur_bet n m M) returns true iff (Rel p) does NOT occur in term M 
+  for n <= p < n+m *)
+
+let noccur_bet 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
+    | DOPL(_,cl)    -> List.iter (occur_rec n) cl
+    | DOP1(_,c)     -> occur_rec n c
+    | DOP2(_,c1,c2) -> occur_rec n c1; occur_rec n c2
+    | DLAM(_,c)     -> occur_rec (n+1) c
+    | DLAMV(_,v)    -> Array.iter (occur_rec (n+1)) v
+    | _             -> ()
+  in 
+  try occur_rec n term; true with Occur -> false
+
+(* Explicit lifts and basic operations *)
+type lift_spec =
+  | ELID
+  | ELSHFT of lift_spec * int (* ELSHFT(l,n) == lift of n, then apply lift l *)
+  | ELLFT of int * lift_spec  (* ELLFT(n,l)  == apply l to de Bruijn > n *)
+                            (*                 i.e under n binders *)
+
+(* compose a relocation of magnitude n *)
+let rec el_shft n = function
+  | ELSHFT(el,k) -> el_shft (k+n) el
+  | el -> if n = 0 then el else ELSHFT(el,n)
+
+
+(* cross n binders *)
+let rec el_liftn n = function
+  | ELID -> ELID
+  | ELLFT(k,el) -> el_liftn (n+k) el
+  | el -> if n=0 then el else ELLFT(n, el)
+
+let el_lift el = el_liftn 1 el
+
+(* relocation of de Bruijn n in an explicit lift *)
+let rec reloc_rel n = function
+  | ELID -> n
+  | ELLFT(k,el) ->
+      if n <= k then n else (reloc_rel (n-k) el) + k
+  | ELSHFT(el,k) -> (reloc_rel (n+k) el)
+
+
+(* 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)
+  | DOPL(oper,cl)    -> DOPL(oper, List.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)
+  | x                -> x
+
+
+(* Lifting the binding depth across k bindings *)
+
+let liftn k n = 
+  match el_liftn (pred n) (el_shft k ELID) with
+    | ELID -> (fun c -> c)
+    | el -> exliftn el
+ 
+let lift k = liftn k 1
+let lift1 c = exliftn (ELSHFT(ELID,1)) c
+
+
+(* explicit substitutions of type 'a *)
+type 'a subs =
+  | ESID                   (* ESID       =          identity *)
+  | CONS of 'a * 'a subs   (* CONS(t,S)  = (S.t)    parallel substitution *)
+  | SHIFT of int * 'a subs (* SHIFT(n,S) = (^n o S) terms in S are relocated *)
+                           (*                        with n vars *)
+  | LIFT of int * 'a subs  (* LIFT(n,S) = (%n S) stands for ((^n o S).n...1) *)
+
+(* operations of subs: collapses constructors when possible.
+ * Needn't be recursive if we always use these functions
+ *)
+let subs_cons(x,s) = CONS(x,s)
+
+let subs_lift = function
+  | ESID -> ESID         (* the identity lifted is still the identity *)
+                         (* (because (^1.1) --> id) *)
+  | LIFT (n,lenv) -> LIFT (n+1, lenv)
+  | lenv -> LIFT (1,lenv)
+
+let subs_shft = function
+  | (0, s)            -> s
+  | (n, SHIFT (k,s1)) -> SHIFT (k+n, s1)
+  | (n, s)            -> SHIFT (n,s)
+
+
+(* Expands de Bruijn k in the explicit substitution subs
+ * lams accumulates de shifts to perform when retrieving the i-th value
+ * the rules used are the following:
+ *
+ *    [id]k       --> k
+ *    [S.t]1      --> t
+ *    [S.t]k      --> [S](k-1)  if k > 1
+ *    [^n o S] k  --> [^n]([S]k)
+ *    [(%n S)] k  --> k         if k <= n
+ *    [(%n S)] k  --> [^n]([S](k-n))
+ *
+ * the result is (Inr k) when the variable is just relocated
+ *) 
+let rec exp_rel lams k subs =
+  match (k,subs) with
+    | (1, CONS (def,_)) -> Inl(lams,def)
+    | (_, CONS (_,l)) -> exp_rel lams (pred k) l
+    | (_, LIFT (n,_)) when k<=n -> Inr(lams+k)
+    | (_, LIFT (n,l)) -> exp_rel (n+lams) (k-n) l
+    | (_, SHIFT (n,s)) -> exp_rel (n+lams) k s
+    | (_, ESID) -> Inr(lams+k)
+
+let expand_rel k subs = exp_rel 0 k subs
+
+
+(* (subst1 M c) substitutes M for Rel(1) in c 
+   we generalise it to (substl [M1,...,Mn] c) which substitutes in parallel
+   M1,...,Mn for respectively Rel(1),...,Rel(n) in c *)
+
+(* 1st : general case *)
+
+type info = Closed | Open | Unknown
+type 'a substituend = { mutable sinfo: info; sit: 'a }
+
+let rec lift_substituend depth s =
+  match s.sinfo with
+    | Closed -> s.sit
+    | Open -> lift depth s.sit
+    | Unknown ->
+        s.sinfo <- if closed0 s.sit then Closed else Open;
+        lift_substituend depth s
+
+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     ->
+        if k<=depth then 
+	  x
+        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)
+    | DOPL(oper,cl)    -> DOPL(oper,List.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)
+    | x                -> x
+  in 
+  substrec n
+
+let substl laml =
+  substn_many (Array.map make_substituend (Array.of_list laml)) 0
+let subst1 lam = substl [lam]
+let pop t = lift (-1) t
+
+
+(* Various occurs checks *)
+
+let occur_opern s = 
+  let rec occur_rec = function
+    | DOPN(oper,cl) -> s=oper or (array_exists occur_rec cl)
+    | DOPL(oper,cl) -> s=oper or (List.exists occur_rec cl)
+    | VAR _         -> false
+    | DOP1(_,c)     -> occur_rec c 
+    | DOP2(_,c1,c2) -> (occur_rec c1) or (occur_rec c2)
+    | DLAM(_,c)     -> occur_rec c
+    | DLAMV(_,v)    -> array_exists occur_rec v
+    | _             -> false
+  in 
+  occur_rec 
+
+let occur_oper0 s = 
+  let rec occur_rec = function
+    | DOPN(_,cl)    -> (array_exists occur_rec cl)
+    | DOPL(_,cl)    -> (List.exists occur_rec cl)
+    | DOP0 oper     -> s=oper
+    | VAR _         -> false
+    | DOP1(_,c)     -> occur_rec c 
+    | DOP2(_,c1,c2) -> (occur_rec c1) or (occur_rec c2)
+    | DLAM(_,c)     -> occur_rec c
+    | DLAMV(_,v)    -> array_exists occur_rec v
+    | _             -> false
+  in 
+  occur_rec 
+
+let occur_var s = 
+  let rec occur_rec = function
+    | DOPN(_,cl)    -> array_exists occur_rec cl
+    | DOPL(_,cl)    -> List.exists occur_rec cl
+    | VAR id        -> s=id
+    | DOP1(_,c)     -> occur_rec c 
+    | DOP2(_,c1,c2) -> (occur_rec c1) or (occur_rec c2)
+    | DLAM(_,c)     -> occur_rec c
+    | DLAMV(_,v)    -> array_exists occur_rec v
+    | _             -> false
+  in 
+  occur_rec 
+
+let occur_oper s = 
+  let rec occur_rec = function
+    | DOPN(oper,cl)    -> s=oper or (array_exists occur_rec cl)
+    | DOPL(oper,cl)    -> s=oper or (List.exists occur_rec cl)
+    | VAR _            -> false
+    | DOP0 oper        -> s=oper
+    | DOP1(oper,c)     -> s=oper or occur_rec c 
+    | DOP2(oper,c1,c2) -> s=oper or (occur_rec c1) or (occur_rec c2)
+    | DLAM(_,c)        -> occur_rec c
+    | DLAMV(_,v)       -> array_exists occur_rec v
+    | _                -> false
+  in 
+  occur_rec 
+
+(* 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
+    | DOPL(oper,cl)      -> List.fold_left filtrec acc cl
+    | DLAM(_,c)          -> filtrec acc c
+    | DLAMV(_,v)         -> Array.fold_left filtrec acc v
+    | _                  -> acc
+  in 
+  filtrec l constr
+
+let global_vars constr = global_varsl [] constr
+
+let global_vars_set constr = 
+  List.fold_left (fun s x -> Idset.add x s) Idset.empty (global_vars constr)
+
+(* alpha equality for generic terms : checks first if M and M' are equal,
+   otherwise checks equality forgetting the name annotation of DLAM and DLAMV*)
+
+let rec eq_term m m' =
+     (m == m') 
+  or (m = m')
+  or (match (m,m') with
+	| (DOP1(oper1,c1),DOP1(oper2,c2)) ->
+            oper1 = oper2 & eq_term c1 c2
+	| (DOP2(oper1,c1,t1),DOP2(oper2,c2,t2)) ->
+            oper1 = oper2 & eq_term c1 c2 & eq_term t1 t2
+	| (DOPN(oper1,cl1),DOPN(oper2,cl2)) ->
+            oper1 = oper2 & array_for_all2 eq_term cl1 cl2
+	| (DOPL(oper1,cl1),DOPL(oper2,cl2)) ->
+            oper1 = oper2 & List.for_all2 eq_term cl1 cl2
+	| (DLAM(_,c1),DLAM(_,c2)) -> eq_term c1 c2
+	| (DLAMV(_,cl1),DLAMV(_,cl2)) -> array_for_all2 eq_term cl1 cl2
+	| _ -> false)
+
+(* (dependent M N) is true iff M is eq_term with a subterm of N 
+   M is appropriately lifted through abstractions of N *)
+let dependent =
+  let rec deprec m = function t ->
+       (eq_term m t)
+    or (match t with
+	  | VAR _       -> false
+	  | DOP1(_,c)   -> deprec m c
+	  | DOP2(_,c,t) -> deprec m c or deprec m t
+	  | DOPN(_,cl)  -> array_exists (deprec m) cl
+	  | DOPL(_,cl)  -> List.exists (deprec m) cl
+	  | DLAM(_,c)   -> deprec (lift1 m) c
+	  | DLAMV(_,v)  -> array_exists (deprec (lift1 m)) v
+	  | _ -> false)
+  in 
+  deprec
+
+(* (thin_val sigma) removes identity substitutions from sigma *)
+
+let rec thin_val = function
+  | [] -> []
+  | (((id,{sit=VAR id'}) as s)::tl) -> 
+      if id = id' 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 *)
+let replace_vars var_alist = 
+  let var_alist = thin_val var_alist in 
+  let rec substrec n = function
+    | (VAR(x) as c)    ->
+        (try lift_substituend n (List.assoc x var_alist)
+         with Not_found -> c)
+	
+    | DOPN(oper,cl)    -> DOPN(oper,Array.map (substrec n) cl)
+    | DOPL(oper,cl)    -> DOPL(oper,List.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)
+    | x                -> x
+  in 
+  if var_alist = [] then (function x -> x) else substrec 0
+
+let subst_varn str n = replace_vars [(str,make_substituend (Rel n))]
+
+(* (subst_var str t) substitute (VAR str) by (Rel 1) in t *)
+let subst_var str = subst_varn str 1
+
+
+(* renames different  ocurrences of (VAR id) in t with a fresh identifier
+   wrt. acc *)
+let rename_diff_occ  id acc t =
+  let rec rename_occ acc  = function
+    | (VAR(x)  as c) -> 
+	if x <> id then 
+	  acc,c
+        else 
+	  let nid = next_ident_away id acc in (nid::acc), (VAR nid)
+    | DOPN(oper,cl) -> 
+	let nacc,ncl = vrename_occ acc  cl in nacc,DOPN(oper, ncl)
+    | DOPL(oper,cl) -> 
+	let nacc,ncl = lrename_occ acc cl in nacc, DOPL(oper,ncl)
+    | DOP1(oper,c) ->
+	let nacc,nc = rename_occ acc c in nacc, DOP1(oper,nc)
+    | DOP2(oper,c1,c2) -> 
+	let nacc,nc1 = rename_occ acc c1 in
+        let nacc2,nc2 = rename_occ   nacc c2 in
+        nacc2, DOP2(oper,nc1,nc2) 
+    | DLAM(na,c) -> 
+	let nacc,nc = rename_occ acc c in (nacc, DLAM(na,nc))
+    | DLAMV(na,v) -> 
+	let nacc,nv = vrename_occ acc v in (nacc, DLAMV(na, nv))
+    | x -> acc,x
+  and lrename_occ acc = function
+    | [] -> acc,[]
+    | (t::lt) -> 
+	let nacc,nt = rename_occ acc t in
+        let nacc2,nlt = lrename_occ nacc lt
+        in nacc2,(nt::nlt)
+  and vrename_occ acc v = 
+    let nacc,nl = lrename_occ acc (Array.to_list v)
+    in nacc, Array.of_list nl
+  in 
+  rename_occ acc t
+
+
+let sAPP c n =
+  match c with 
+    | DLAM(na,m) -> subst1 n m
+    | _ -> invalid_arg "SAPP"
+	  
+let sAPPV c n =
+  match c with
+    | DLAMV(na,mV) -> Array.map (subst1 n) mV
+    | _ -> invalid_arg "SAPPV"
+
+let sAPPVi i c n =
+  match c with
+    | DLAMV(na,mV) -> subst1 n mV.(i)
+    | _ -> invalid_arg "SAPPVi"
+
+let sAPPList constr cl = 
+  let rec srec stack = function
+    | (DLAM(_,c), (h::t)) -> srec (h::stack) (c,t)
+    | (c,         [])     -> substl stack c
+    | (_,         _)      -> failwith "SAPPList"
+  in 
+  srec [] (constr,cl) 
+
+let sAPPVList constr cl = 
+  let rec srec stack = function
+    | (DLAM(_,c), (h::t)) -> srec (h::stack) (c,t)
+    | (DLAMV(_,c), [h])   -> Array.map (substl (h::stack)) c
+    | (_,             _)  -> failwith "SAPPVList"
+  in 
+  srec [] (constr,cl) 
+
+let sAPPViList i constr cl= 
+  let rec srec stack = function
+    | (DLAM(_,c), (h::t)) -> srec (h::stack) (c,t)
+    | (DLAMV(_,c), [h])   -> substl (h::stack) c.(i)
+    | (_,             _)  -> failwith "SAPPViList"
+  in 
+  srec [] (constr,cl)
+
+let under_dlams f = 
+  let rec apprec = function 
+    | DLAMV(na,c) -> DLAMV(na,Array.map f c)
+    | DLAM(na,c)  -> DLAM(na,apprec c)
+    | _           -> failwith "under_dlams"
+  in 
+  apprec 
+
+
+(* utility for discharge *)
+type modification_action = ABSTRACT | ERASE
+
+let interp_modif absfun oper (oper',modif) cl = 
+  let rec interprec = function
+    | ([], cl) -> DOPN(oper',Array.of_list cl)
+    | (ERASE::tlm, c::cl) -> interprec (tlm,cl)
+    | (ABSTRACT::tlm, c::cl) -> absfun (interprec (tlm,cl)) c
+    | _ -> assert false
+  in 
+  interprec (modif,cl)
+
+
+type 'a modification =
+  | NOT_OCCUR
+  | DO_ABSTRACT of 'a * modification_action list
+  | DO_REPLACE
+
+let modify_opers replfun absfun oper_alist =
+  let failure () =
+    anomalylabstrm "generic__modify_opers"
+      [< 'sTR"An oper which was never supposed to appear has just appeared" ;
+         'sPC ; 'sTR"Either this is in system code, and you need to" ; 'sPC;
+         'sTR"report this error," ; 'sPC ;
+         'sTR"Or you are using a user-written tactic which calls" ; 'sPC ;
+         'sTR"generic__modify_opers, in which case the user-written code" ;
+         'sPC ; 'sTR"is broken - this function is an internal system" ;
+         'sPC ; 'sTR"for internal system use only" >]
+  in
+  let rec substrec = function
+    | DOPN(oper,cl) as c ->
+	let cl' = Array.map substrec cl in
+	(try
+	   (match List.assoc oper oper_alist with
+	      | NOT_OCCUR -> failure ()
+	      | DO_ABSTRACT (oper',modif) ->
+		  if List.length modif > Array.length cl then
+		    anomaly "found a reference with too few args"
+		  else 
+		    interp_modif absfun oper (oper',modif) (Array.to_list cl')
+	      | DO_REPLACE -> substrec (replfun (DOPN(oper,cl'))))
+	 with 
+	   | Not_found -> DOPN(oper,cl'))
+    | DOP1(i,c) -> DOP1(i,substrec c)
+    | DOPL(oper,cl) -> DOPL(oper,List.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)
+    | x -> x
+  in 
+  if oper_alist = [] then fun x -> x else substrec
+
+let put_DLAMSV lna lc = 
+  match lna with 
+    | [] -> anomaly "put_DLAM"
+    | na::lrest -> List.fold_left (fun c na -> DLAM(na,c)) (DLAMV(na,lc)) lrest
+
+let put_DLAMSV_subst lid lc = 
+  match lid with
+    | [] -> anomaly "put_DLAM"
+    | id::lrest ->  
+        List.fold_left (fun c id' -> DLAM(Name id',subst_var id' c)) 
+          (DLAMV(Name id,Array.map (subst_var id) lc)) lrest
+
+let rec decomp_DLAMV n = function 
+  | DLAM(_,lc)  -> decomp_DLAMV (n-1) lc
+  | DLAMV(_,lc) -> if n = 1 then lc else error "decomp_DLAMV 0"
+  | _           -> error "decomp_DLAMV 1"
+
+let decomp_DLAMV_name n = 
+  let rec decomprec lna n = function 
+    | DLAM(na,lc)  -> decomprec (na::lna) (pred n) lc
+    | DLAMV(na,lc) -> if n = 1 then (na::lna,lc) else error "decomp_DLAMV 0"
+    | _           -> error "decomp_DLAMV 1"
+  in 
+  decomprec [] n 
+
+let decomp_all_DLAMV_name constr = 
+  let rec decomprec lna = function 
+    | DLAM(na,lc)  -> decomprec (na::lna) lc
+    | DLAMV(na,lc) -> (na::lna,lc)
+    | _ -> assert false
+  in 
+  decomprec [] constr
+  
+
+(* [Rel (n+m);...;Rel(n+1)] *)
+
+let rel_vect n m = Array.init m (fun i -> Rel(n+m-i))
+
+let rel_list n m = 
+  let rec reln l p = 
+    if p>m then l else reln (Rel(n+p)::l) (p+1)
+  in 
+  reln [] 1
+
+
+(* Hash-consing *)
+let comp_term t1 t2 =
+  match (t1,t2) with
+    | (DOP0 o1, DOP0 o2) -> o1==o2
+    | (DOP1(o1,t1), DOP1(o2,t2)) -> o1==o2 & t1==t2
+    | (DOP2(o1,t1,u1), DOP2(o2,t2,u2)) -> o1==o2 & t1==t2 & u1==u2
+    | (DOPN(o1,v1), DOPN(o2,v2)) ->
+        (o1==o2) & (Array.length v1 = Array.length v2)
+        & array_for_all2 (==) v1 v2
+    | (DOPL(o1,l1), DOPL(o2,l2)) ->
+        (o1==o2) & (List.length l1 = List.length l2)
+        & List.for_all2 (==) l1 l2
+    | (DLAM(x1,t1), DLAM(x2,t2)) -> x1==x2 & t1==t2
+    | (DLAMV(x1,v1), DLAMV(x2,v2)) ->
+        (x1==x2) & (Array.length v1 = Array.length v2)
+        & array_for_all2 (==) v1 v2
+    | (Rel i, Rel j) -> i=j
+    | (VAR x, VAR y) -> x==y
+    | _ -> false
+
+let hash_term (sh_rec,(sh_op,sh_na,sh_id)) t =
+  match t with
+    | DOP0 o -> DOP0 (sh_op o)
+    | DOP1(o,t) -> DOP1(sh_op o, sh_rec t)
+    | DOP2(o,t1,t2) -> DOP2(sh_op o, sh_rec t1, sh_rec t2)
+    | DOPN(o,v) -> DOPN(sh_op o, Array.map sh_rec v)
+    | DOPL(o,l) -> DOPL(sh_op o, List.map sh_rec l)
+    | DLAM(n,t) -> DLAM(sh_na n, sh_rec t)
+    | DLAMV(n,v) -> DLAMV(sh_na n, Array.map sh_rec v)
+    | Rel i -> t
+    | VAR x -> VAR (sh_id x) 
diff --git a/kernel/generic.mli b/kernel/generic.mli
new file mode 100644
index 0000000000..c9d3dd73df
--- /dev/null
+++ b/kernel/generic.mli
@@ -0,0 +1,116 @@
+
+(* $Id$ *)
+
+open Util
+open Names
+
+exception FreeVar
+exception Occur
+
+type 'oper term =
+  | DOP0 of 'oper                            (* atomic terms *)
+  | DOP1 of 'oper * 'oper term               (* operator of arity 1 *)
+  | DOP2 of 'oper * 'oper term * 'oper term  (* operator of arity 2 *)
+  | DOPN of 'oper * 'oper term array         (* operator of variadic arity *)
+  | DOPL of 'oper * 'oper term list          (* operator of variadic arity *)
+  | DLAM of name * 'oper term                (* deBruijn binder on one term*)
+  | DLAMV of name * 'oper term array         (* deBruijn binder on many terms*)
+  | VAR of identifier                        (* named variable *)
+  | Rel of int                               (* variable as deBruijn index *)
+
+val isRel  : 'a term -> bool
+val isVAR  : 'a term -> bool
+val free_rels : 'a term -> Intset.t
+val closedn : int -> 'a term -> unit
+val closed0 : 'a term -> bool
+val noccurn : int -> 'a term -> bool
+val noccur_bet : int -> int -> 'a term -> bool
+
+
+(* lifts *)
+type lift_spec =
+  | ELID
+  | ELSHFT of lift_spec * int (* ELSHFT(l,n) == lift of n, then apply lift l *)
+  | ELLFT of int * lift_spec  (* ELLFT(n,l)  == apply l to de Bruijn > n *)
+                              (*                 i.e under n binders *)
+val el_shft : int -> lift_spec -> lift_spec
+val el_lift : lift_spec -> lift_spec
+val el_liftn :  int -> lift_spec -> lift_spec
+val reloc_rel: int -> lift_spec -> int
+
+(* explicit substitutions of type 'a *)
+type 'a subs =
+  | ESID                   (* ESID       =          identity *)
+  | CONS of 'a * 'a subs   (* CONS(t,S)  = (S.t)    parallel substitution *)
+  | SHIFT of int * 'a subs (* SHIFT(n,S) = (^n o S) terms in S are relocated *)
+                           (*                        with n vars *)
+  | LIFT of int * 'a subs  (* LIFT(n,S) = (%n S) stands for ((^n o S).n...1) *)
+
+val subs_cons  : 'a * 'a subs -> 'a subs
+val subs_lift  : 'a subs -> 'a subs
+val subs_shft  : int * 'a subs -> 'a subs
+val exp_rel    : int -> int -> 'a subs -> (int * 'a, int) union
+val expand_rel : int -> 'a subs -> (int * 'a, int) union
+
+type info = Closed | Open | Unknown
+type 'a substituend = { mutable sinfo : info; sit : 'a }
+
+val exliftn : lift_spec -> 'a term -> 'a term
+val liftn : int -> int -> 'a term -> 'a term
+val lift : int -> 'a term -> 'a term
+val pop : 'a term -> 'a term
+val lift_substituend : int -> 'a term substituend -> 'a term
+val make_substituend : 'a term -> 'a term substituend
+val substn_many : 'a term substituend array -> int -> 'a term -> 'a term
+val substl : 'a term list -> 'a term -> 'a term
+val subst1 : 'a term -> 'a term -> 'a term
+val occur_opern : 'a -> 'a term -> bool
+val occur_oper0 : 'a -> 'a term -> bool
+val occur_var : identifier -> 'a term -> bool
+val occur_oper : 'a -> 'a term -> bool
+val dependent : 'a term -> 'a term -> bool
+val global_varsl : identifier list -> 'a term -> identifier list
+val global_vars : 'a term -> identifier list
+val global_vars_set : 'a term -> Idset.t
+val subst_var : identifier -> 'a term -> 'a term
+val subst_varn : identifier -> int -> 'a term -> 'a term
+val replace_vars : 
+  (identifier * 'a term substituend) list -> 'a term -> 'a term
+
+val rename_diff_occ : 
+  identifier -> identifier list ->'a term -> identifier list * 'a term 
+
+val sAPP : 'a term -> 'a term -> 'a term
+val sAPPV : 'a term -> 'a term -> 'a term array
+val sAPPVi : int -> 'a term -> 'a term -> 'a term
+
+val sAPPList : 'a term -> 'a term list -> 'a term
+val sAPPVList : 'a term -> 'a term list-> 'a term array
+val sAPPViList : int -> 'a term -> 'a term list -> 'a term
+val under_dlams : ('a term -> 'a term) -> 'a term -> 'a term
+val eq_term : 'a term -> 'a term -> bool
+
+type modification_action = ABSTRACT | ERASE
+
+type 'a modification =
+  | NOT_OCCUR
+  | DO_ABSTRACT of 'a * modification_action list
+  | DO_REPLACE
+
+val modify_opers : ('a term -> 'a term) -> ('a term -> 'a term -> 'a term) 
+  -> ('a * 'a modification) list -> 'a term -> 'a term
+
+val put_DLAMSV : name list -> 'a term array -> 'a term
+val decomp_DLAMV : int -> 'a term -> 'a term array
+val decomp_DLAMV_name : int -> 'a term -> name list * 'a term array
+val decomp_all_DLAMV_name : 'a term -> name list * 'a term array
+val put_DLAMSV_subst : identifier list -> 'a term array -> 'a term
+val rel_vect : int -> int -> 'a term array
+val rel_list : int -> int -> 'a term list
+
+(* For hash-consing use *)
+val hash_term :
+  ('a term -> 'a term)
+  * (('a -> 'a) * (name -> name) * (identifier -> identifier))
+  -> 'a term -> 'a term
+val comp_term : 'a term -> 'a term -> bool
diff --git a/kernel/names.ml b/kernel/names.ml
index af7f1f7195..e9de197fea 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -65,6 +65,14 @@ let id_ord id1 id2 =
 
 let id_without_number id = id.index = (-1)
 
+module IdOrdered = 
+  struct
+    type t = identifier
+    let compare = id_ord
+  end
+
+module Idset = Set.Make(IdOrdered)
+
 
 (* Fresh names *)
 
@@ -105,6 +113,9 @@ let get_new_ids n id lids  =
   in 
   get_rec n []
 
+let id_of_name default = function
+  | Name s -> s
+  | Anonymous -> default
 
 (* Kinds *)
 
@@ -199,6 +210,8 @@ module SpOrdered =
 
 module Spset = Set.Make(SpOrdered)
 
+module Spmap = Map.Make(SpOrdered)
+
 (* Hash-consing of name objects *)
 module Hident = Hashcons.Make(
   struct 
diff --git a/kernel/names.mli b/kernel/names.mli
index 5445065f7a..5d8791ba97 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -18,6 +18,7 @@ val index_of_id : identifier -> int
 val id_ord : identifier -> identifier -> int
 val id_without_number : identifier -> bool
 
+module Idset : Set.S with type elt = identifier
 
 val lift_ident : identifier -> identifier
 val next_ident_away_from : identifier -> identifier list -> identifier
@@ -27,6 +28,7 @@ val next_name_away_with_default :
   string -> name -> identifier list -> identifier
 val get_new_ids : int -> identifier -> identifier list -> identifier list
 
+val id_of_name : identifier -> name -> identifier
 
 type path_kind = CCI | FW | OBJ
 
@@ -58,6 +60,7 @@ val sp_ord : section_path -> section_path -> int
 val sp_gt : section_path * section_path -> bool
 
 module Spset : Set.S with type elt = section_path
+module Spmap : Map.S with type key = section_path
 
 (* Hash-consing *)
 val hcons_names : unit ->
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 7aa3f75e9a..35731c7341 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -3,6 +3,8 @@
 
 open Names
 open Util
+open Generic
+open Term
 
 (* Signatures *)
 
@@ -139,6 +141,28 @@ let prepend_sign gamma1 gamma2 =
   else
     invalid_arg "prepend_sign"
 
+let dunbind default sign ty = function 
+  | DLAM(na,c) ->
+      let id = next_ident_away (id_of_name default na) (ids_of_sign sign) in
+      (add_sign (id,ty) sign, subst1 (VAR id) c)
+  | _ -> invalid_arg "dunbind default"
+
+let dunbindv default sign ty = function
+  | DLAMV(na,c) ->
+      let id = next_ident_away (id_of_name default na) (ids_of_sign sign) in 
+      (add_sign (id,ty) sign,Array.map (subst1 (VAR id)) c)
+  | _ -> invalid_arg "dunbindv default"
+
+let dbind sign c =
+  let (id,ty) = hd_sign sign
+  and sign' = tl_sign sign in
+  (ty,DLAM(Name id,subst_var id c))
+
+let dbindv sign cl =
+  let (id,ty) = hd_sign sign
+  and sign' = tl_sign sign in
+  (ty,DLAMV(Name id,Array.map (subst_var id) cl))
+
 
 (* Signatures + de Bruijn environments *)
 
@@ -207,3 +231,7 @@ let lookup_id id env =
   with 
     | Not_found -> let (x,y) = lookup_glob id env in GLOBNAME(x,y)
 
+
+type 'b assumptions = (type_judgment,'b) env
+type environment = (type_judgment,type_judgment) env
+type context = type_judgment signature
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 2cbab3672d..b07fcd0310 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -2,6 +2,8 @@
 (* $Id$ *)
 
 open Names
+open Generic
+open Term
 
 type 'a signature = identifier list * 'a list
 type 'a db_signature = (name * 'a) list
@@ -40,6 +42,13 @@ val add_sign_replacing :
   identifier -> (identifier * 'a) -> 'a signature -> 'a signature
 val prepend_sign : 'a signature -> 'a signature -> 'a signature
 
+val dunbind : identifier -> 'a signature -> 'a -> 'b term 
+  -> 'a signature * 'b term
+val dunbindv : identifier -> 'a signature -> 'a -> 'b term 
+  -> 'a signature * 'b term array
+val dbind : 'a signature -> 'b term -> 'a * 'b term
+val dbindv : 'a signature -> 'b term array -> 'a * 'b term
+
 
 val gLOB : 'b signature -> ('b,'a) env
 
@@ -66,3 +75,6 @@ type ('b,'a) search_result =
 val lookup_id : identifier -> ('b,'a) env -> ('b,'a) search_result
 
 
+type 'b assumptions = (type_judgment,'b) env
+type environment = (type_judgment,type_judgment) env
+type context = type_judgment signature
diff --git a/kernel/term.ml b/kernel/term.ml
new file mode 100644
index 0000000000..0e8a8cdaaf
--- /dev/null
+++ b/kernel/term.ml
@@ -0,0 +1,1489 @@
+
+(* $Id$ *)
+
+(* This module instanciates the structure of generic deBruijn terms to Coq *)
+
+open Util
+open Pp
+open Names
+open Generic
+open Univ
+
+(* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *)
+
+type 'a oper = 
+  (* DOP0 *)
+  | Meta of int
+  | Sort of 'a
+  | Implicit
+  (* DOP2 *)
+  | Cast | Prod | Lambda
+  (* DOPN *)
+  | AppL | Const of section_path | Abst of section_path
+  | MutInd of section_path * int
+  | MutConstruct of (section_path * int) * int
+  | MutCase of case_info
+  | Fix of int array * int
+  | CoFix of int
+
+  | XTRA of string * Coqast.t list
+      (* an extra slot, for putting in whatever sort of
+         operator we need for whatever sort of application *)
+
+and case_info = (section_path * int) option
+
+(* 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
+      
+let mk_Set  = Prop Pos
+let mk_Prop = Prop Null
+
+type constr = sorts oper term
+
+type 'a judge = { body : constr; typ : 'a }
+
+type type_judgment = sorts judge
+type term_judgment = type_judgment judge
+
+type conv_pb = CONV | CONV_LEQ | CONV_X | CONV_X_LEQ
+
+(****************************************************************************)
+(*              Functions for dealing with constr terms                     *)
+(****************************************************************************)
+
+(*********************)
+(* Term constructors *)
+(*********************)
+
+(* Constructs a DeBrujin index with number n *)
+let mkRel   n = (Rel n)
+
+(* Constructs an existential variable named "?" *)
+let mkExistential = (DOP0 (XTRA ("ISEVAR",[])))
+
+(* Constructs an existential variable named "?n" *)
+let mkMeta  n =  DOP0 (Meta n)
+
+(* Constructs a Variable named id *)
+let mkVar id = VAR id
+
+(* Construct an XTRA term (XTRA is an extra slot for whatever you want) *)
+let mkXtra s astlist = (DOP0 (XTRA (s, astlist)))
+
+(* 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 prop = Prop Null
+and spec = Prop Pos
+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))
+
+(* Constructs the product (x:t1)t2 *)
+let mkProd x t1 t2 = (DOP2 (Prod,t1,(DLAM (x,t2))))
+
+(* non-dependant product t1 -> t2 *)
+let mkArrow t1 t2 = mkProd Anonymous t1 t2
+
+(* named product *)
+let mkNamedProd name typ c = mkProd (Name name) typ (subst_var name c)
+
+(* Constructs the abstraction [x:t1]t2 *)
+let mkLambda x t1 t2 = (DOP2 (Lambda,t1,(DLAM (x,t2))))
+let mkNamedLambda name typ c = mkLambda (Name name) typ (subst_var name c)
+
+(* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *)
+let mkAppL a    = DOPN (AppL, a)
+let mkAppList l   = DOPN (AppL, Array.of_list l)
+
+(* Constructs a constant *) 
+(* The array of terms correspond to the variables introduced in the section *)
+let mkConst sp a = DOPN (Const  sp, a)
+
+(* Constructs an abstract object *)
+let mkAbst sp a = DOPN (Abst sp, a)
+
+(* 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 sp i l = (DOPN (MutInd (sp,i), l))
+
+(* 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 sp i j l =  (DOPN ((MutConstruct ((sp,i),j),l))) 
+
+(* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
+let mkMutCase ci p c ac = DOPN (MutCase ci,Array.append [|p;c|] (Array.of_list ac))
+let mkMutCaseA ci p c ac = DOPN (MutCase ci,Array.append [|p;c|] ac)
+
+(* If recindxs = [|i1,...in|] 
+      typarray = [|t1,...tn|]
+      funnames = [f1,.....fn]
+      bodies   = [b1,.....bn]
+   then    
+
+      mkFix recindxs i typarray funnames bodies
+   
+   constructs 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.
+
+   Warning: as an invariant the ti are casted during the Fix formation;
+   these casts are then used by destFix
+*)
+let in_fixcast {body=b; typ=s} = DOP2 (Cast, b, DOP0 (Sort s))
+
+(* Here, we assume the body already constructed *)
+let mkFixDlam recindxs i jtypsarray body =
+  let typsarray = Array.map in_fixcast jtypsarray in
+  DOPN (Fix (recindxs,i),Array.append typsarray body)
+
+let mkFix recindxs i jtypsarray funnames bodies = 
+  let rec wholebody l = 
+    match l with 
+      | [h]    -> (DLAMV (h,bodies)) 
+      | (x::l) -> (DLAM  (x, wholebody l))
+      | [] -> anomaly "in Term.mkFix : empty list of funnames"
+  in 
+  mkFixDlam recindxs i jtypsarray [|(wholebody funnames)|]
+
+(* If typarray = [|t1,...tn|]
+      funnames = [f1,.....fn]
+      bodies   = [b1,.....bn]
+   then
+
+      mkCoFix i typsarray funnames bodies 
+
+   constructs the ith function of the block  
+   
+    CoFixpoint f1 = b1
+    with       f2 = b2
+    ...
+    with       fn = bn.
+
+*)
+(* Here, we assume the body already constructed *)
+let mkCoFixDlam i jtypsarray body =
+  let typsarray = Array.map in_fixcast 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"
+
+let isMETA = function DOP0(Meta _) -> true | _ -> false
+
+(* Destructs a variable *)
+let destVar = function
+  | (VAR id) -> id
+  | _ -> invalid_arg "destVar"
+
+(* Destructs an XTRA *)
+let destXtra = function
+  | DOP0 (XTRA (s,astlist)) -> (s,astlist)
+  | _ -> invalid_arg "destXtra"
+
+(* Destructs a type *)
+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 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 cast_term = function
+  | DOP2(Cast,c,t) -> c
+  | _ -> anomaly "found a type which did not contain a cast (cast_term)"
+
+let cast_type = function
+  | DOP2(Cast,c,t) -> t
+  | _ -> anomaly "found a type which did not contain a cast (cast_type)"
+
+let rec strip_outer_cast = function
+  | DOP2(Cast,c,_) -> strip_outer_cast c
+  | c -> c
+
+(* Destructs the product (x:t1)t2 *)
+let destProd = function 
+  | DOP2 (Prod, t1, (DLAM (x,t2))) -> (x,t1,t2) 
+  | _ -> invalid_arg "destProd"
+
+let rec hd_of_prod prod =
+  match strip_outer_cast prod with
+    | DOP2(Prod,c,DLAM(n,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 
+  | DOP2 (Lambda, t1, (DLAM (x,t2))) -> (x,t1,t2) 
+  | _ -> invalid_arg "destLambda"
+
+(* Destructs an application *)
+let destAppL = function 
+  | (DOPN (AppL,a)) -> a
+  | _ -> invalid_arg "destAppL"
+
+let isAppL = function DOPN(AppL,_) -> true | _ -> false
+
+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 abstract term *)
+let destAbst = function
+  | DOPN (Abst sp, a) -> (sp, a)
+  | _ -> invalid_arg "destAbst"  
+
+let path_of_abst = function
+  | DOPN(Abst sp,_) -> sp
+  | _ -> anomaly "path_of_abst called with bad args"
+
+let args_of_abst = function
+  | DOPN(Abst _,args) -> args
+  | _ -> anomaly "args_of_abst called with bad args"
+
+(* Destructs a (co)inductive type named sp *)
+let destMutInd = function
+  | DOPN (MutInd (sp,i), l) -> (sp,i,l)
+  | _ -> invalid_arg "destMutInd"
+	
+let op_of_mind = function
+  | DOPN(MutInd (sp,i),_) -> (sp,i)
+  | _ -> 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"
+
+let ci_of_mind = function
+  | DOPN(MutInd(sp,tyi),_) -> Some (sp,tyi)
+  | _ -> invalid_arg "ci_of_mind"
+
+(* Destructs a constructor *)
+let destMutConstruct = function
+  | DOPN (MutConstruct ((sp,i),j),l) -> (sp,i,j,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 out_fixcast = function
+  | DOP2 (Cast, b, DOP0 (Sort s)) -> { body = b; typ = s }
+  | _ -> anomaly "destFix: malformed recursive definition"
+
+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,Array.map out_fixcast types,funnames,bodies)
+  | _ -> invalid_arg "destFix"
+	
+let destCoFix = function 
+  | DOPN ((CoFix i),a) ->
+      let (types,funnames,bodies) = destGralFix a in
+      (i,Array.map out_fixcast types,funnames,bodies)
+  | _ -> invalid_arg "destCoFix"
+
+(* Provisoire, le temps de maitriser les cast *)
+let destUntypedFix = function 
+  | DOPN (Fix (recindxs,i),a) -> 
+      let (types,funnames,bodies) = destGralFix a in 
+      (recindxs,i,types,funnames,bodies)
+  | _ -> invalid_arg "destFix"
+
+let destUntypedCoFix = function 
+  | DOPN (CoFix i,a) -> 
+      let (types,funnames,bodies) = destGralFix a in 
+      (i,types,funnames,bodies)
+  | _ -> invalid_arg "destCoFix"
+
+
+(******************)
+(* Term analysis  *)
+(******************)
+
+type kindOfTerm = 
+  | IsRel            of int
+  | IsMeta           of int
+  | IsVar            of identifier
+  | IsXtra           of string * (Coqast.t list)
+  | IsSort           of sorts
+  | IsImplicit       
+  | IsCast           of constr*constr
+  | IsProd           of name*constr*constr
+  | IsLambda         of name*constr*constr
+  | IsAppL           of constr array
+  | IsConst          of section_path*constr array 
+  | IsAbst           of section_path*constr array
+  | IsMutInd         of section_path*int*constr array 
+  | IsMutConstruct   of section_path*int*int*constr array 
+  | IsMutCase        of case_info*constr*constr*(constr array)
+  | IsFix            of (int array)*int*
+                        (constr array)*(name list)*(constr array)
+  | IsCoFix          of int*(constr array) *
+                        (name list)*(constr array)
+
+
+(* 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, astlist))             -> IsXtra (s,astlist)
+    | DOP0 Implicit                        -> IsImplicit
+    | DOP2 (Cast, t1, t2)                  -> IsCast   (t1,t2)
+    | DOP2 (Prod, t1, (DLAM (x,t2)))       -> IsProd (x,t1,t2) 
+    | DOP2 (Lambda, t1, (DLAM (x,t2)))     -> IsLambda (x,t1,t2)
+    | DOPN (AppL,a)                        -> IsAppL a
+    | DOPN (Const  sp, a)                  -> IsConst (sp,a)
+    | DOPN (Abst sp, a)                    -> IsAbst (sp, a)
+    | DOPN (MutInd (sp,i), l)              -> IsMutInd (sp,i,l)
+    | DOPN (MutConstruct ((sp,i), j),l)    -> IsMutConstruct (sp,i,j,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 (types,funnames,bodies) = destGralFix a in
+	IsFix (recindxs,i,types,funnames,bodies)
+    | DOPN ((CoFix i),a)                    ->  
+      	let (types,funnames,bodies) = destGralFix a in
+      	IsCoFix (i,types,funnames,bodies)
+    | _ -> errorlabstrm "Term.kind_of_term" [< 'sTR "ill-formed constr" >]
+
+(***************************)
+(* Other term constructors *)
+(***************************)
+
+let abs_implicit c = mkLambda Anonymous mkImplicit c
+let lambda_implicit a = mkLambda (Name(id_of_string"y")) mkImplicit a
+let lambda_implicit_lift n a = iterate lambda_implicit n (lift n a)
+
+(* prod_it b [x1:T1;..xn:Tn] = (x1:T1)..(xn:Tn)b *)
+let prod_it = List.fold_left (fun c (n,t)  -> mkProd n t c)
+
+(* lam_it b [x1:T1;..xn:Tn] = [x1:T1]..[xn:Tn]b *)
+let lam_it = List.fold_left (fun c (n,t)  -> mkLambda n t c)
+
+(* prodn n ([x1:T1]..[xn:Tn]Gamma) b = (x1:T1)..(xn:Tn)b *)
+let prodn n env b =
+  let rec prodrec = function
+    | (0, env, b)        -> b
+    | (n, ((v,t)::l), b) -> prodrec (n-1,  l, DOP2(Prod,t,DLAM(v,b)))
+    | _ -> assert false
+  in 
+  prodrec (n,env,b)
+
+(* lamn n ([x1:T1]..[xn:T]Gamma) b = [x1:T1]..[xn:Tn]b *)
+let lamn n env b =
+  let rec lamrec = function
+    | (0, env, b)        -> b
+    | (n, ((v,t)::l), b) -> lamrec (n-1,  l, DOP2(Lambda,t,DLAM(v,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)
+	    
+and appvectc f l = appvect (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 *)
+let rec to_lambda n prod =
+  if n=0 then 
+    prod 
+  else 
+    match prod with 
+      | DOP2(Prod,ty,DLAM(na,bd)) -> 
+          DOP2(Lambda,ty,DLAM(na, to_lambda (n-1) bd))
+      | DOP2(Cast,c,_) -> to_lambda n c
+      | _   -> errorlabstrm "to_lambda" [<>]                      
+
+let rec to_prod n lam =
+  if n=0 then 
+    lam
+  else   
+    match lam with 
+      | DOP2(Lambda,ty,DLAM(na,bd)) -> 
+          DOP2(Prod,ty,DLAM(na, to_prod (n-1) bd))
+      | DOP2(Cast,c,_) -> to_prod n c
+      | _   -> errorlabstrm "to_prod" [<>]                      
+	    
+(* pseudo-reduction rule:
+ * [prod_app  s (Prod(_,B)) N --> B[N]
+ * with an strip_outer_cast on the first argument to produce a product.
+ * if this does not work, then we use the string S as part of our
+ * error message.
+ *)
+
+let prod_app s t n =
+  match strip_outer_cast t with
+    | DOP2(Prod,_,b) -> sAPP b n
+    | _ ->
+	errorlabstrm s [< 'sTR"Needed a product, but didn't find one in " ;
+			  'sTR s ; 'fNL >]
+
+
+(* prod_appvect s T [| a1 ; ... ; an |] -> (T a1 ... an) *)
+let prod_appvect s t nL = Array.fold_left (prod_app s) t nL
+
+(* prod_applist s T [ a1 ; ... ; an ] -> (T a1 ... an) *)
+let prod_applist s t nL = List.fold_left (prod_app s) t nL
+
+
+(*********************************)
+(* Other term destructors        *)
+(*********************************)
+
+(* 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
+    | DOP2(Prod,t,DLAM(x,c)) -> prodec_rec ((x,t)::l) c
+    | DOP2(Cast,c,_)         -> prodec_rec l c
+    | c                      -> l,c
+  in 
+  prodec_rec [] 
+
+(* 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
+    | DOP2(Lambda,t,DLAM(x,c)) -> lamdec_rec ((x,t)::l) c
+    | DOP2(Cast,c,_)         -> lamdec_rec l c
+    | c                      -> l,c
+  in 
+  lamdec_rec [] 
+
+(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T 
+   into the pair ([(xn,Tn);...;(x1,T1)],T) *)
+let decompose_prod_n n =
+  if n < 0 then 
+    error "decompose_prod_n: integer parameter must be positive"
+  else
+    let rec prodec_rec l n c = 
+      if n=0 then l,c 
+      else match c with 
+	| DOP2(Prod,t,DLAM(x,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"
+    in 
+    prodec_rec [] n 
+
+(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T 
+   into the pair ([(xn,Tn);...;(x1,T1)],T) *)
+let decompose_lam_n n =
+  if n < 0 then
+    error "decompose_lam_n: integer parameter must be positive"
+  else 
+    let rec lamdec_rec l n c = 
+      if n=0 then l,c 
+      else match c with 
+        | DOP2(Lambda,t,DLAM(x,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"
+    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
+    | DOP2(Lambda,_,DLAM(_,c)) -> nbrec (n+1) c
+    | DOP2(Cast,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
+    | DOP2(Prod,_,DLAM(_,c)) -> nbrec (n+1) c
+    | DOP2(Cast,c,_) -> nbrec n c
+    | _ -> n
+  in 
+  nbrec 0
+
+(********************************************************************)
+(*   various utility functions for implementing terms with bindings *)
+(********************************************************************)
+
+let extract_lifted (n,x) = lift n x
+let insert_lifted x = (0,x)
+
+(* l is a list of pairs (n:nat,x:constr), env is a stack of (na:name,T:constr)
+   push_and_lift adds a component to env and lifts l one step *)
+let push_and_lift (na,t) env l =
+  ((na,t)::env, List.map (fun (n,x) -> (n+1,x)) l)
+
+
+(* if T is not (x1:A1)(x2:A2)....(xn:An)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 *)
+let push_and_liftl n env t l = 
+  let rec pushrec n t (env,l) =
+    match (n,t) with
+      | (0, _) -> (env,t,l)
+      | (_, DOP2(Prod,t,DLAM(na,b))) -> 
+          pushrec (n-1) b (push_and_lift (na,t) env l)
+      | (_, DOP2(Cast,t,_)) -> pushrec n t (env,l)
+      | _ -> error "push_and_liftl"
+  in 
+  pushrec n t (env,l)
+
+(* if T is not (x1:A1)(x2:A2)....(xn:An)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 *)
+let push_lam_and_liftl n env t l = 
+  let rec pushrec n t (env,l) =
+    match (n,t) with
+      | (0, _) -> (env,t,l)
+      | (_, DOP2(Lambda,t,DLAM(na,b))) -> 
+	  pushrec (n-1) b (push_and_lift (na,t) env l)
+      | (_, DOP2(Cast,t,_)) -> pushrec n t (env,l)
+      | _ -> error "push_lam_and_liftl"
+  in 
+  pushrec n t (env,l)
+
+(* l is a list of pairs (n:nat,x:constr), tlenv is a stack of
+(na:name,T:constr), B : constr, na : name
+(prod_and_pop ((na,T)::tlenv) B l) gives (tlenv, (na:T)B, l')
+where l' is l lifted down one step *)
+let prod_and_pop env b l =
+  match env with
+    | [] -> error "prod_and_pop"
+    | (na,t)::tlenv ->
+        (tlenv,DOP2(Prod,t,DLAM(na,b)),
+         List.map (function 
+                       (0,x) -> (0,lift (-1) x)
+                     | (n,x) -> (n-1,x)) l)
+
+(* recusively applies prod_and_pop :
+if env = [na1:T1 ; na2:T2 ; ... ; nan:Tn]@tlenv
+then
+(prod_and_popl n env T l) gives (tlenv,(nan:Tn)...(na1:Ta1)T,l') where
+l' is l lifted down n steps *)
+let prod_and_popl n env t l = 
+  let rec poprec = function
+    | (0, (env,b,l)) -> (env,b,l)
+    | (n, ([],_,_))  -> error "prod_and_popl"
+    | (n, (env,b,l)) -> poprec (n-1, prod_and_pop env b l)
+  in 
+  poprec (n,(env,t,l))
+
+(* similar to prod_and_pop, but gives [na:T]B intead of (na:T)B *)
+let lam_and_pop env b l =
+  match env with
+    | [] -> error "lam_and_pop"
+    | (na,t)::tlenv ->
+        (tlenv,DOP2(Lambda,t,DLAM(na,b)),
+         List.map (function
+                       (0,x) -> (0,lift (-1) x)
+                     | (n,x) -> (n-1,x)) l)
+
+(* similar to lamn_and_pop but generates new names whenever the name is 
+ *  Anonymous *)
+let lam_and_pop_named env body l acc_ids =
+  match env with
+    | [] -> error "lam_and_pop"
+    | (na,t)::tlenv ->
+ 	let id = match na with
+	  | Anonymous -> next_ident_away (id_of_string "a") acc_ids
+	  | Name id -> id
+	in
+	(tlenv,DOP2(Lambda,t,DLAM((Name id),body)),
+         List.map (function
+                     | (0,x) -> (0,lift (-1) x)
+                     | (n,x) -> (n-1,x)) l,
+         (id::acc_ids))
+
+(* similar to prod_and_popl but gives [nan:Tan]...[na1:Ta1]B instead of
+ * (nan:Tan)...(na1:Ta1)B *)
+let lam_and_popl n env t l = 
+  let rec poprec = function
+    | (0, (env,b,l)) -> (env,b,l)
+    | (n, ([],_,_)) -> error "lam_and_popl"
+    | (n, (env,b,l)) -> poprec (n-1, lam_and_pop env b l)
+  in 
+  poprec (n,(env,t,l))
+
+(* similar to prod_and_popl but gives [nan:Tan]...[na1:Ta1]B instead of
+ * but it generates names whenever nai=Anonymous *)
+
+let lam_and_popl_named  n env t l = 
+  let rec poprec = function
+    | (0, (env,b,l,_)) -> (env,b,l)
+    | (n, ([],_,_,_)) -> error "lam_and_popl"
+    | (n, (env,b,l,acc_ids)) -> poprec (n-1, lam_and_pop_named env b l acc_ids)
+  in 
+  poprec (n,(env,t,l,[]))
+
+(* [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 *)
+let lambda_ize n t endpt =
+  let env = [] 
+  and carry = [insert_lifted endpt] in
+  let env, endpt = 
+    match push_and_liftl n env t carry with
+      | (env,_,[endpt]) ->   env, endpt
+      | _ -> anomaly "bud in Term.lamda_ize" 
+  in
+  let t = extract_lifted endpt in
+  match lam_and_popl n env t [] with
+    | (_,t,[]) -> t
+    | _ -> anomaly "bud in Term.lamda_ize"
+	  
+let sort_hdchar = function
+  | Prop(_) -> "P"
+  | Type(_) -> "T"
+
+let pb_is_univ_adjust pb =
+  pb = CONV or pb = CONV_LEQ
+
+let pb_is_equal pb =
+  pb = CONV or pb = CONV_X
+
+let pb_equal = function
+  | CONV_LEQ -> CONV
+  | CONV_X_LEQ -> CONV_X
+  | pb -> pb
+
+(* Level comparison for information extraction : Prop <= Type *)
+let le_kind l m = (isprop l) or (is_Type m)
+
+let le_kind_implicit k1 k2 = 
+  (k1=mkImplicit) or (isprop k1) or (k2=mkImplicit) or (is_Type 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)
+      in 
+      collapse_rec (array_hd cl, array_list_of_tl cl)
+  | c -> 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,[])
+
+(* strips head casts and flattens head applications *)
+let 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)
+      in 
+      collapse_rec(array_hd cl, array_app_tl cl [])
+  | c -> c
+
+(* (occur_const (s:section_path) c) -> true if constant s occurs in c,
+ * false otherwise *)
+let occur_const s = occur_opern (Const s)
+
+(* 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 ;
+
+   - 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.
+
+   NOTE : the case of DOPL is not handled...
+*)
+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_map_to_list make_substituend 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)
+    | x                 -> x
+  in 
+  if const_alist = [] then function x -> x else substrec
+
+(* NOTE : the case of DOPL is not handled by whd_castapp_stack *)
+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
+  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 [])
+
+
+(***************************************)
+(*  alpha and eta conversion functions *)                         
+(***************************************)
+
+(* alpha conversion : ignore print names and casts *)
+let rec eq_constr_rec m n = 
+  if m = n then true else
+  match (strip_head_cast m,strip_head_cast n) with
+    | (DOP2(Cast,c1,_),c2) 	       -> eq_constr_rec c1 c2
+    | (c1,DOP2(Cast,c2,_))              -> eq_constr_rec c1 c2
+    | (Rel p1,Rel p2)                   -> p1=p2
+    | (DOPN(oper1,cl1),DOPN(oper2,cl2)) ->
+        oper1=oper2 & array_for_all2 eq_constr_rec cl1 cl2
+    | (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
+    | _ -> false
+
+let eq_constr = eq_constr_rec
+
+let rec eq_constr_with_meta_rec m n=
+  (m=n) or 
+  (match (strip_head_cast m,strip_head_cast n) with
+     | (DOP2(Cast,c1,_),c2) 	       -> eq_constr_rec c1 c2
+     | (c1,DOP2(Cast,c2,_))              -> eq_constr_rec c1 c2
+     | (Rel p1,Rel p2)                   -> p1=p2
+     | (DOPN(oper1,cl1),DOPN(oper2,cl2)) ->
+         oper1=oper2 & array_for_all2 eq_constr_rec cl1 cl2
+     | (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
+     | _ -> false)
+
+(* 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
+    | DOP2(Lambda,c1,DLAM(_,c')) ->
+	(match eta_reduce_head c' with
+           | DOPN(AppL,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 (Rel 1) c'))) 
+                        then lift (-1) c'
+                        else c
+                    | _     -> c)
+           | _ -> c)
+    | _ -> c
+
+(* alpha-eta conversion : ignore print names and casts *)
+
+let rec eta_eq_constr 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) -> eta_eq_constr c1 c2
+    | (c1,DOP2(Cast,c2,_)) -> eta_eq_constr c1 c2
+    | (Rel p1,Rel p2)                   -> p1=p2
+    | (DOPN(oper1,cl1),DOPN(oper2,cl2)) ->
+	oper1=oper2 & array_for_all2 eta_eq_constr cl1 cl2
+    | (DOP0 oper1,DOP0 oper2)                 -> oper1=oper2
+    | (DOP1(i,c1),DOP1(j,c2)) -> (i=j) & eta_eq_constr c1 c2
+    | (DOP2(i,c1,c1'),DOP2(j,c2,c2')) ->
+	(i=j) & eta_eq_constr c1 c2 & eta_eq_constr c1' c2'
+    | (DLAM(_,c1),DLAM(_,c2)) -> eta_eq_constr c1 c2
+    | (DLAMV(_,cl1),DLAMV(_,cl2)) -> array_for_all2 eta_eq_constr cl1 cl2
+    | _ -> false
+
+
+(* This renames bound variablew with fresh and distinct names *)
+(* in such a way that the printer doe not generate new names  *)
+(* and therefore that printed names are the intern names      *)
+(* In this way, tactics such as Induction works well          *)
+
+let rec rename_bound_var l = function
+  | DOP2(Prod,c1,DLAM(Name(s),c2))  ->
+      if dependent (Rel 1) c2 then
+        let s' = next_ident_away s (global_vars c2@l) in
+        DOP2(Prod,c1,DLAM(Name(s'),rename_bound_var (s'::l) c2))
+      else 
+	DOP2(Prod,c1,DLAM(Name(s),rename_bound_var l c2))
+  | DOP2(Prod,c1,DLAM(Anonymous,c2)) ->
+      DOP2(Prod,c1,DLAM(Anonymous,rename_bound_var l c2))
+  | DOP2(Cast,c,t) -> DOP2(Cast,rename_bound_var l c,t)
+  |  x -> x
+
+(***************************)
+(*  substitution functions *)                         
+(***************************)
+
+(* 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 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))))
+	else 
+	  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 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))))
+	else 
+	  None
+  | (_,_) -> None
+
+(* Used in trad and progmach *)
+let rec rename_rels curidx sofar = function
+  | [] -> sofar
+  | ((id,Rel n)::tl as l) ->
+      if curidx = n then
+	rename_rels (curidx+1) (subst1 (VAR id) sofar) tl
+      else 
+	rename_rels (curidx+1) (subst1 (DOP0 Implicit) sofar) l
+  | _ -> assert false
+
+let sort_increasing_snd = 
+  Sort.list 
+    (fun x y -> match x,y with 
+	 (_,Rel m),(_,Rel n) -> m < n
+       | _ -> assert false)
+
+let clean_rhs rhs worklist =
+  let workvars = List.filter (compose isVAR snd) worklist in
+  let rhs' =
+    replace_vars
+      (List.map (fun (id',v) -> let id = destVar v in 
+		 (id,{sinfo=Closed; sit=VAR id'})) 
+	 workvars)
+      rhs 
+  in
+  let workrels = List.filter (compose isRel snd) worklist in
+  let workrels' = sort_increasing_snd workrels in
+  rename_rels 1 rhs' workrels'
+
+(* Recognizing occurrences of a given subterm in a term for Pattern :
+   (subst_term c t) substitutes (Rel 1) for all occurrences of term c 
+   in a (closed) term t *)
+
+let subst_term c t = 
+  let rec substrec k c t =
+    match prefix_application k c t with
+      | Some x -> x
+      | None ->
+	  (if eq_constr 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)
+	     | _ -> t)
+  in 
+  substrec 1 c t
+
+(* same as subst_term, but modulo eta *)
+
+let subst_term_eta_eq c t = 
+  let rec substrec k c t =
+    match prefix_application_eta k c t with
+      | Some x -> x
+      | None ->
+	  (if eta_eq_constr t c then Rel(k) else match t with
+	     | DOPN(Const sp,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)
+	     | _ -> t)
+  in 
+  substrec 1 c t
+
+(* bl : (int,constr) Listmap.t = (int * constr) list *)
+(* c : constr *)
+(* for each binding (i,c_i) in bl, substitutes the metavar i by c_i in c *)
+(* Raises Not_found if c contains a meta that is not in the association list *)
+
+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')
+    | _ -> c
+  
+(***************************)
+(* occurs check functions  *)                         
+(***************************)
+
+let rec occur_meta = function
+  | DOP2(Prod,t,DLAM(_,c))   -> (occur_meta t) or (occur_meta c)
+  | DOP2(Lambda,t,DLAM(_,c)) -> (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 rel_vect = (Generic.rel_vect : int -> int -> constr array)
+		 
+(* Transforms a constr into a matchable constr*)
+let rec matchable=function
+  | DOP1(op,t) ->
+      DOP1(op,matchable t)
+  | DOP2(op,t1,t2) ->
+      DOP2(op,matchable t1,matchable t2)
+  | DOPN(op,tab) ->
+      (match op with
+         | MutInd(sp,rk) ->
+             DOPL(XTRA("IT",[Coqast.Id((rk,0),string_of_path sp)]),
+		  Array.to_list (Array.map matchable tab))
+         | MutConstruct((sp,rkt),rkc) ->
+             DOPL(XTRA("IC",[Coqast.Id((rkt,rkc),string_of_path sp)]),
+		  Array.to_list (Array.map matchable tab))
+         | Const sp ->
+             DOPL(XTRA("C",[Coqast.Id((0,0),string_of_path sp)]),
+		  Array.to_list (Array.map matchable tab))
+         | a ->
+             DOPL(a,Array.to_list (Array.map matchable tab)))
+  | DOPL(op,lst) ->
+      DOPL(op,List.map matchable lst)
+  | DLAM(ne,t) ->
+      DLAM(ne,matchable t)
+  | DLAMV(ne,tab) ->
+      DLAMV(ne,(Array.map matchable tab))
+  | a -> a
+
+let rec unmatchable=function
+  | DOP1(op,t) ->
+      DOP1(op,unmatchable t)
+  | DOP2(op,t1,t2) ->
+      DOP2(op,unmatchable t1,unmatchable t2)
+  | DOPN(op,tab) ->
+      DOPN(op,Array.map unmatchable tab)
+  | DOPL(op,lst) ->
+      (match op with
+         | XTRA("IT",[Coqast.Id((rk,0),str)]) ->
+             DOPN(MutInd(path_of_string str,rk),
+		  Array.of_list (List.map unmatchable lst))
+         | XTRA("IC",[Coqast.Id((rkt,rkc),str)]) ->
+             DOPN(MutConstruct((path_of_string str,rkt),rkc),
+		  Array.of_list (List.map unmatchable lst))
+         | XTRA("C",[Coqast.Id((0,0),str)]) ->
+             DOPN(Const(path_of_string str),
+		  Array.of_list (List.map unmatchable lst))
+         | a ->
+             DOPN(a,Array.of_list (List.map unmatchable lst)))
+  | DLAM(ne,t) ->
+      DLAM(ne,unmatchable t)
+  | DLAMV(ne,tab) ->
+      DLAMV(ne,(Array.map unmatchable tab))
+  | a -> a
+
+(***************************)
+(* hash-consing functions  *)                         
+(***************************)
+
+module Hsorts =
+  Hashcons.Make(
+    struct
+      type t = sorts
+      type u = section_path -> section_path
+      let hash_sub hsp = function
+	| Prop c -> Prop c
+        | Type {u_sp=sp; u_num=n} -> Type {u_sp=hsp sp; u_num=n}
+      let equal s1 s2 =
+        match (s1,s2) with
+          | (Prop c1, Prop c2) -> c1=c2
+          | (Type {u_sp=sp1; u_num=n1}, Type {u_sp=sp2; u_num=n2}) ->
+              sp1==sp2 & n1=n2
+          |_ -> false
+      let hash = Hashtbl.hash
+    end)
+
+module Hoper =
+  Hashcons.Make(
+    struct
+      type t = sorts oper
+      type u = (Coqast.t -> Coqast.t) * (sorts -> sorts)
+               * (section_path -> section_path) * (string -> string)
+      let hash_sub (hast,hsort,hsp,hstr) = function
+	| XTRA(s,al) -> XTRA(hstr s, List.map hast al)
+        | Sort s -> Sort (hsort s)
+        | Const sp -> Const (hsp sp)
+        | Abst sp -> Abst (hsp sp)
+        | MutInd (sp,i) -> MutInd (hsp sp, i)
+        | MutConstruct ((sp,i),j) -> MutConstruct ((hsp sp,i),j)
+        | MutCase(Some (sp,i)) -> MutCase(Some (hsp sp, i))
+        | t -> t 
+      let equal o1 o2 =
+        match (o1,o2) with
+          | (XTRA(s1,al1), XTRA(s2,al2)) ->
+              (s1==s2 & List.length al1 = List.length al2)
+              & List.for_all2 (==) al1 al2
+          | (Sort s1, Sort s2) -> s1==s2
+          | (Const sp1, Const sp2) -> sp1==sp2
+          | (Abst sp1, Abst 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(Some (sp1,i1)),MutCase(Some (sp2,i2))) -> sp1==sp2 & i1=i2
+          | _ -> 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 (hast,hsorts,hsp,hstr) =
+  Hashcons.simple_hcons Hoper.f (hast,hsorts,hsp,hstr)
+
+let hcons_term (hast,hsorts,hsp,hname,hident,hstr) =
+  let hoper = hcons_oper (hast,hsorts,hsp,hstr) in
+  Hashcons.recursive_hcons Hconstr.f (hoper,hname,hident)
+
+module Htype =
+  Hashcons.Make(
+    struct
+      type t = type_judgment
+      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 = 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
+  let (hast,_) = Coqast.hcons_ast hstr in
+  let hcci = hcons_term (hast,hsortscci,hspcci,hname,hident,hstr) in
+  let hfw = hcons_term (hast,hsortsfw,hspfw,hname,hident,hstr) in
+  let htcci = Hashcons.simple_hcons Htype.f (hcci,hsortscci) in
+  (hcci,hfw,htcci)
+
+let hcons1_constr c =
+  let hnames = hcons_names() in
+  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
+	 
+(*Gives the occurences number of t in u*)
+let rec nb_occ_term t u=
+  let one_step t=function
+    | DOP1(_,c) -> nb_occ_term t c
+    | DOP2(_,c0,c1) -> (nb_occ_term t c0)+(nb_occ_term t c1)
+    | DOPN(_,a) -> Array.fold_left (fun a x -> a+(nb_occ_term t x)) 0 a
+    | DOPL(_,l) -> List.fold_left (fun a x -> a+(nb_occ_term t x)) 0 l
+    | DLAM(_,c) -> nb_occ_term t c
+    | DLAMV(_,a) -> Array.fold_left (fun a x -> a+(nb_occ_term t x)) 0 a
+    | _ -> 0
+  in
+  if t=u then
+    1
+  else
+    one_step t u
+
+(*Alpha-conversion*)
+let bind_eq=function
+  | (Anonymous,Anonymous) -> true
+  | (Name _,Name _) -> true
+  | _ -> false
+	
+	(*Tells if two constrs are equal modulo unification*)
+let rec eq_mod_rel l_meta=function
+  | (t,DOP0(Meta n)) ->
+      if not(List.mem n (fst (List.split l_meta))) then
+	Some ([(n,t)]@l_meta)
+      else if (List.assoc n l_meta)=t then
+	Some l_meta
+      else
+	None
+  | DOP1(op0,c0), DOP1(op1,c1) ->
+      if op0=op1 then
+	eq_mod_rel l_meta (c0,c1)
+      else
+	None
+  | DOP2(op0,t0,c0), DOP2(op1,t1,c1) ->
+      if op0=op1 then
+	match (eq_mod_rel l_meta (t0,t1)) with
+          | None -> None
+          | Some l -> eq_mod_rel l (c0,c1)	
+      else
+	None
+  | DOPN(op0,t0), DOPN(op1,t1) ->
+      if (op0=op1) & ((Array.length t0)=(Array.length t1)) then
+	List.fold_left2
+          (fun a c1 c2 ->
+             match a with
+	       | None -> None
+               | Some l -> eq_mod_rel l (c1,c2)) (Some l_meta)
+          (Array.to_list t0) (Array.to_list t1)
+      else
+	None
+  | DLAM(n0,t0),DLAM(n1,t1) ->
+      if (bind_eq (n0,n1)) then
+	eq_mod_rel l_meta (t0,t1)
+      else
+	None
+  | (t,u) ->
+      if t=u then Some l_meta else None
+
+(*Substitutes a list of meta l in t*)
+let rec subst_with_lmeta l=function
+  | DOP0(Meta n) -> List.assoc n l
+  | DOP1(op,t) -> DOP1(op,subst_with_lmeta l t)
+  | DOP2(op,t0,t1) -> DOP2(op,subst_with_lmeta l t0,subst_with_lmeta l t1)
+  | DOPN(op,t) -> DOPN(op,Array.map (subst_with_lmeta l) t)
+  | DOPL(op,ld) -> DOPL(op,List.map (subst_with_lmeta l) ld)
+  | DLAM(n,t) -> DLAM(n,subst_with_lmeta l t)
+  | DLAMV(n,t) -> DLAMV(n,Array.map (subst_with_lmeta l) t)
+  | t -> t
+
+(*Carries out the following translation: DOPN(AppL,[|t|]) -> t and
+  DOPN(AppL,[|DOPN(AppL,t);...;t'|]) -> DOPN(AppL;[|t;...;t'|])*)
+let rec appl_elim=function
+  | DOPN(AppL,t) ->
+      if (Array.length t)=1 then
+	appl_elim t.(0)
+      else
+	(match t.(0) with
+           | DOPN(AppL,t') -> 
+	       appl_elim (DOPN(AppL,Array.append t' 
+				 (Array.of_list
+				    (List.tl (Array.to_list t)))))
+           |_ -> DOPN(AppL,Array.map appl_elim t))
+  | DOP1(op,t) -> DOP1(op,appl_elim t)
+  | DOP2(op,t0,t1) -> DOP2(op,appl_elim t0,appl_elim t1)
+  | DOPN(op,t) -> DOPN(op,Array.map appl_elim t)
+  | DOPL(op,ld) -> DOPL(op,List.map appl_elim ld)
+  | DLAM(n,t) -> DLAM(n,appl_elim t)
+  | DLAMV(n,t) -> DLAMV(n,Array.map appl_elim t)
+  | t -> t
+
+(*Gives Some(first instance of ceq in cref,occurence number for this
+  instance) or None if no instance of ceq can be found in cref*)
+let sub_term_with_unif cref ceq=
+  let rec find_match l_meta nb_occ op_ceq t_eq=function
+    | DOPN(AppL,t) as u ->
+	(match (t.(0)) with
+           | DOPN(op,t_op) ->
+               let t_args=Array.of_list (List.tl (Array.to_list t)) in
+               if op=op_ceq then
+                 match
+                   (List.fold_left2 
+                      (fun a c0 c1 ->
+                         match a with
+                           | None -> None
+                           | Some l -> eq_mod_rel l (c0,c1)) (Some l_meta)
+                      (Array.to_list t_args) (Array.to_list t_eq))
+                 with
+                   | None ->
+                       List.fold_left
+                         (fun (l_meta,nb_occ) x -> find_match l_meta nb_occ
+                              op_ceq t_eq x) (l_meta,nb_occ) (Array.to_list
+								t_args)
+                   | Some l -> (l,nb_occ+1)
+               else
+                 List.fold_left 
+		   (fun (l_meta,nb_occ) x -> find_match l_meta
+			nb_occ op_ceq t_eq x) 
+		   (l_meta,nb_occ) (Array.to_list t)
+           | VAR _ ->
+	       List.fold_left 
+		 (fun (l_meta,nb_occ) x -> find_match l_meta
+		      nb_occ op_ceq t_eq x) 
+		 (l_meta,nb_occ) (Array.to_list t)
+           |_ -> (l_meta,nb_occ))
+    | DOP2(_,t,DLAM(_,c)) ->
+	let (lt,nbt)=find_match l_meta nb_occ op_ceq t_eq t in
+        find_match lt nbt op_ceq t_eq c
+    | DOPN(_,t) -> 
+	List.fold_left 
+	  (fun (l_meta,nb_occ) x -> find_match l_meta nb_occ op_ceq t_eq x) 
+	  (l_meta,nb_occ) (Array.to_list t)
+    |_ -> (l_meta,nb_occ)
+  in
+  match (is_hd_const ceq) with
+    | None ->
+        if (occur_meta ceq) then
+          None
+        else
+          let nb_occ=nb_occ_term ceq cref in
+          if nb_occ=0 then
+            None
+          else
+            Some (ceq,nb_occ)
+    | Some (head,t_args) ->
+        let (l,nb)=find_match [] 0 head t_args cref in
+        if nb=0 then
+          None
+        else
+          Some ((subst_with_lmeta l ceq),nb)
diff --git a/kernel/term.mli b/kernel/term.mli
new file mode 100644
index 0000000000..d5a9b11d35
--- /dev/null
+++ b/kernel/term.mli
@@ -0,0 +1,520 @@
+
+(* $Id$ *)
+
+open Names
+open Generic
+
+(* The Type of Constructions Terms. *)
+
+(* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *)
+
+type 'a oper = 
+  (* DOP0 *)
+  | Meta of int
+  | Sort of 'a
+  | Implicit
+  (* DOP2 *)
+  | Cast | Prod | Lambda
+  (* DOPN *)
+  | AppL | Const of section_path | Abst of section_path
+  | MutInd of section_path * int
+  | MutConstruct of (section_path * int) * int
+  | MutCase of case_info
+  | Fix of int array * int
+  | CoFix of int
+
+  | XTRA of string * Coqast.t list
+      (* an extra slot, for putting in whatever sort of
+         operator we need for whatever sort of application *)
+
+and case_info = (section_path * int) option
+
+type contents = Pos | Null
+
+val str_of_contents : contents -> string
+val contents_of_str : string -> contents
+
+type sorts =
+  | Prop of contents       (* Prop and Set *)
+  | Type of Univ.universe  (* Type *)
+
+val mk_Set  : sorts
+val mk_Prop : sorts
+
+type constr = sorts oper term
+
+type 'a judge = { body : constr; typ : 'a }
+
+type type_judgment = sorts judge
+type term_judgment = type_judgment judge
+
+type conv_pb = CONV | CONV_LEQ | CONV_X | CONV_X_LEQ
+
+
+(****************************************************************************)
+(*              Functions for dealing with constr terms                     *)
+(****************************************************************************)
+
+(* The following functions are intended to simplify and to uniform the 
+   manipulation of terms. Some of these functions may be overlapped with
+   previous ones. *)
+
+(* Concrete type for making pattern-matching *)
+
+type kindOfTerm =
+  | IsRel          of int
+  | IsMeta         of int
+  | IsVar          of identifier
+  | IsXtra         of string * Coqast.t list
+  | IsSort         of sorts
+  | IsImplicit
+  | IsCast         of constr * constr
+  | IsProd         of name * constr * constr
+  | IsLambda       of name * constr * constr
+  | IsAppL         of constr array
+  | IsConst        of section_path  * constr array
+  | IsAbst         of section_path  * constr array
+  | IsMutInd       of section_path * int * constr array
+  | IsMutConstruct of section_path * int * int * constr array
+  | IsMutCase      of case_info * constr * constr * constr array
+  | IsFix          of int array * int * constr array * name list *
+                      constr array
+  | IsCoFix        of int * constr array * name list * constr array
+
+(* 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.  
+*)
+
+val kind_of_term : constr -> kindOfTerm
+
+(*********************)
+(* Term constructors *)
+(*********************)
+
+(* Constructs a DeBrujin index *)
+val mkRel          : int -> constr
+
+(* Constructs an existential variable named "?" *)
+val mkExistential  : constr
+
+(* Constructs an existential variable named "?n" *)
+val mkMeta         : int -> constr
+
+(* Constructs a Variable *)
+val mkVar          : identifier -> constr
+
+(* Construct an XTRA term (XTRA is an extra slot for whatever you want) *)
+val mkXtra         : string -> Coqast.t list -> constr
+
+(* Construct a type *)
+val mkSort         : sorts -> constr
+val mkProp         : constr
+val mkSet          : constr 
+val mkType         : Univ.universe -> constr
+val prop : sorts
+val spec : sorts
+val types : sorts 
+val type_0 : sorts
+val type_1 : sorts
+
+(* Construct an implicit (see implicit arguments in the RefMan) *)
+(* Used for extraction *)
+val mkImplicit     : constr
+val implicit_sort  : sorts
+
+(* 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) *)
+val mkCast         : constr -> constr -> constr
+
+(* Constructs the product (x:t1)t2  -- x may be anonymous *)
+val mkProd         : name -> constr -> constr -> constr
+
+(* non-dependant product t1 -> t2 *)
+val mkArrow : constr -> constr -> constr
+
+(* named product *)
+val mkNamedProd : identifier -> constr -> constr -> constr
+
+(* Constructs the abstraction [x:t1]t2 *)
+val mkLambda       : name -> constr -> constr -> constr
+val mkNamedLambda : identifier -> constr -> constr -> constr
+
+(* If a = [| t1; ...; tn |], constructs the application (t1 ... tn) *)
+val mkAppL         : constr array -> constr
+val mkAppList      : constr list  -> constr
+
+(* Constructs a constant *) 
+(* The array of terms correspond to the variables introduced in the section *)
+val mkConst        : section_path -> constr array -> constr
+
+(* Constructs an abstract object *)
+val mkAbst         : section_path -> constr array -> constr
+
+(* Constructs the ith (co)inductive type of the block named sp *)
+(* The array of terms correspond to the variables introduced in the section *)
+val mkMutInd       : section_path -> int -> constr array -> constr
+
+(* 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 *)
+val mkMutConstruct : section_path -> int -> int -> constr array -> constr
+
+(* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
+val mkMutCase      : case_info -> constr -> constr -> constr list -> constr
+val mkMutCaseA     : case_info -> constr -> constr -> constr array -> constr
+
+(* If recindxs = [|i1,...in|] 
+      typarray = [|t1,...tn|]
+      funnames = [f1,.....fn]
+      bodies   = [b1,.....bn]
+   then    
+
+      mkFix recindxs i typarray funnames bodies
+   
+   constructs 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.
+*)
+val mkFix          : int array -> int -> type_judgment array -> name list 
+                      -> constr array -> constr
+
+(* Similarly, but we assume the body already constructed *)
+val mkFixDlam      : int array -> int -> type_judgment array
+                     -> constr array -> constr 
+
+(* If typarray = [|t1,...tn|]
+      funnames = [f1,.....fn]
+      bodies   = [b1,.....bn]
+   then
+
+      mkCoFix i typsarray funnames bodies 
+
+   constructs the ith function of the block  
+   
+    CoFixpoint f1 = b1
+    with       f2 = b2
+    ...
+    with       fn = bn.
+
+*)
+val mkCoFix        : int -> type_judgment array -> name list 
+                     -> constr array -> constr
+
+(* Similarly, but we assume the body already constructed *)
+val mkCoFixDlam    : int -> type_judgment array -> constr array -> constr
+
+(********************)
+(* Term destructors *)
+(********************)
+
+(* Destructor operations : partial functions 
+   Raise invalid_arg "dest*" if the const has not the expected form *)
+
+(* Destructs a DeBrujin index *)
+val destRel          : constr -> int
+
+(* Destructs an existential variable *)
+val destMeta         : constr -> int
+val isMETA : constr -> bool
+
+(* Destructs a variable *)
+val destVar          : constr -> identifier
+
+(* Destructs an XTRA *)
+val destXtra        : constr -> string * Coqast.t list
+
+(* Destructs a sort *)
+val destSort         : constr -> sorts
+val contents_of_kind : constr -> contents
+val is_Prop          : constr -> bool (* true for Prop *) 
+val is_Set           : constr -> bool  (* true for Set *)
+val isprop           : constr -> bool (* true for DOP0 (Sort (Prop _)) *)
+val is_Type          : constr -> bool (* true for DOP0 (Sort (Type _)) *)
+val iskind           : constr -> bool (* true for Prop, Set and Type(_) *)
+
+val isType           : sorts -> bool (* true for Type(_) *)
+val is_small         : sorts -> bool (* true for Prop and Set *)
+
+(* Destructs a casted term *)
+val destCast         : constr -> constr * constr
+val cast_type : constr -> constr (* 2nd proj *)
+val cast_term : constr -> constr (* 1st proj *)
+val isCast : constr -> bool
+(* removes recursively the casts around a term *)
+(* strip_outer_cast (Cast (Cast ... (Cast c, t) ... )) is c *)
+val strip_outer_cast : constr -> constr
+
+(* Destructs the product (x:t1)t2 *)
+val destProd          : constr -> name * constr * constr
+val hd_of_prod        : constr -> constr
+val hd_is_constructor : constr -> bool
+
+(* Destructs the abstraction [x:t1]t2 *)
+val destLambda       : constr -> name * constr * constr
+
+(* Destructs an application *)
+val destAppL   : constr -> constr array
+val isAppL     : constr -> bool
+val hd_app     : constr -> constr 
+val args_app   : constr -> constr array
+
+(* Destructs a constant *)
+val destConst     : constr -> section_path * constr array
+val path_of_const : constr -> section_path
+val args_of_const : constr -> constr array
+
+(* Destrucy an abstract term *)
+val destAbst         : constr -> section_path * constr array
+val path_of_abst : constr -> section_path
+val args_of_abst : constr -> constr array
+
+(* Destructs a (co)inductive type *)
+val destMutInd    : constr -> section_path * int * constr array
+val op_of_mind    : constr -> section_path * int
+val args_of_mind  : constr -> constr array
+val ci_of_mind    : constr -> case_info
+
+(* Destructs a constructor *)
+val destMutConstruct : constr -> section_path * int * int * constr array
+val op_of_mconstr    : constr -> (section_path * int) * int
+val args_of_mconstr  : constr -> constr array
+
+(* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
+val destCase         : constr -> case_info * constr * constr * constr array
+
+(* 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.
+*)
+val destGralFix      : constr array -> constr array * Names.name list 
+                                        * constr array
+val destFix          : constr -> int array * int * type_judgment array
+                                  * Names.name list * constr array
+val destCoFix        : constr -> int * type_judgment array * Names.name list 
+                                  * constr array
+
+(* Provisoire, le temps de maitriser les cast *)
+val destUntypedFix          : constr -> int array * int * constr array
+                                  * Names.name list * constr array
+val destUntypedCoFix        : constr -> int * constr array * Names.name list 
+                                  * constr array
+
+(***********************************)
+(* Other term constructors         *)
+(***********************************)
+
+val abs_implicit : constr -> constr
+val lambda_implicit : constr -> constr
+val lambda_implicit_lift : int -> constr -> constr
+
+val applist : constr * constr list -> constr
+val applistc : constr -> constr list -> constr
+val appvect : constr * constr array -> constr
+val appvectc : constr -> constr array -> constr
+(* prodn n ([x1:T1]..[xn:Tn]Gamma) b = (x1:T1)..(xn:Tn)b *)
+val prodn   : int -> (name * constr) list -> constr -> constr
+(* lamn n ([x1:T1]..[xn:T]Gamma) b = [x1:T1]..[xn:Tn]b *)
+val lamn : int -> (name * constr) list -> constr -> constr
+
+(* prod_it b [x1:T1;..xn:Tn] = (x1:T1)..(xn:Tn)b *)
+val prod_it : constr -> (name * constr) list -> constr
+(* lam_it b [x1:T1;..xn:Tn] = [x1:T1]..[xn:Tn]b *)
+val lam_it : constr -> (name * constr) list -> constr
+
+
+(* 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 *)
+val to_lambda : int -> constr -> constr
+val to_prod : int -> constr -> constr
+
+(*********************************)
+(* Other term destructors        *)
+(*********************************)
+
+(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
+   ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
+val decompose_prod  : constr -> (name*constr) list * constr
+
+(* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair
+   ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)
+val decompose_lam   : constr -> (name*constr) list * constr
+
+(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T 
+   into the pair ([(xn,Tn);...;(x1,T1)],T) *)
+val decompose_prod_n  : int -> constr -> (name*constr) list * constr
+
+(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T 
+   into the pair ([(xn,Tn);...;(x1,T1)],T) *)
+val decompose_lam_n   : int -> constr -> (name*constr) list * constr
+
+(* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
+ * gives n (casts are ignored) *)
+val nb_lam : constr -> int
+
+(* similar to nb_lam, but gives the number of products instead *)
+val nb_prod : constr -> int
+
+(********************************************************************)
+(*   various utility functions for implementing terms with bindings *)
+(********************************************************************)
+
+val extract_lifted : int * constr -> constr
+val insert_lifted : constr -> int * constr
+
+(* l is a list of pairs (n:nat,x:constr), env is a stack of (na:name,T:constr)
+   push_and_lift adds a component 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 (x1:A1)(x2:A2)....(xn:An)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 [x1:A1][x2:A2]....[xn:An]T' then (push_lam_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_lam_and_liftl :
+  int -> (name * constr) list -> constr -> (int * constr) list
+    -> (name * constr) list * constr * (int * constr) list
+
+(* l is a list of pairs (n:nat,x:constr), tlenv is a stack of
+(na:name,T:constr), B : constr, na : name
+(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 = [na1:T1 ; na2:T2 ; ... ; nan:Tn]@tlenv
+then
+(prod_and_popl n env T l) gives (tlenv,(nan:Tn)...(na1:Ta1)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 [nan:Tan]...[na1:Ta1]B instead of
+ * (nan:Tan)...(na1:Ta1)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 [nan:Tan]...[na1:Ta1]B instead of
+ * but it generates names whenever nai=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
+
+(******************************************************************)
+(* 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
+
+
+(********************************************)
+(* Misc functions on terms, judgments, etc  *)
+(********************************************)
+
+(* Level comparison for information extraction : Prop <= Type *)
+val same_kind : constr -> constr -> bool
+val le_kind : constr -> constr -> bool
+val le_kind_implicit : constr -> constr -> bool
+
+val pb_is_univ_adjust : conv_pb -> bool
+val pb_is_equal : conv_pb -> bool
+val pb_equal : conv_pb -> conv_pb
+val sort_hdchar : sorts -> string
+(* val sort_cmp : conv_pb -> sorts -> sorts -> bool *)
+
+
+(***************************)
+(* occurs check functions  *)                         
+(***************************)
+val occur_meta : constr -> bool
+val rel_vect : int -> int -> constr array
+
+(* (occur_const (s:section_path) c) -> true if constant s occurs in c,
+ * false otherwise *)
+val occur_const : section_path -> 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
+val eta_eq_constr : constr -> constr -> bool
+val rename_rels : int -> constr -> (identifier * constr) list -> constr
+val clean_rhs : constr -> (identifier * constr) list -> constr
+val subst_term : constr -> constr -> constr
+val subst_term_eta_eq : constr -> constr -> constr
+val replace_consts :
+  (section_path * (identifier list * constr) option) list -> constr -> constr
+
+(* bl : (int,constr) Listmap.t = (int * constr) list *)
+(* c : constr *)
+(* for each binding (i,c_i) in bl, substitutes the metavar i by c_i in c *)
+(* Raises Not_found if c contains a meta that is not in the association list *)
+
+val subst_meta : (int * constr) list -> constr -> constr
+
+(* Transforms a constr into a matchable constr *)
+val matchable : constr -> constr
+val unmatchable: constr -> constr
+
+(* New hash-cons functions *)
+
+val hcons_constr:
+  (section_path -> section_path) *
+  (section_path -> section_path) *
+  (name -> name) *
+  (identifier -> identifier) *
+  (string -> string) 
+  ->
+    (constr -> constr) *
+    (constr -> constr) *
+    (type_judgment -> type_judgment)
+
+val hcons1_constr : constr -> constr
diff --git a/kernel/univ.mli b/kernel/univ.mli
new file mode 100644
index 0000000000..0bfaddbcc5
--- /dev/null
+++ b/kernel/univ.mli
@@ -0,0 +1,12 @@
+
+(* $Id$ *)
+
+open Names
+
+type universe = { u_sp : section_path; u_num : int }
+
+val dummy_univ : universe
+
+val prop_univ : universe
+val prop_univ_univ : universe
+val prop_univ_univ_univ : universe