Splitting Term into five unrelated interfaces:

1. sorts.ml: A small file utility for sorts;

2. constr.ml: Really low-level terms, essentially kind_of_constr, smart
constructor and basic operators;

3. vars.ml: Everything related to term variables, that is, occurences
and substitution;

4. context.ml: Rel/Named context and all that;

5. term.ml: derived utility operations on terms; also includes constr.ml
up to some renaming, and acts as a compatibility layer, to be deprecated.

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

126 files changed, 1810 insertions, 1279 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 73bda713a..b09c8e97e 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -40,6 +40,10 @@ Dnet
 Names
 Univ
 Esubst
+Sorts
+Constr
+Context
+Vars
 Term
 Mod_subst
 Sign
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 0a4192c3e..4cf79337c 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -9,6 +9,7 @@
 open Pp
 open Names
 open Term
+open Context
 open Termops
 open Sign
 open Environ
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 99c2a338e..1fa0db911 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Term
+open Context
 open Sign
 open Evd
 open Environ
diff --git a/kernel/closure.ml b/kernel/closure.ml
index b22dd42e7..2628895eb 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -22,8 +22,9 @@
 open Errors
 open Util
 open Pp
-open Term
 open Names
+open Term
+open Vars
 open Environ
 open Esubst
 
diff --git a/kernel/constr.ml b/kernel/constr.ml
new file mode 100644
index 000000000..d09222ead
--- /dev/null
+++ b/kernel/constr.ml
@@ -0,0 +1,660 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* File initially created by Gérard Huet and Thierry Coquand in 1984 *)
+(* Extension to inductive constructions by Christine Paulin for Coq V5.6 *)
+(* Extension to mutual inductive constructions by Christine Paulin for
+   Coq V5.10.2 *)
+(* Extension to co-inductive constructions by Eduardo Gimenez *)
+(* Optimization of substitution functions by Chet Murthy *)
+(* Optimization of lifting functions by Bruno Barras, Mar 1997 *)
+(* Hash-consing by Bruno Barras in Feb 1998 *)
+(* Restructuration of Coq of the type-checking kernel by Jean-Christophe 
+   Filliâtre, 1999 *)
+(* Abstraction of the syntax of terms and iterators by Hugo Herbelin, 2000 *)
+(* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *)
+
+(* This file defines the internal syntax of the Calculus of
+   Inductive Constructions (CIC) terms together with constructors,
+   destructors, iterators and basic functions *)
+
+open Errors
+open Util
+open Pp
+open Names
+open Univ
+open Esubst
+
+
+type existential_key = int
+type metavariable = int
+
+(* This defines the strategy to use for verifiying a Cast *)
+(* Warning: REVERTcast is not exported to vo-files; as of r14492, it has to *)
+(* come after the vo-exported cast_kind so as to be compatible with coqchk *)
+type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast
+
+(* This defines Cases annotations *)
+type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
+type case_printing =
+  { ind_nargs : int; (* length of the arity of the inductive type *)
+    style     : case_style }
+type case_info =
+  { ci_ind        : inductive;
+    ci_npar       : int;
+    ci_cstr_ndecls : int array; (* number of pattern vars of each constructor *)
+    ci_pp_info    : case_printing (* not interpreted by the kernel *)
+  }
+
+(********************************************************************)
+(*       Constructions as implemented                               *)
+(********************************************************************)
+
+(* [constr array] is an instance matching definitional [named_context] in
+   the same order (i.e. last argument first) *)
+type 'constr pexistential = existential_key * 'constr array
+type ('constr, 'types) prec_declaration =
+    Name.t array * 'types array * 'constr array
+type ('constr, 'types) pfixpoint =
+    (int array * int) * ('constr, 'types) prec_declaration
+type ('constr, 'types) pcofixpoint =
+    int * ('constr, 'types) prec_declaration
+
+(* [Var] is used for named variables and [Rel] for variables as
+   de Bruijn indices. *)
+type ('constr, 'types) kind_of_term =
+  | Rel       of int
+  | Var       of Id.t
+  | Meta      of metavariable
+  | Evar      of 'constr pexistential
+  | Sort      of Sorts.t
+  | Cast      of 'constr * cast_kind * 'types
+  | Prod      of Name.t * 'types * 'types
+  | Lambda    of Name.t * 'types * 'constr
+  | LetIn     of Name.t * 'constr * 'types * 'constr
+  | App       of 'constr * 'constr array
+  | Const     of constant
+  | Ind       of inductive
+  | Construct of constructor
+  | Case      of case_info * 'constr * 'constr * 'constr array
+  | Fix       of ('constr, 'types) pfixpoint
+  | CoFix     of ('constr, 'types) pcofixpoint
+
+(* constr is the fixpoint of the previous type. Requires option
+   -rectypes of the Caml compiler to be set *)
+type t = (t,t) kind_of_term
+type constr = t
+
+type existential = existential_key * constr array
+type rec_declaration = Name.t array * constr array * constr array
+type fixpoint = (int array * int) * rec_declaration
+type cofixpoint = int * rec_declaration
+
+type types = constr
+
+(*********************)
+(* Term constructors *)
+(*********************)
+
+(* Constructs a DeBrujin index with number n *)
+let rels =
+  [|Rel  1;Rel  2;Rel  3;Rel  4;Rel  5;Rel  6;Rel  7; Rel  8;
+    Rel  9;Rel 10;Rel 11;Rel 12;Rel 13;Rel 14;Rel 15; Rel 16|]
+
+let mkRel n = if 0<n & n<=16 then rels.(n-1) else Rel n
+
+(* Construct a type *)
+let mkProp   = Sort Sorts.prop
+let mkSet    = Sort Sorts.set
+let mkType u = Sort (Sorts.Type u)
+let mkSort   = function
+  | Sorts.Prop Sorts.Null -> mkProp (* Easy sharing *)
+  | Sorts.Prop Sorts.Pos -> mkSet
+  | s -> Sort s
+
+(* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *)
+(* (that means t2 is declared as the type of t1) *)
+let mkCast (t1,k2,t2) =
+  match t1 with
+  | Cast (c,k1, _) when (k1 == VMcast || k1 == NATIVEcast) && k1 == k2 -> Cast (c,k1,t2)
+  | _ -> Cast (t1,k2,t2)
+
+(* Constructs the product (x:t1)t2 *)
+let mkProd (x,t1,t2) = Prod (x,t1,t2)
+
+(* Constructs the abstraction [x:t1]t2 *)
+let mkLambda (x,t1,t2) = Lambda (x,t1,t2)
+
+(* Constructs [x=c_1:t]c_2 *)
+let mkLetIn (x,c1,t,c2) = LetIn (x,c1,t,c2)
+
+(* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *)
+(* We ensure applicative terms have at least one argument and the
+   function is not itself an applicative term *)
+let mkApp (f, a) =
+  if Int.equal (Array.length a) 0 then f else
+    match f with
+      | App (g, cl) -> App (g, Array.append cl a)
+      | _ -> App (f, a)
+
+(* Constructs a constant *)
+let mkConst c = Const c
+
+(* Constructs an existential variable *)
+let mkEvar e = Evar e
+
+(* Constructs the ith (co)inductive type of the block named kn *)
+let mkInd m = Ind m
+
+(* Constructs the jth constructor of the ith (co)inductive type of the
+   block named kn. The array of terms correspond to the variables
+   introduced in the section *)
+let mkConstruct c = Construct c
+
+(* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
+let mkCase (ci, p, c, ac) = Case (ci, p, c, ac)
+
+(* If recindxs = [|i1,...in|]
+      funnames = [|f1,...fn|]
+      typarray = [|t1,...tn|]
+      bodies   = [|b1,...bn|]
+   then
+
+      mkFix ((recindxs,i),(funnames,typarray,bodies))
+
+   constructs the ith function of the block
+
+    Fixpoint f1 [ctx1] : t1 := b1
+    with     f2 [ctx2] : t2 := b2
+    ...
+    with     fn [ctxn] : tn := bn.
+
+   where the length of the jth context is ij.
+*)
+
+let mkFix fix = Fix fix
+
+(* If funnames = [|f1,...fn|]
+      typarray = [|t1,...tn|]
+      bodies   = [|b1,...bn|]
+   then
+
+      mkCoFix (i,(funnames,typsarray,bodies))
+
+   constructs the ith function of the block
+
+    CoFixpoint f1 : t1 := b1
+    with       f2 : t2 := b2
+    ...
+    with       fn : tn := bn.
+*)
+let mkCoFix cofix= CoFix cofix
+
+(* Constructs an existential variable named "?n" *)
+let mkMeta  n =  Meta n
+
+(* Constructs a Variable named id *)
+let mkVar id = Var id
+
+
+(************************************************************************)
+(*    kind_of_term = constructions as seen by the user                 *)
+(************************************************************************)
+
+(* User view of [constr]. For [App], it is ensured there is at
+   least one argument and the function is not itself an applicative
+   term *)
+
+let kind c = c
+
+(****************************************************************************)
+(*              Functions to recur through subterms                         *)
+(****************************************************************************)
+
+(* [fold f acc c] folds [f] on the immediate subterms of [c]
+   starting from [acc] and proceeding from left to right according to
+   the usual representation of the constructions; it is not recursive *)
+
+let fold f acc c = match kind c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> acc
+  | Cast (c,_,t) -> f (f acc c) t
+  | Prod (_,t,c) -> f (f acc t) c
+  | Lambda (_,t,c) -> f (f acc t) c
+  | LetIn (_,b,t,c) -> f (f (f acc b) t) c
+  | App (c,l) -> Array.fold_left f (f acc c) l
+  | Evar (_,l) -> Array.fold_left f acc l
+  | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
+  | Fix (_,(lna,tl,bl)) ->
+      let fd = Array.map3 (fun na t b -> (na,t,b)) lna tl bl in
+      Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd
+  | CoFix (_,(lna,tl,bl)) ->
+      let fd = Array.map3 (fun na t b -> (na,t,b)) lna tl bl in
+      Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd
+
+(* [iter f c] iters [f] on the immediate subterms of [c]; it is
+   not recursive and the order with which subterms are processed is
+   not specified *)
+
+let iter f c = match kind c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> ()
+  | Cast (c,_,t) -> f c; f t
+  | Prod (_,t,c) -> f t; f c
+  | Lambda (_,t,c) -> f t; f c
+  | LetIn (_,b,t,c) -> f b; f t; f c
+  | App (c,l) -> f c; Array.iter f l
+  | Evar (_,l) -> Array.iter f l
+  | Case (_,p,c,bl) -> f p; f c; Array.iter f bl
+  | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
+  | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
+
+(* [iter_with_binders g f n c] iters [f n] on the immediate
+   subterms of [c]; it carries an extra data [n] (typically a lift
+   index) which is processed by [g] (which typically add 1 to [n]) at
+   each binder traversal; it is not recursive and the order with which
+   subterms are processed is not specified *)
+
+let iter_with_binders g f n c = match kind c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> ()
+  | Cast (c,_,t) -> f n c; f n t
+  | Prod (_,t,c) -> f n t; f (g n) c
+  | Lambda (_,t,c) -> f n t; f (g n) c
+  | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c
+  | App (c,l) -> f n c; Array.iter (f n) l
+  | Evar (_,l) -> Array.iter (f n) l
+  | Case (_,p,c,bl) -> f n p; f n c; Array.iter (f n) bl
+  | Fix (_,(_,tl,bl)) ->
+      Array.iter (f n) tl;
+      Array.iter (f (iterate g (Array.length tl) n)) bl
+  | CoFix (_,(_,tl,bl)) ->
+      Array.iter (f n) tl;
+      Array.iter (f (iterate g (Array.length tl) n)) bl
+
+(* [map f c] maps [f] on the immediate subterms of [c]; it is
+   not recursive and the order with which subterms are processed is
+   not specified *)
+
+let map f c = match kind c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> c
+  | Cast (c,k,t) -> mkCast (f c, k, f t)
+  | Prod (na,t,c) -> mkProd (na, f t, f c)
+  | Lambda (na,t,c) -> mkLambda (na, f t, f c)
+  | LetIn (na,b,t,c) -> mkLetIn (na, f b, f t, f c)
+  | App (c,l) -> mkApp (f c, Array.map f l)
+  | Evar (e,l) -> mkEvar (e, Array.map f l)
+  | Case (ci,p,c,bl) -> mkCase (ci, f p, f c, Array.map f bl)
+  | Fix (ln,(lna,tl,bl)) ->
+      mkFix (ln,(lna,Array.map f tl,Array.map f bl))
+  | CoFix(ln,(lna,tl,bl)) ->
+      mkCoFix (ln,(lna,Array.map f tl,Array.map f bl))
+
+(* [map_with_binders g f n c] maps [f n] on the immediate
+   subterms of [c]; it carries an extra data [n] (typically a lift
+   index) which is processed by [g] (which typically add 1 to [n]) at
+   each binder traversal; it is not recursive and the order with which
+   subterms are processed is not specified *)
+
+let map_with_binders g f l c = match kind c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> c
+  | Cast (c,k,t) -> mkCast (f l c, k, f l t)
+  | Prod (na,t,c) -> mkProd (na, f l t, f (g l) c)
+  | Lambda (na,t,c) -> mkLambda (na, f l t, f (g l) c)
+  | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g l) c)
+  | App (c,al) -> mkApp (f l c, Array.map (f l) al)
+  | Evar (e,al) -> mkEvar (e, Array.map (f l) al)
+  | Case (ci,p,c,bl) -> mkCase (ci, f l p, f l c, Array.map (f l) bl)
+  | Fix (ln,(lna,tl,bl)) ->
+      let l' = iterate g (Array.length tl) l in
+      mkFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
+  | CoFix(ln,(lna,tl,bl)) ->
+      let l' = iterate g (Array.length tl) l in
+      mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
+
+(* [compare f c1 c2] compare [c1] and [c2] using [f] to compare
+   the immediate subterms of [c1] of [c2] if needed; Cast's,
+   application associativity, binders name and Cases annotations are
+   not taken into account *)
+
+
+let compare_head f t1 t2 =
+  match kind t1, kind t2 with
+  | Rel n1, Rel n2 -> Int.equal n1 n2
+  | Meta m1, Meta m2 -> Int.equal m1 m2
+  | Var id1, Var id2 -> Id.equal id1 id2
+  | Sort s1, Sort s2 -> Int.equal (Sorts.compare s1 s2) 0
+  | Cast (c1,_,_), _ -> f c1 t2
+  | _, Cast (c2,_,_) -> f t1 c2
+  | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 && f c1 c2
+  | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 && f c1 c2
+  | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 && f t1 t2 && f c1 c2
+  | App (Cast(c1, _, _),l1), _ -> f (mkApp (c1,l1)) t2
+  | _, App (Cast (c2, _, _),l2) -> f t1 (mkApp (c2,l2))
+  | App (c1,l1), App (c2,l2) ->
+    Int.equal (Array.length l1) (Array.length l2) &&
+      f c1 c2 && Array.equal f l1 l2
+  | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 && Array.equal f l1 l2
+  | Const c1, Const c2 -> eq_constant c1 c2
+  | Ind c1, Ind c2 -> eq_ind c1 c2
+  | Construct c1, Construct c2 -> eq_constructor c1 c2
+  | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
+      f p1 p2 & f c1 c2 && Array.equal f bl1 bl2
+  | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
+      Int.equal i1 i2 && Array.equal Int.equal ln1 ln2
+      && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
+  | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
+      Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
+  | _ -> false
+
+(*******************************)
+(*  alpha conversion functions *)
+(*******************************)
+
+(* alpha conversion : ignore print names and casts *)
+
+let rec eq_constr m n =
+  (m == n) || compare_head eq_constr m n
+
+let equal m n = eq_constr m n (* to avoid tracing a recursive fun *)
+
+let constr_ord_int f t1 t2 =
+  let (=?) f g i1 i2 j1 j2=
+    let c = f i1 i2 in
+    if Int.equal c 0 then g j1 j2 else c in
+  let (==?) fg h i1 i2 j1 j2 k1 k2=
+    let c=fg i1 i2 j1 j2 in
+    if Int.equal c 0 then h k1 k2 else c in
+  let fix_cmp (a1, i1) (a2, i2) =
+    ((Array.compare Int.compare) =? Int.compare) a1 a2 i1 i2
+  in
+  match kind t1, kind t2 with
+    | Rel n1, Rel n2 -> Int.compare n1 n2
+    | Meta m1, Meta m2 -> Int.compare m1 m2
+    | Var id1, Var id2 -> Id.compare id1 id2
+    | Sort s1, Sort s2 -> Sorts.compare s1 s2
+    | Cast (c1,_,_), _ -> f c1 t2
+    | _, Cast (c2,_,_) -> f t1 c2
+    | Prod (_,t1,c1), Prod (_,t2,c2)
+    | Lambda (_,t1,c1), Lambda (_,t2,c2) ->
+        (f =? f) t1 t2 c1 c2
+    | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) ->
+        ((f =? f) ==? f) b1 b2 t1 t2 c1 c2
+    | App (Cast(c1,_,_),l1), _ -> f (mkApp (c1,l1)) t2
+    | _, App (Cast(c2, _,_),l2) -> f t1 (mkApp (c2,l2))
+    | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2
+    | Evar (e1,l1), Evar (e2,l2) ->
+        ((-) =? (Array.compare f)) e1 e2 l1 l2
+    | Const c1, Const c2 -> con_ord c1 c2
+    | Ind ind1, Ind ind2 -> ind_ord ind1 ind2
+    | Construct ct1, Construct ct2 -> constructor_ord ct1 ct2
+    | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
+        ((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2
+    | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
+        ((fix_cmp =? (Array.compare f)) ==? (Array.compare f))
+        ln1 ln2 tl1 tl2 bl1 bl2
+    | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
+        ((Int.compare =? (Array.compare f)) ==? (Array.compare f))
+        ln1 ln2 tl1 tl2 bl1 bl2
+    | t1, t2 -> Pervasives.compare t1 t2
+
+let rec compare m n=
+  constr_ord_int compare m n
+
+(*******************)
+(*  hash-consing   *)
+(*******************)
+
+(* Hash-consing of [constr] does not use the module [Hashcons] because
+   [Hashcons] is not efficient on deep tree-like data
+   structures. Indeed, [Hashcons] is based the (very efficient)
+   generic hash function [Hashtbl.hash], which computes the hash key
+   through a depth bounded traversal of the data structure to be
+   hashed. As a consequence, for a deep [constr] like the natural
+   number 1000 (S (S (... (S O)))), the same hash is assigned to all
+   the sub [constr]s greater than the maximal depth handled by
+   [Hashtbl.hash]. This entails a huge number of collisions in the
+   hash table and leads to cubic hash-consing in this worst-case.
+
+   In order to compute a hash key that is independent of the data
+   structure depth while being constant-time, an incremental hashing
+   function must be devised. A standard implementation creates a cache
+   of the hashing function by decorating each node of the hash-consed
+   data structure with its hash key. In that case, the hash function
+   can deduce the hash key of a toplevel data structure by a local
+   computation based on the cache held on its substructures.
+   Unfortunately, this simple implementation introduces a space
+   overhead that is damageable for the hash-consing of small [constr]s
+   (the most common case). One can think of an heterogeneous
+   distribution of caches on smartly chosen nodes, but this is forbidden
+   by the use of generic equality in Coq source code. (Indeed, this forces
+   each [constr] to have a unique canonical representation.)
+
+   Given that hash-consing proceeds inductively, we can nonetheless
+   computes the hash key incrementally during hash-consing by changing
+   a little the signature of the hash-consing function: it now returns
+   both the hash-consed term and its hash key. This simple solution is
+   implemented in the following code: it does not introduce a space
+   overhead in [constr], that's why the efficiency is unchanged for
+   small [constr]s. Besides, it does handle deep [constr]s without
+   introducing an unreasonable number of collisions in the hash table.
+   Some benchmarks make us think that this implementation of
+   hash-consing is linear in the size of the hash-consed data
+   structure for our daily use of Coq.
+*)
+
+let array_eqeq t1 t2 =
+  t1 == t2 ||
+  (Int.equal (Array.length t1) (Array.length t2) &&
+   let rec aux i =
+     (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1))
+   in aux 0)
+
+let hasheq t1 t2 =
+  match t1, t2 with
+    | Rel n1, Rel n2 -> n1 == n2
+    | Meta m1, Meta m2 -> m1 == m2
+    | Var id1, Var id2 -> id1 == id2
+    | Sort s1, Sort s2 -> s1 == s2
+    | Cast (c1,k1,t1), Cast (c2,k2,t2) -> c1 == c2 & k1 == k2 & t1 == t2
+    | Prod (n1,t1,c1), Prod (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2
+    | Lambda (n1,t1,c1), Lambda (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2
+    | LetIn (n1,b1,t1,c1), LetIn (n2,b2,t2,c2) ->
+      n1 == n2 & b1 == b2 & t1 == t2 & c1 == c2
+    | App (c1,l1), App (c2,l2) -> c1 == c2 & array_eqeq l1 l2
+    | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 & array_eqeq l1 l2
+    | Const c1, Const c2 -> c1 == c2
+    | Ind (sp1,i1), Ind (sp2,i2) -> sp1 == sp2 && Int.equal i1 i2
+    | Construct ((sp1,i1),j1), Construct ((sp2,i2),j2) ->
+      sp1 == sp2 && Int.equal i1 i2 && Int.equal j1 j2
+    | Case (ci1,p1,c1,bl1), Case (ci2,p2,c2,bl2) ->
+      ci1 == ci2 & p1 == p2 & c1 == c2 & array_eqeq bl1 bl2
+    | Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) ->
+      Int.equal i1 i2
+      && Array.equal Int.equal ln1 ln2
+      && array_eqeq lna1 lna2
+      && array_eqeq tl1 tl2
+      && array_eqeq bl1 bl2
+    | CoFix(ln1,(lna1,tl1,bl1)), CoFix(ln2,(lna2,tl2,bl2)) ->
+      Int.equal ln1 ln2
+      & array_eqeq lna1 lna2
+      & array_eqeq tl1 tl2
+      & array_eqeq bl1 bl2
+    | _ -> false
+
+(** Note that the following Make has the side effect of creating
+    once and for all the table we'll use for hash-consing all constr *)
+
+module HashsetTerm = Hashset.Make(struct type t = constr let equal = hasheq end)
+
+let term_table = HashsetTerm.create 19991
+(* The associative table to hashcons terms. *)
+
+open Hashset.Combine
+
+(* [hashcons hash_consing_functions constr] computes an hash-consed
+   representation for [constr] using [hash_consing_functions] on
+   leaves. *)
+let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
+
+  (* Note : we hash-cons constr arrays *in place* *)
+
+  let rec hash_term_array t =
+    let accu = ref 0 in
+    for i = 0 to Array.length t - 1 do
+      let x, h = sh_rec t.(i) in
+      accu := combine !accu h;
+      t.(i) <- x
+    done;
+    !accu
+
+  and hash_term t =
+    match t with
+      | Var i ->
+	(Var (sh_id i), combinesmall 1 (Hashtbl.hash i))
+      | Sort s ->
+	(Sort (sh_sort s), combinesmall 2 (Hashtbl.hash s))
+      | Cast (c, k, t) ->
+	let c, hc = sh_rec c in
+	let t, ht = sh_rec t in
+	(Cast (c, k, t), combinesmall 3 (combine3 hc (Hashtbl.hash k) ht))
+      | Prod (na,t,c) ->
+	let t, ht = sh_rec t
+	and c, hc = sh_rec c in
+	(Prod (sh_na na, t, c), combinesmall 4 (combine3 (Hashtbl.hash na) ht hc))
+      | Lambda (na,t,c) ->
+	let t, ht = sh_rec t
+	and c, hc = sh_rec c in
+	(Lambda (sh_na na, t, c), combinesmall 5 (combine3 (Hashtbl.hash na) ht hc))
+      | LetIn (na,b,t,c) ->
+	let b, hb = sh_rec b in
+	let t, ht = sh_rec t in
+	let c, hc = sh_rec c in
+	(LetIn (sh_na na, b, t, c), combinesmall 6 (combine4 (Hashtbl.hash na) hb ht hc))
+      | App (c,l) ->
+	let c, hc = sh_rec c in
+	let hl = hash_term_array l in
+	(App (c, l), combinesmall 7 (combine hl hc))
+      | Evar (e,l) ->
+	let hl = hash_term_array l in
+	(* since the array have been hashed in place : *)
+	(t, combinesmall 8 (combine (Hashtbl.hash e) hl))
+      | Const c ->
+	(Const (sh_con c), combinesmall 9 (Hashtbl.hash c))
+      | Ind ((kn,i) as ind) ->
+	(Ind (sh_ind ind), combinesmall 10 (combine (Hashtbl.hash kn) i))
+      | Construct (((kn,i),j) as c)->
+	(Construct (sh_construct c), combinesmall 11 (combine3 (Hashtbl.hash kn) i j))
+      | Case (ci,p,c,bl) ->
+	let p, hp = sh_rec p
+	and c, hc = sh_rec c in
+	let hbl = hash_term_array bl in
+	let hbl = combine (combine hc hp) hbl in
+	(Case (sh_ci ci, p, c, bl), combinesmall 12 hbl)
+      | Fix (ln,(lna,tl,bl)) ->
+	let hbl = hash_term_array  bl in
+	let htl = hash_term_array  tl in
+	Array.iteri (fun i x -> lna.(i) <- sh_na x) lna;
+	(* since the three arrays have been hashed in place : *)
+	(t, combinesmall 13 (combine (Hashtbl.hash lna) (combine hbl htl)))
+      | CoFix(ln,(lna,tl,bl)) ->
+	let hbl = hash_term_array bl in
+	let htl = hash_term_array tl in
+	Array.iteri (fun i x -> lna.(i) <- sh_na x) lna;
+	(* since the three arrays have been hashed in place : *)
+	(t, combinesmall 14 (combine (Hashtbl.hash lna) (combine hbl htl)))
+      | Meta n ->
+	(t, combinesmall 15 n)
+      | Rel n ->
+	(t, combinesmall 16 n)
+
+  and sh_rec t =
+    let (y, h) = hash_term t in
+    (* [h] must be positive. *)
+    let h = h land 0x3FFFFFFF in
+    (HashsetTerm.repr h y term_table, h)
+
+  in
+  (* Make sure our statically allocated Rels (1 to 16) are considered
+     as canonical, and hence hash-consed to themselves *)
+  ignore (hash_term_array rels);
+
+  fun t -> fst (sh_rec t)
+
+(* Exported hashing fonction on constr, used mainly in plugins.
+   Appears to have slight differences from [snd (hash_term t)] above ? *)
+
+let rec hash t =
+  match kind t with
+    | Var i -> combinesmall 1 (Hashtbl.hash i)
+    | Sort s -> combinesmall 2 (Hashtbl.hash s)
+    | Cast (c, _, _) -> hash c
+    | Prod (_, t, c) -> combinesmall 4 (combine (hash t) (hash c))
+    | Lambda (_, t, c) -> combinesmall 5 (combine (hash t) (hash c))
+    | LetIn (_, b, t, c) ->
+      combinesmall 6 (combine3 (hash b) (hash t) (hash c))
+    | App (Cast(c, _, _),l) -> hash (mkApp (c,l))
+    | App (c,l) ->
+      combinesmall 7 (combine (hash_term_array l) (hash c))
+    | Evar (e,l) ->
+      combinesmall 8 (combine (Hashtbl.hash e) (hash_term_array l))
+    | Const c ->
+      combinesmall 9 (Hashtbl.hash c)	(* TODO: proper hash function for constants *)
+    | Ind (kn,i) ->
+      combinesmall 10 (combine (Hashtbl.hash kn) i)
+    | Construct ((kn,i),j) ->
+      combinesmall 11 (combine3 (Hashtbl.hash kn) i j)
+    | Case (_ , p, c, bl) ->
+      combinesmall 12 (combine3 (hash c) (hash p) (hash_term_array bl))
+    | Fix (ln ,(_, tl, bl)) ->
+      combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl))
+    | CoFix(ln, (_, tl, bl)) ->
+       combinesmall 14 (combine (hash_term_array bl) (hash_term_array tl))
+    | Meta n -> combinesmall 15 n
+    | Rel n -> combinesmall 16 n
+
+and hash_term_array t =
+  Array.fold_left (fun acc t -> combine (hash t) acc) 0 t
+
+module Hcaseinfo =
+  Hashcons.Make(
+    struct
+      type t = case_info
+      type u = inductive -> inductive
+      let hashcons hind ci = { ci with ci_ind = hind ci.ci_ind }
+      let pp_info_equal info1 info2 =
+        Int.equal info1.ind_nargs info2.ind_nargs &&
+        info1.style == info2.style
+      let equal ci ci' =
+	ci.ci_ind == ci'.ci_ind &&
+	Int.equal ci.ci_npar ci'.ci_npar &&
+	Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *)
+	pp_info_equal ci.ci_pp_info ci'.ci_pp_info  (* we use (=) on purpose *)
+      let hash = Hashtbl.hash
+    end)
+
+let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate hcons_ind
+
+let hcons =
+  hashcons
+    (Sorts.hcons,
+     hcons_caseinfo,
+     hcons_construct,
+     hcons_ind,
+     hcons_con,
+     Name.hcons,
+     Id.hcons)
+
+(* let hcons_types = hcons_constr *)
+
+(*******)
+(* Type of abstract machine values *)
+(** FIXME: nothing to do there *)
+type values
diff --git a/kernel/constr.mli b/kernel/constr.mli
new file mode 100644
index 000000000..59430125f
--- /dev/null
+++ b/kernel/constr.mli
@@ -0,0 +1,246 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+
+(** {6 Existential variables } *)
+type existential_key = int
+
+(** {6 Existential variables } *)
+type metavariable = int
+
+(** {6 Case annotation } *)
+type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle 
+  | RegularStyle (** infer printing form from number of constructor *)
+type case_printing =
+  { ind_nargs : int; (** length of the arity of the inductive type *)
+    style     : case_style }
+
+(** the integer is the number of real args, needed for reduction *)
+type case_info =
+  { ci_ind        : inductive;
+    ci_npar       : int;
+    ci_cstr_ndecls : int array; (** number of real args of each constructor *)
+    ci_pp_info    : case_printing (** not interpreted by the kernel *)
+  }
+
+(** {6 The type of constructions } *)
+
+type t
+type constr = t
+(** [types] is the same as [constr] but is intended to be used for
+   documentation to indicate that such or such function specifically works
+   with {e types} (i.e. terms of type a sort).
+   (Rem:plurial form since [type] is a reserved ML keyword) *)
+
+type types = constr
+
+(** {5 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. *)
+
+(** {6 Term constructors. } *)
+
+(** Constructs a DeBrujin index (DB indices begin at 1) *)
+val mkRel : int -> constr
+
+(** Constructs a Variable *)
+val mkVar : Id.t -> constr
+
+(** Constructs an patvar named "?n" *)
+val mkMeta : metavariable -> constr
+
+(** Constructs an existential variable *)
+type existential = existential_key * constr array
+val mkEvar : existential -> constr
+
+(** Construct a sort *)
+val mkSort : Sorts.t -> types
+val mkProp : types
+val mkSet  : types
+val mkType : Univ.universe -> types
+
+
+(** This defines the strategy to use for verifiying a Cast *)
+type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast
+
+(** Constructs the term [t1::t2], i.e. the term t{_ 1} casted with the
+   type t{_ 2} (that means t2 is declared as the type of t1). *)
+val mkCast : constr * cast_kind * constr -> constr
+
+(** Constructs the product [(x:t1)t2] *)
+val mkProd : Name.t * types * types -> types
+
+(** Constructs the abstraction \[x:t{_ 1}\]t{_ 2} *)
+val mkLambda : Name.t * types * constr -> constr
+
+(** Constructs the product [let x = t1 : t2 in t3] *)
+val mkLetIn : Name.t * constr * types * constr -> constr
+
+(** [mkApp (f,[| t_1; ...; t_n |]] constructs the application
+   {% $(f~t_1~\dots~t_n)$ %}. *)
+val mkApp : constr * constr array -> constr
+
+(** Constructs a constant 
+   The array of terms correspond to the variables introduced in the section *)
+val mkConst : constant -> constr
+
+(** Inductive types *)
+
+(** Constructs the ith (co)inductive type of the block named kn 
+   The array of terms correspond to the variables introduced in the section *)
+val mkInd : inductive -> constr
+
+(** Constructs the jth constructor of the ith (co)inductive type of the
+   block named kn. The array of terms correspond to the variables
+   introduced in the section *)
+val mkConstruct : constructor -> constr
+
+(** Constructs a destructor of inductive type.
+    
+    [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] 
+    presented as describe in [ci].
+
+    [p] stucture is [fun args x -> "return clause"]
+
+    [ac]{^ ith} element is ith constructor case presented as 
+    {e lambda construct_args (without params). case_term } *)
+val mkCase : case_info * constr * constr * constr array -> constr
+
+(** If [recindxs = [|i1,...in|]]
+      [funnames = [|f1,.....fn|]]
+      [typarray = [|t1,...tn|]]
+      [bodies   = [|b1,.....bn|]]
+   then [mkFix ((recindxs,i), funnames, typarray, bodies) ]
+   constructs the {% $ %}i{% $ %}th function of the block (counting from 0)
+
+    [Fixpoint f1 [ctx1] = b1
+     with     f2 [ctx2] = b2
+     ...
+     with     fn [ctxn] = bn.]
+
+   where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}.
+*)
+type rec_declaration = Name.t array * types array * constr array
+type fixpoint = (int array * int) * rec_declaration
+val mkFix : fixpoint -> constr
+
+(** If [funnames = [|f1,.....fn|]]
+      [typarray = [|t1,...tn|]]
+      [bodies   = [b1,.....bn]] 
+   then [mkCoFix (i, (funnames, typarray, bodies))]
+   constructs the ith function of the block
+   
+    [CoFixpoint f1 = b1
+     with       f2 = b2
+     ...
+     with       fn = bn.]
+ *)
+type cofixpoint = int * rec_declaration
+val mkCoFix : cofixpoint -> constr
+
+
+(** {6 Concrete type for making pattern-matching. } *)
+
+(** [constr array] is an instance matching definitional [named_context] in
+   the same order (i.e. last argument first) *)
+type 'constr pexistential = existential_key * 'constr array
+type ('constr, 'types) prec_declaration =
+    Name.t array * 'types array * 'constr array
+type ('constr, 'types) pfixpoint =
+    (int array * int) * ('constr, 'types) prec_declaration
+type ('constr, 'types) pcofixpoint =
+    int * ('constr, 'types) prec_declaration
+
+type ('constr, 'types) kind_of_term =
+  | Rel       of int
+  | Var       of Id.t
+  | Meta      of metavariable
+  | Evar      of 'constr pexistential
+  | Sort      of Sorts.t
+  | Cast      of 'constr * cast_kind * 'types
+  | Prod      of Name.t * 'types * 'types
+  | Lambda    of Name.t * 'types * 'constr
+  | LetIn     of Name.t * 'constr * 'types * 'constr
+  | App       of 'constr * 'constr array
+  | Const     of constant
+  | Ind       of inductive
+  | Construct of constructor
+  | Case      of case_info * 'constr * 'constr * 'constr array
+  | Fix       of ('constr, 'types) pfixpoint
+  | CoFix     of ('constr, 'types) pcofixpoint
+
+(** User view of [constr]. For [App], it is ensured there is at
+   least one argument and the function is not itself an applicative
+   term *)
+
+val kind : constr -> (constr, types) kind_of_term
+
+(** [equal a b] is true if [a] equals [b] modulo alpha, casts,
+   and application grouping *)
+val equal : constr -> constr -> bool
+
+(** Total ordering compatible with [equal] *)
+val compare : constr -> constr -> int
+
+(** {6 Functionals working on the immediate subterm of a construction } *)
+
+(** [fold f acc c] folds [f] on the immediate subterms of [c]
+   starting from [acc] and proceeding from left to right according to
+   the usual representation of the constructions; it is not recursive *)
+
+val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a
+
+(** [map f c] maps [f] on the immediate subterms of [c]; it is
+   not recursive and the order with which subterms are processed is
+   not specified *)
+
+val map : (constr -> constr) -> constr -> constr
+
+(** [map_with_binders g f n c] maps [f n] on the immediate
+   subterms of [c]; it carries an extra data [n] (typically a lift
+   index) which is processed by [g] (which typically add 1 to [n]) at
+   each binder traversal; it is not recursive and the order with which
+   subterms are processed is not specified *)
+
+val map_with_binders :
+  ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
+
+(** [iter f c] iters [f] on the immediate subterms of [c]; it is
+   not recursive and the order with which subterms are processed is
+   not specified *)
+
+val iter : (constr -> unit) -> constr -> unit
+
+(** [iter_with_binders g f n c] iters [f n] on the immediate
+   subterms of [c]; it carries an extra data [n] (typically a lift
+   index) which is processed by [g] (which typically add 1 to [n]) at
+   each binder traversal; it is not recursive and the order with which
+   subterms are processed is not specified *)
+
+val iter_with_binders :
+  ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
+
+(** [compare_head f c1 c2] compare [c1] and [c2] using [f] to compare
+   the immediate subterms of [c1] of [c2] if needed; Cast's, binders
+   name and Cases annotations are not taken into account *)
+
+val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool
+
+(** {6 Hashconsing} *)
+
+val hash : constr -> int
+
+(*********************************************************************)
+
+val hcons : constr -> constr
+
+(**************************************)
+
+type values
diff --git a/kernel/context.ml b/kernel/context.ml
new file mode 100644
index 000000000..4bc268da1
--- /dev/null
+++ b/kernel/context.ml
@@ -0,0 +1,64 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+
+(***************************************************************************)
+(*     Type of assumptions                                                 *)
+(***************************************************************************)
+
+type named_declaration = Id.t * Constr.t option * Constr.t
+type rel_declaration = Name.t * Constr.t option * Constr.t
+
+let map_named_declaration f (id, (v : Constr.t option), ty) =
+  (id, Option.map f v, f ty)
+
+let map_rel_declaration = map_named_declaration
+
+let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a)
+let fold_rel_declaration = fold_named_declaration
+
+let exists_named_declaration f (_, v, ty) = Option.cata f false v || f ty
+let exists_rel_declaration f (_, v, ty) = Option.cata f false v || f ty
+
+let for_all_named_declaration f (_, v, ty) = Option.cata f true v && f ty
+let for_all_rel_declaration f (_, v, ty) = Option.cata f true v && f ty
+
+let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
+  Id.equal i1 i2 && Option.equal Constr.equal c1 c2 && Constr.equal t1 t2
+
+let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) =
+  Name.equal n1 n2 && Option.equal Constr.equal c1 c2 && Constr.equal t1 t2
+
+(***************************************************************************)
+(*     Type of local contexts (telescopes)                                 *)
+(***************************************************************************)
+
+(*s Signatures of ordered optionally named variables, intended to be
+   accessed by de Bruijn indices (to represent bound variables) *)
+
+type rel_context = rel_declaration list
+
+let empty_rel_context = []
+
+let add_rel_decl d ctxt = d::ctxt
+
+let rec lookup_rel n sign =
+  match n, sign with
+  | 1, decl :: _ -> decl
+  | n, _ :: sign -> lookup_rel (n-1) sign
+  | _, []        -> raise Not_found
+
+let rel_context_length = List.length
+
+let rel_context_nhyps hyps =
+  let rec nhyps acc = function
+    | [] -> acc
+    | (_,None,_)::hyps -> nhyps (1+acc) hyps
+    | (_,Some _,_)::hyps -> nhyps acc hyps in
+  nhyps 0 hyps
diff --git a/kernel/context.mli b/kernel/context.mli
new file mode 100644
index 000000000..32efb743a
--- /dev/null
+++ b/kernel/context.mli
@@ -0,0 +1,60 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+
+(** {6 Local } *)
+(** A {e declaration} has the form [(name,body,type)]. It is either an
+    {e assumption} if [body=None] or a {e definition} if
+    [body=Some actualbody]. It is referred by {e name} if [na] is an
+    identifier or by {e relative index} if [na] is not an identifier
+    (in the latter case, [na] is of type [name] but just for printing
+    purpose) *)
+
+type named_declaration = Id.t * Constr.t option * Constr.t
+type rel_declaration = Name.t * Constr.t option * Constr.t
+
+val map_named_declaration :
+  (Constr.t -> Constr.t) -> named_declaration -> named_declaration
+val map_rel_declaration :
+  (Constr.t -> Constr.t) -> rel_declaration -> rel_declaration
+
+val fold_named_declaration :
+  (Constr.t -> 'a -> 'a) -> named_declaration -> 'a -> 'a
+val fold_rel_declaration :
+  (Constr.t -> 'a -> 'a) -> rel_declaration -> 'a -> 'a
+
+val exists_named_declaration :
+  (Constr.t -> bool) -> named_declaration -> bool
+val exists_rel_declaration :
+  (Constr.t -> bool) -> rel_declaration -> bool
+
+val for_all_named_declaration :
+  (Constr.t -> bool) -> named_declaration -> bool
+val for_all_rel_declaration :
+  (Constr.t -> bool) -> rel_declaration -> bool
+
+val eq_named_declaration :
+  named_declaration -> named_declaration -> bool
+
+val eq_rel_declaration :
+    rel_declaration -> rel_declaration -> bool
+
+(** {6 Contexts of declarations referred to by de Bruijn indices } *)
+
+(** In [rel_context], more recent declaration is on top *)
+type rel_context = rel_declaration list
+
+val empty_rel_context : rel_context
+val add_rel_decl : rel_declaration -> rel_context -> rel_context
+
+val lookup_rel : int -> rel_context -> rel_declaration
+(** Size of the [rel_context] including LetIns *)
+val rel_context_length : rel_context -> int
+(** Size of the [rel_context] without LetIns *)
+val rel_context_nhyps : rel_context -> int
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 0ff7d64f0..0851f682d 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -17,6 +17,7 @@ open Errors
 open Util
 open Names
 open Term
+open Context
 open Sign
 open Declarations
 open Environ
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 5dd4cb570..d00a20a80 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -14,6 +14,7 @@
 
 open Names
 open Term
+open Context
 open Vm
 open Cemitcodes
 open Cbytecodes
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 3a05f9309..5d9eaa928 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Term
+open Context
 
 (** This module defines the internal representation of global
    declarations. This includes global constants/axioms, mutual
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 0063aa6f2..d3b223505 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -23,9 +23,11 @@
 open Errors
 open Util
 open Names
+open Term
+open Context
 open Sign
+open Vars
 open Univ
-open Term
 open Declarations
 open Pre_env
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index d2ca7b3da..ffe28ddc4 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Term
+open Context
 open Declarations
 open Sign
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 57e638982..77675bd58 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -11,6 +11,8 @@ open Util
 open Names
 open Univ
 open Term
+open Vars
+open Context
 open Declarations
 open Declareops
 open Inductive
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index b93237679..ef4416061 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -11,6 +11,8 @@ open Util
 open Names
 open Univ
 open Term
+open Vars
+open Context
 open Declarations
 open Declareops
 open Environ
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index abf5e6c2c..9a458f02a 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -9,6 +9,7 @@
 open Names
 open Univ
 open Term
+open Context
 open Declarations
 open Environ
 
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index ef3ef6d94..421003560 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -1,6 +1,10 @@
 Names
 Univ
 Esubst
+Sorts
+Constr
+Context
+Vars
 Term
 Mod_subst
 Sign
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index dcf56a23c..f112393cd 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -6,8 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 open Errors
-open Term
 open Names
+open Term
+open Context
 open Declarations
 open Util
 open Nativevalues
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index f365d19c3..922fbae92 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -15,6 +15,7 @@
 
 open Util
 open Names
+open Context
 open Sign
 open Univ
 open Term
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 569e8830a..d3d500b2c 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -10,6 +10,7 @@ open Names
 open Sign
 open Univ
 open Term
+open Context
 open Declarations
 
 (** The type of environments. *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 7a14e57cc..1f5a6a6a0 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -19,6 +19,8 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
+open Context
 open Univ
 open Environ
 open Closure
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 9d1d12573..3f958dc9d 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Term
+open Context
 open Environ
 open Closure
 
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 3fced7119..66c872f12 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -18,6 +18,7 @@
 open Names
 open Util
 open Term
+open Context
 
 (*s Signatures of named hypotheses. Used for section variables and
     goal assumptions. *)
@@ -71,7 +72,7 @@ let iter_named_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
 
 (* Push named declarations on top of a rel context *)
 (* Bizarre. Should be avoided. *)
-let push_named_to_rel_context hyps ctxt =
+(*let push_named_to_rel_context hyps ctxt =
   let rec push = function
     | (id,b,t) :: l ->
 	let s, hyps = push l in
@@ -84,4 +85,4 @@ let push_named_to_rel_context hyps ctxt =
 	let n, ctxt = subst l in
 	(n+1), (map_rel_declaration (substn_vars n s) d)::ctxt
     | [] -> 1, hyps in
-  snd (subst ctxt)
+  snd (subst ctxt)*)
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 6239ab5dc..6e581df34 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -8,6 +8,9 @@
 
 open Names
 open Term
+open Context
+
+(** TODO: Merge this with Context *)
 
 (** {6 Signatures of ordered named declarations } *)
 
@@ -41,7 +44,7 @@ val instance_from_named_context : named_context -> constr array
 (** Signatures of ordered optionally named variables, intended to be
    accessed by de Bruijn indices *)
 
-val push_named_to_rel_context : named_context -> rel_context -> rel_context
+(* val push_named_to_rel_context : named_context -> rel_context -> rel_context *)
 
 (** {6 Recurrence on [rel_context]: older declarations processed first } *)
 val fold_rel_context :
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
new file mode 100644
index 000000000..7ab6b553a
--- /dev/null
+++ b/kernel/sorts.ml
@@ -0,0 +1,64 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Univ
+
+type contents = Pos | Null
+
+type family = InProp | InSet | InType
+
+type t =
+  | Prop of contents                      (* proposition types *)
+  | Type of universe
+
+let prop = Prop Null
+let set = Prop Pos
+let type1 = Type type1_univ
+
+let compare s1 s2 =
+  if s1 == s2 then 0 else
+  match s1, s2 with
+  | Prop c1, Prop c2 ->
+    begin match c1, c2 with
+    | Pos, Pos | Null, Null -> 0
+    | Pos, Null -> -1
+    | Null, Pos -> 1
+    end
+  | Type u1, Type u2 -> Universe.compare u1 u2
+  | Prop _, Type _ -> -1
+  | Type _, Prop _ -> 1
+
+let equal s1 s2 = Int.equal (compare s1 s2) 0
+
+let is_prop = function
+| Prop Null -> true
+| _ -> false
+
+let family = function
+  | Prop Null -> InProp
+  | Prop Pos -> InSet
+  | Type _ -> InType
+
+module Hsorts =
+  Hashcons.Make(
+    struct
+      type _t = t
+      type t = _t
+      type u = universe -> universe
+      let hashcons huniv = function
+          Prop c -> Prop c
+        | Type u -> Type (huniv u)
+      let equal s1 s2 =
+        match (s1,s2) with
+            (Prop c1, Prop c2) -> c1 == c2
+          | (Type u1, Type u2) -> u1 == u2
+          |_ -> false
+      let hash = Hashtbl.hash
+    end)
+
+let hcons = Hashcons.simple_hcons Hsorts.generate hcons_univ
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
new file mode 100644
index 000000000..f15b7cba4
--- /dev/null
+++ b/kernel/sorts.mli
@@ -0,0 +1,29 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** {6 The sorts of CCI. } *)
+
+type contents = Pos | Null
+
+type family = InProp | InSet | InType
+
+type t =
+| Prop of contents       (** Prop and Set *)
+| Type of Univ.universe  (** Type *)
+
+val set  : t
+val prop : t
+val type1  : t
+
+val equal : t -> t -> bool
+val compare : t -> t -> int
+
+val is_prop : t -> bool
+val family : t -> family
+
+val hcons : t -> t
diff --git a/kernel/term.ml b/kernel/term.ml
index 82d534a33..258f8423c 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -6,106 +6,63 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* File initially created by Gérard Huet and Thierry Coquand in 1984 *)
-(* Extension to inductive constructions by Christine Paulin for Coq V5.6 *)
-(* Extension to mutual inductive constructions by Christine Paulin for
-   Coq V5.10.2 *)
-(* Extension to co-inductive constructions by Eduardo Gimenez *)
-(* Optimization of substitution functions by Chet Murthy *)
-(* Optimization of lifting functions by Bruno Barras, Mar 1997 *)
-(* Hash-consing by Bruno Barras in Feb 1998 *)
-(* Restructuration of Coq of the type-checking kernel by Jean-Christophe 
-   Filliâtre, 1999 *)
-(* Abstraction of the syntax of terms and iterators by Hugo Herbelin, 2000 *)
-(* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *)
-
-(* This file defines the internal syntax of the Calculus of
-   Inductive Constructions (CIC) terms together with constructors,
-   destructors, iterators and basic functions *)
-
-open Errors
 open Util
 open Pp
+open Errors
 open Names
-open Univ
-open Esubst
-
+open Context
+open Vars
 
-type existential_key = int
-type metavariable = int
+(**********************************************************************)
+(**         Redeclaration of types from module Constr                 *)
+(**********************************************************************)
 
-(* This defines the strategy to use for verifiying a Cast *)
-(* Warning: REVERTcast is not exported to vo-files; as of r14492, it has to *)
-(* come after the vo-exported cast_kind so as to be compatible with coqchk *)
-type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast
+type contents = Sorts.contents = Pos | Null
 
-(* This defines Cases annotations *)
-type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
-type case_printing =
-  { ind_nargs : int; (* length of the arity of the inductive type *)
-    style     : case_style }
-type case_info =
-  { ci_ind        : inductive;
-    ci_npar       : int;
-    ci_cstr_ndecls : int array; (* number of pattern vars of each constructor *)
-    ci_pp_info    : case_printing (* not interpreted by the kernel *)
-  }
+type sorts = Sorts.t =
+  | Prop of contents       (** Prop and Set *)
+  | Type of Univ.universe  (** Type *)
 
-(* Sorts. *)
+type sorts_family = Sorts.family = InProp | InSet | InType
 
-type contents = Pos | Null
+type constr = Constr.t
+(** Alias types, for compatibility. *)
 
-type sorts =
-  | Prop of contents                      (* proposition types *)
-  | Type of universe
+type types = Constr.t
+(** Same as [constr], for documentation purposes. *)
 
-let prop_sort = Prop Null
-let set_sort = Prop Pos
-let type1_sort = Type type1_univ
+type existential_key = Constr.existential_key
 
-let sorts_ord s1 s2 =
-  if s1 == s2 then 0 else
-  match s1, s2 with
-  | Prop c1, Prop c2 ->
-    begin match c1, c2 with
-    | Pos, Pos | Null, Null -> 0
-    | Pos, Null -> -1
-    | Null, Pos -> 1
-    end
-  | Type u1, Type u2 -> Universe.compare u1 u2
-  | Prop _, Type _ -> -1
-  | Type _, Prop _ -> 1
+type existential = Constr.existential
 
-let sorts_eq s1 s2 = Int.equal (sorts_ord s1 s2) 0
+type metavariable = Constr.metavariable
 
-let is_prop_sort = function
-| Prop Null -> true
-| _ -> false
+type case_style = Constr.case_style =
+  LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
 
-type sorts_family = InProp | InSet | InType
+type case_printing = Constr.case_printing =
+  { ind_nargs : int; style     : case_style }
 
-let family_of_sort = function
-  | Prop Null -> InProp
-  | Prop Pos -> InSet
-  | Type _ -> InType
+type case_info = Constr.case_info =
+  { ci_ind        : inductive;
+    ci_npar       : int;
+    ci_cstr_ndecls : int array;
+    ci_pp_info    : case_printing
+  }
 
-(********************************************************************)
-(*       Constructions as implemented                               *)
-(********************************************************************)
+type cast_kind = Constr.cast_kind =
+  VMcast | NATIVEcast | DEFAULTcast | REVERTcast
 
-(* [constr array] is an instance matching definitional [named_context] in
-   the same order (i.e. last argument first) *)
-type 'constr pexistential = existential_key * 'constr array
+type rec_declaration = Constr.rec_declaration
+type fixpoint = Constr.fixpoint
+type cofixpoint = Constr.cofixpoint
+type 'constr pexistential = 'constr Constr.pexistential
 type ('constr, 'types) prec_declaration =
-    Name.t array * 'types array * 'constr array
-type ('constr, 'types) pfixpoint =
-    (int array * int) * ('constr, 'types) prec_declaration
-type ('constr, 'types) pcofixpoint =
-    int * ('constr, 'types) prec_declaration
-
-(* [Var] is used for named variables and [Rel] for variables as
-   de Bruijn indices. *)
-type ('constr, 'types) kind_of_term =
+  ('constr, 'types) Constr.prec_declaration
+type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint
+type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint
+
+type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term =
   | Rel       of int
   | Var       of Id.t
   | Meta      of metavariable
@@ -123,148 +80,62 @@ type ('constr, 'types) kind_of_term =
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
 
-(* constr is the fixpoint of the previous type. Requires option
-   -rectypes of the Caml compiler to be set *)
-type constr = (constr,constr) kind_of_term
-
-type existential = existential_key * constr array
-type rec_declaration = Name.t array * constr array * constr array
-type fixpoint = (int array * int) * rec_declaration
-type cofixpoint = int * rec_declaration
-
-
-(*********************)
-(* Term constructors *)
-(*********************)
-
-(* Constructs a DeBrujin index with number n *)
-let rels =
-  [|Rel  1;Rel  2;Rel  3;Rel  4;Rel  5;Rel  6;Rel  7; Rel  8;
-    Rel  9;Rel 10;Rel 11;Rel 12;Rel 13;Rel 14;Rel 15; Rel 16|]
-
-let mkRel n = if 0<n & n<=16 then rels.(n-1) else Rel n
-
-(* Construct a type *)
-let mkProp   = Sort prop_sort
-let mkSet    = Sort set_sort
-let mkType u = Sort (Type u)
-let mkSort   = function
-  | Prop Null -> mkProp (* Easy sharing *)
-  | Prop Pos -> mkSet
-  | s -> Sort s
-
-(* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *)
-(* (that means t2 is declared as the type of t1) *)
-let mkCast (t1,k2,t2) =
-  match t1 with
-  | Cast (c,k1, _) when (k1 == VMcast || k1 == NATIVEcast) && k1 == k2 -> Cast (c,k1,t2)
-  | _ -> Cast (t1,k2,t2)
-
-(* Constructs the product (x:t1)t2 *)
-let mkProd (x,t1,t2) = Prod (x,t1,t2)
-
-(* Constructs the abstraction [x:t1]t2 *)
-let mkLambda (x,t1,t2) = Lambda (x,t1,t2)
-
-(* Constructs [x=c_1:t]c_2 *)
-let mkLetIn (x,c1,t,c2) = LetIn (x,c1,t,c2)
-
-(* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *)
-(* We ensure applicative terms have at least one argument and the
-   function is not itself an applicative term *)
-let mkApp (f, a) =
-  if Int.equal (Array.length a) 0 then f else
-    match f with
-      | App (g, cl) -> App (g, Array.append cl a)
-      | _ -> App (f, a)
-
-(* Constructs a constant *)
-let mkConst c = Const c
-
-(* Constructs an existential variable *)
-let mkEvar e = Evar e
-
-(* Constructs the ith (co)inductive type of the block named kn *)
-let mkInd m = Ind m
-
-(* Constructs the jth constructor of the ith (co)inductive type of the
-   block named kn. The array of terms correspond to the variables
-   introduced in the section *)
-let mkConstruct c = Construct c
-
-(* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
-let mkCase (ci, p, c, ac) = Case (ci, p, c, ac)
-
-(* If recindxs = [|i1,...in|]
-      funnames = [|f1,...fn|]
-      typarray = [|t1,...tn|]
-      bodies   = [|b1,...bn|]
-   then
-
-      mkFix ((recindxs,i),(funnames,typarray,bodies))
+type values = Constr.values
 
-   constructs the ith function of the block
-
-    Fixpoint f1 [ctx1] : t1 := b1
-    with     f2 [ctx2] : t2 := b2
-    ...
-    with     fn [ctxn] : tn := bn.
-
-   where the length of the jth context is ij.
-*)
-
-let mkFix fix = Fix fix
-
-(* If funnames = [|f1,...fn|]
-      typarray = [|t1,...tn|]
-      bodies   = [|b1,...bn|]
-   then
-
-      mkCoFix (i,(funnames,typsarray,bodies))
-
-   constructs the ith function of the block
-
-    CoFixpoint f1 : t1 := b1
-    with       f2 : t2 := b2
-    ...
-    with       fn : tn := bn.
-*)
-let mkCoFix cofix= CoFix cofix
-
-(* Constructs an existential variable named "?n" *)
-let mkMeta  n =  Meta n
-
-(* Constructs a Variable named id *)
-let mkVar id = Var id
-
-
-(************************************************************************)
-(*    kind_of_term = constructions as seen by the user                 *)
-(************************************************************************)
+(**********************************************************************)
+(**         Redeclaration of functions from module Constr             *)
+(**********************************************************************)
 
-(* User view of [constr]. For [App], it is ensured there is at
-   least one argument and the function is not itself an applicative
-   term *)
+let set_sort  = Sorts.set
+let prop_sort = Sorts.prop
+let type1_sort  = Sorts.type1
+let sorts_ord = Sorts.compare
+let is_prop_sort = Sorts.is_prop
+let family_of_sort = Sorts.family
+
+(** {6 Term constructors. } *)
+
+let mkRel = Constr.mkRel
+let mkVar = Constr.mkVar
+let mkMeta = Constr.mkMeta
+let mkEvar = Constr.mkEvar
+let mkSort = Constr.mkSort
+let mkProp = Constr.mkProp
+let mkSet  = Constr.mkSet 
+let mkType = Constr.mkType
+let mkCast = Constr.mkCast
+let mkProd = Constr.mkProd
+let mkLambda = Constr.mkLambda
+let mkLetIn = Constr.mkLetIn
+let mkApp = Constr.mkApp
+let mkConst = Constr.mkConst
+let mkInd = Constr.mkInd
+let mkConstruct = Constr.mkConstruct
+let mkCase = Constr.mkCase
+let mkFix = Constr.mkFix
+let mkCoFix = Constr.mkCoFix
 
-let kind_of_term c = c
+(**********************************************************************)
+(**         Aliases of functions from module Constr                   *)
+(**********************************************************************)
 
-(* Experimental, used in Presburger contrib *)
-type ('constr, 'types) kind_of_type =
-  | SortType   of sorts
-  | CastType   of 'types * 'types
-  | ProdType   of Name.t * 'types * 'types
-  | LetInType  of Name.t * 'constr * 'types * 'types
-  | AtomicType of 'constr * 'constr array
+let eq_constr = Constr.equal
+let kind_of_term = Constr.kind
+let constr_ord = Constr.compare
+let fold_constr = Constr.fold
+let map_constr = Constr.map
+let map_constr_with_binders = Constr.map_with_binders
+let iter_constr = Constr.iter
+let iter_constr_with_binders = Constr.iter_with_binders
+let compare_constr = Constr.compare_head
+let hash_constr = Constr.hash
+let hcons_sorts = Sorts.hcons
+let hcons_constr = Constr.hcons
+let hcons_types = Constr.hcons
 
-let kind_of_type = function
-  | Sort s -> SortType s
-  | Cast (c,_,t) -> CastType (c, t)
-  | Prod (na,t,c) -> ProdType (na, t, c)
-  | LetIn (na,b,t,c) -> LetInType (na, b, t, c)
-  | App (c,l) -> AtomicType (c, l)
-  | (Rel _ | Meta _ | Var _ | Evar _ | Const _ | Case _ | Fix _ | CoFix _ | Ind _ as c)
-    -> AtomicType (c,[||])
-  | (Lambda _ | Construct _) -> failwith "Not a type"
+(**********************************************************************)
+(**         HERE BEGINS THE INTERESTING STUFF                         *)
+(**********************************************************************)
 
 (**********************************************************************)
 (*          Non primitive term destructors                            *)
@@ -438,7 +309,7 @@ let rec strip_outer_cast c = match kind_of_term c with
   | Cast (c,_,_) -> strip_outer_cast c
   | _ -> c
 
-(* Fonction spéciale qui laisse les cast clés sous les Fix ou les Case *)
+(* Fonction spéciale qui laisse les cast clés sous les Fix ou les Case *)
 
 let under_outer_cast f c =  match kind_of_term c with
   | Cast (b,k,t) -> mkCast (f b, k, f t)
@@ -457,8 +328,8 @@ let collapse_appl c = match kind_of_term c with
   | App (f,cl) ->
       let rec collapse_rec f cl2 =
         match kind_of_term (strip_outer_cast f) with
-	| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
-	| _ -> mkApp (f,cl2)
+        | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
+        | _ -> mkApp (f,cl2)
       in
       collapse_rec f cl
   | _ -> c
@@ -469,430 +340,9 @@ let decompose_app c =
     | _ -> (c,[])
 
 (****************************************************************************)
-(*              Functions to recur through subterms                         *)
-(****************************************************************************)
-
-(* [fold_constr f acc c] folds [f] on the immediate subterms of [c]
-   starting from [acc] and proceeding from left to right according to
-   the usual representation of the constructions; it is not recursive *)
-
-let fold_constr f acc c = match kind_of_term c with
-  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> acc
-  | Cast (c,_,t) -> f (f acc c) t
-  | Prod (_,t,c) -> f (f acc t) c
-  | Lambda (_,t,c) -> f (f acc t) c
-  | LetIn (_,b,t,c) -> f (f (f acc b) t) c
-  | App (c,l) -> Array.fold_left f (f acc c) l
-  | Evar (_,l) -> Array.fold_left f acc l
-  | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
-  | Fix (_,(lna,tl,bl)) ->
-      let fd = Array.map3 (fun na t b -> (na,t,b)) lna tl bl in
-      Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd
-  | CoFix (_,(lna,tl,bl)) ->
-      let fd = Array.map3 (fun na t b -> (na,t,b)) lna tl bl in
-      Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd
-
-(* [iter_constr f c] iters [f] on the immediate subterms of [c]; it is
-   not recursive and the order with which subterms are processed is
-   not specified *)
-
-let iter_constr f c = match kind_of_term c with
-  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> ()
-  | Cast (c,_,t) -> f c; f t
-  | Prod (_,t,c) -> f t; f c
-  | Lambda (_,t,c) -> f t; f c
-  | LetIn (_,b,t,c) -> f b; f t; f c
-  | App (c,l) -> f c; Array.iter f l
-  | Evar (_,l) -> Array.iter f l
-  | Case (_,p,c,bl) -> f p; f c; Array.iter f bl
-  | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
-  | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
-
-(* [iter_constr_with_binders g f n c] iters [f n] on the immediate
-   subterms of [c]; it carries an extra data [n] (typically a lift
-   index) which is processed by [g] (which typically add 1 to [n]) at
-   each binder traversal; it is not recursive and the order with which
-   subterms are processed is not specified *)
-
-let iter_constr_with_binders g f n c = match kind_of_term c with
-  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> ()
-  | Cast (c,_,t) -> f n c; f n t
-  | Prod (_,t,c) -> f n t; f (g n) c
-  | Lambda (_,t,c) -> f n t; f (g n) c
-  | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c
-  | App (c,l) -> f n c; Array.iter (f n) l
-  | Evar (_,l) -> Array.iter (f n) l
-  | Case (_,p,c,bl) -> f n p; f n c; Array.iter (f n) bl
-  | Fix (_,(_,tl,bl)) ->
-      Array.iter (f n) tl;
-      Array.iter (f (iterate g (Array.length tl) n)) bl
-  | CoFix (_,(_,tl,bl)) ->
-      Array.iter (f n) tl;
-      Array.iter (f (iterate g (Array.length tl) n)) bl
-
-(* [map_constr f c] maps [f] on the immediate subterms of [c]; it is
-   not recursive and the order with which subterms are processed is
-   not specified *)
-
-let map_constr f c = match kind_of_term c with
-  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> c
-  | Cast (c,k,t) -> mkCast (f c, k, f t)
-  | Prod (na,t,c) -> mkProd (na, f t, f c)
-  | Lambda (na,t,c) -> mkLambda (na, f t, f c)
-  | LetIn (na,b,t,c) -> mkLetIn (na, f b, f t, f c)
-  | App (c,l) -> mkApp (f c, Array.map f l)
-  | Evar (e,l) -> mkEvar (e, Array.map f l)
-  | Case (ci,p,c,bl) -> mkCase (ci, f p, f c, Array.map f bl)
-  | Fix (ln,(lna,tl,bl)) ->
-      mkFix (ln,(lna,Array.map f tl,Array.map f bl))
-  | CoFix(ln,(lna,tl,bl)) ->
-      mkCoFix (ln,(lna,Array.map f tl,Array.map f bl))
-
-(* [map_constr_with_binders g f n c] maps [f n] on the immediate
-   subterms of [c]; it carries an extra data [n] (typically a lift
-   index) which is processed by [g] (which typically add 1 to [n]) at
-   each binder traversal; it is not recursive and the order with which
-   subterms are processed is not specified *)
-
-let map_constr_with_binders g f l c = match kind_of_term c with
-  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> c
-  | Cast (c,k,t) -> mkCast (f l c, k, f l t)
-  | Prod (na,t,c) -> mkProd (na, f l t, f (g l) c)
-  | Lambda (na,t,c) -> mkLambda (na, f l t, f (g l) c)
-  | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g l) c)
-  | App (c,al) -> mkApp (f l c, Array.map (f l) al)
-  | Evar (e,al) -> mkEvar (e, Array.map (f l) al)
-  | Case (ci,p,c,bl) -> mkCase (ci, f l p, f l c, Array.map (f l) bl)
-  | Fix (ln,(lna,tl,bl)) ->
-      let l' = iterate g (Array.length tl) l in
-      mkFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
-  | CoFix(ln,(lna,tl,bl)) ->
-      let l' = iterate g (Array.length tl) l in
-      mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
-
-(* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare
-   the immediate subterms of [c1] of [c2] if needed; Cast's,
-   application associativity, binders name and Cases annotations are
-   not taken into account *)
-
-
-let compare_constr f t1 t2 =
-  match kind_of_term t1, kind_of_term t2 with
-  | Rel n1, Rel n2 -> Int.equal n1 n2
-  | Meta m1, Meta m2 -> Int.equal m1 m2
-  | Var id1, Var id2 -> Id.equal id1 id2
-  | Sort s1, Sort s2 -> Int.equal (sorts_ord s1 s2) 0
-  | Cast (c1,_,_), _ -> f c1 t2
-  | _, Cast (c2,_,_) -> f t1 c2
-  | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 && f c1 c2
-  | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 && f c1 c2
-  | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 && f t1 t2 && f c1 c2
-  | App (c1,l1), _ when isCast c1 -> f (mkApp (pi1 (destCast c1),l1)) t2
-  | _, App (c2,l2) when isCast c2 -> f t1 (mkApp (pi1 (destCast c2),l2))
-  | App (c1,l1), App (c2,l2) ->
-    Int.equal (Array.length l1) (Array.length l2) &&
-      f c1 c2 && Array.equal f l1 l2
-  | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 && Array.equal f l1 l2
-  | Const c1, Const c2 -> eq_constant c1 c2
-  | Ind c1, Ind c2 -> eq_ind c1 c2
-  | Construct c1, Construct c2 -> eq_constructor c1 c2
-  | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
-      f p1 p2 & f c1 c2 && Array.equal f bl1 bl2
-  | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
-      Int.equal i1 i2 && Array.equal Int.equal ln1 ln2
-      && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
-  | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-      Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
-  | _ -> false
-
-(*******************************)
-(*  alpha conversion functions *)
-(*******************************)
-
-(* alpha conversion : ignore print names and casts *)
-
-let rec eq_constr m n =
-  (m == n) || compare_constr eq_constr m n
-
-let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *)
-
-let constr_ord_int f t1 t2 =
-  let (=?) f g i1 i2 j1 j2=
-    let c = f i1 i2 in
-    if Int.equal c 0 then g j1 j2 else c in
-  let (==?) fg h i1 i2 j1 j2 k1 k2=
-    let c=fg i1 i2 j1 j2 in
-    if Int.equal c 0 then h k1 k2 else c in
-  let fix_cmp (a1, i1) (a2, i2) =
-    ((Array.compare Int.compare) =? Int.compare) a1 a2 i1 i2
-  in
-  match kind_of_term t1, kind_of_term t2 with
-    | Rel n1, Rel n2 -> Int.compare n1 n2
-    | Meta m1, Meta m2 -> Int.compare m1 m2
-    | Var id1, Var id2 -> Id.compare id1 id2
-    | Sort s1, Sort s2 -> sorts_ord s1 s2
-    | Cast (c1,_,_), _ -> f c1 t2
-    | _, Cast (c2,_,_) -> f t1 c2
-    | Prod (_,t1,c1), Prod (_,t2,c2)
-    | Lambda (_,t1,c1), Lambda (_,t2,c2) ->
-	(f =? f) t1 t2 c1 c2
-    | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) ->
-	((f =? f) ==? f) b1 b2 t1 t2 c1 c2
-    | App (c1,l1), _ when isCast c1 -> f (mkApp (pi1 (destCast c1),l1)) t2
-    | _, App (c2,l2) when isCast c2 -> f t1 (mkApp (pi1 (destCast c2),l2))
-    | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2
-    | Evar (e1,l1), Evar (e2,l2) ->
-	((-) =? (Array.compare f)) e1 e2 l1 l2
-    | Const c1, Const c2 -> con_ord c1 c2
-    | Ind ind1, Ind ind2 -> ind_ord ind1 ind2
-    | Construct ct1, Construct ct2 -> constructor_ord ct1 ct2
-    | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
-	((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2
-    | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
-	((fix_cmp =? (Array.compare f)) ==? (Array.compare f))
-	ln1 ln2 tl1 tl2 bl1 bl2
-    | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-	((Int.compare =? (Array.compare f)) ==? (Array.compare f))
-	ln1 ln2 tl1 tl2 bl1 bl2
-    | t1, t2 -> Pervasives.compare t1 t2
-
-let rec constr_ord m n=
-  constr_ord_int constr_ord m n
-
-(***************************************************************************)
-(*     Type of assumptions                                                 *)
-(***************************************************************************)
-
-type types = constr
-
-type strategy = types option
-
-type named_declaration = Id.t * constr option * types
-type rel_declaration = Name.t * constr option * types
-
-let map_named_declaration f (id, (v : strategy), ty) = (id, Option.map f v, f ty)
-let map_rel_declaration = map_named_declaration
-
-let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a)
-let fold_rel_declaration = fold_named_declaration
-
-let exists_named_declaration f (_, v, ty) = Option.cata f false v || f ty
-let exists_rel_declaration f (_, v, ty) = Option.cata f false v || f ty
-
-let for_all_named_declaration f (_, v, ty) = Option.cata f true v && f ty
-let for_all_rel_declaration f (_, v, ty) = Option.cata f true v && f ty
-
-let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
-  Id.equal i1 i2 && Option.equal eq_constr c1 c2 && eq_constr t1 t2
-
-let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) =
-  Name.equal n1 n2 && Option.equal eq_constr c1 c2 && eq_constr t1 t2
-
-(***************************************************************************)
-(*     Type of local contexts (telescopes)                                 *)
-(***************************************************************************)
-
-(*s Signatures of ordered optionally named variables, intended to be
-   accessed by de Bruijn indices (to represent bound variables) *)
-
-type rel_context = rel_declaration list
-
-let empty_rel_context = []
-
-let add_rel_decl d ctxt = d::ctxt
-
-let rec lookup_rel n sign =
-  match n, sign with
-  | 1, decl :: _ -> decl
-  | n, _ :: sign -> lookup_rel (n-1) sign
-  | _, []        -> raise Not_found
-
-let rel_context_length = List.length
-
-let rel_context_nhyps hyps =
-  let rec nhyps acc = function
-    | [] -> acc
-    | (_,None,_)::hyps -> nhyps (1+acc) hyps
-    | (_,Some _,_)::hyps -> nhyps acc hyps in
-  nhyps 0 hyps
-
-(****************************************************************************)
 (*              Functions for dealing with constr terms                     *)
 (****************************************************************************)
 
-(*********************)
-(*     Occurring     *)
-(*********************)
-
-exception LocalOccur
-
-(* (closedn n M) raises FreeVar if a variable of height greater than n
-   occurs in M, returns () otherwise *)
-
-let closedn n c =
-  let rec closed_rec n c = match kind_of_term c with
-    | Rel m -> if m>n then raise LocalOccur
-    | _ -> iter_constr_with_binders succ closed_rec n c
-  in
-  try closed_rec n c; true with LocalOccur -> false
-
-(* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
-
-let closed0 = closedn 0
-
-(* (noccurn n M) returns true iff (Rel n) does NOT occur in term M  *)
-
-let noccurn n term =
-  let rec occur_rec n c = match kind_of_term c with
-    | Rel m -> if Int.equal m n then raise LocalOccur
-    | _ -> iter_constr_with_binders succ occur_rec n c
-  in
-  try occur_rec n term; true with LocalOccur -> false
-
-(* (noccur_between n m M) returns true iff (Rel p) does NOT occur in term M
-  for n <= p < n+m *)
-
-let noccur_between n m term =
-  let rec occur_rec n c = match kind_of_term c with
-    | Rel(p) -> if n<=p && p<n+m then raise LocalOccur
-    | _        -> iter_constr_with_binders succ occur_rec n c
-  in
-  try occur_rec n term; true with LocalOccur -> false
-
-(* Checking function for terms containing existential variables.
- The function [noccur_with_meta] considers the fact that
- each existential variable (as well as each isevar)
- in the term appears applied to its local context,
- which may contain the CoFix variables. These occurrences of CoFix variables
- are not considered *)
-
-let noccur_with_meta n m term =
-  let rec occur_rec n c = match kind_of_term c with
-    | Rel p -> if n<=p & p<n+m then raise LocalOccur
-    | App(f,cl) ->
-	(match kind_of_term f with
-           | Cast (c,_,_) when isMeta c -> ()
-           | Meta _ -> ()
-	   | _ -> iter_constr_with_binders succ occur_rec n c)
-    | Evar (_, _) -> ()
-    | _ -> iter_constr_with_binders succ occur_rec n c
-  in
-  try (occur_rec n term; true) with LocalOccur -> false
-
-
-(*********************)
-(*      Lifting      *)
-(*********************)
-
-(* The generic lifting function *)
-let rec exliftn el c = match kind_of_term c with
-  | Rel i -> mkRel(reloc_rel i el)
-  | _ -> map_constr_with_binders el_lift exliftn el c
-
-(* Lifting the binding depth across k bindings *)
-
-let liftn n k =
-  match el_liftn (pred k) (el_shft n el_id) with
-    | ELID -> (fun c -> c)
-    | el -> exliftn el
-
-let lift n = liftn n 1
-
-(*********************)
-(*   Substituting    *)
-(*********************)
-
-(* (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 c =
-  let lv = Array.length lamv in
-  if Int.equal lv 0 then c
-  else
-    let rec substrec depth c = match kind_of_term c with
-      | Rel k     ->
-          if k<=depth then c
-          else if k-depth <= lv then lift_substituend depth lamv.(k-depth-1)
-          else mkRel (k-lv)
-      | _ -> map_constr_with_binders succ substrec depth c in
-    substrec n c
-
-(*
-let substkey = Profile.declare_profile "substn_many";;
-let substn_many lamv n c = Profile.profile3 substkey substn_many lamv n c;;
-*)
-
-let substnl laml n =
-  substn_many (Array.map make_substituend (Array.of_list laml)) n
-let substl laml = substnl laml 0
-let subst1 lam = substl [lam]
-
-let substnl_decl laml k = map_rel_declaration (substnl laml k)
-let substl_decl laml = substnl_decl laml 0
-let subst1_decl lam = substl_decl [lam]
-let substl_named_decl = substl_decl
-let subst1_named_decl = subst1_decl
-
-(* (thin_val sigma) removes identity substitutions from sigma *)
-
-let rec thin_val = function
-  | [] -> []
-  | (((id,{ sit = v }) as s)::tl) when isVar v ->
-      if Id.equal id (destVar v) then thin_val tl else s::(thin_val tl)
-  | h::tl -> h::(thin_val tl)
-
-(* (replace_vars sigma M) applies substitution sigma to term M *)
-let replace_vars var_alist =
-  let var_alist =
-    List.map (fun (str,c) -> (str,make_substituend c)) var_alist in
-  let var_alist = thin_val var_alist in
-  let rec substrec n c = match kind_of_term c with
-    | Var x ->
-        (try lift_substituend n (List.assoc x var_alist)
-         with Not_found -> c)
-    | _ -> map_constr_with_binders succ substrec n c
-  in
-  match var_alist with
-  | [] -> (function x -> x)
-  | _ -> substrec 0
-
-(*
-let repvarkey = Profile.declare_profile "replace_vars";;
-let replace_vars vl c = Profile.profile2 repvarkey replace_vars vl c ;;
-*)
-
-(* (subst_var str t) substitute (VAR str) by (Rel 1) in t *)
-let subst_var str = replace_vars [(str, mkRel 1)]
-
-(* (subst_vars [id1;...;idn] t) substitute (VAR idj) by (Rel j) in t *)
-let substn_vars p vars =
-  let _,subst =
-    List.fold_left (fun (n,l) var -> ((n+1),(var,mkRel n)::l)) (p,[]) vars
-  in replace_vars (List.rev subst)
-
-let subst_vars = substn_vars 1
-
 (***************************)
 (* Other term constructors *)
 (***************************)
@@ -997,8 +447,8 @@ let prod_app t n =
   match kind_of_term (strip_outer_cast t) with
     | Prod (_,_,b) -> subst1 n b
     | _ ->
-	errorlabstrm "prod_app"
-	  (str"Needed a product, but didn't find one" ++ fnl ())
+        errorlabstrm "prod_app"
+          (str"Needed a product, but didn't find one" ++ fnl ())
 
 
 (* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
@@ -1177,269 +627,22 @@ let rec isArity c =
   | Sort _          -> true
   | _               -> false
 
-(*******************)
-(*  hash-consing   *)
-(*******************)
-
-(* Hash-consing of [constr] does not use the module [Hashcons] because
-   [Hashcons] is not efficient on deep tree-like data
-   structures. Indeed, [Hashcons] is based the (very efficient)
-   generic hash function [Hashtbl.hash], which computes the hash key
-   through a depth bounded traversal of the data structure to be
-   hashed. As a consequence, for a deep [constr] like the natural
-   number 1000 (S (S (... (S O)))), the same hash is assigned to all
-   the sub [constr]s greater than the maximal depth handled by
-   [Hashtbl.hash]. This entails a huge number of collisions in the
-   hash table and leads to cubic hash-consing in this worst-case.
-
-   In order to compute a hash key that is independent of the data
-   structure depth while being constant-time, an incremental hashing
-   function must be devised. A standard implementation creates a cache
-   of the hashing function by decorating each node of the hash-consed
-   data structure with its hash key. In that case, the hash function
-   can deduce the hash key of a toplevel data structure by a local
-   computation based on the cache held on its substructures.
-   Unfortunately, this simple implementation introduces a space
-   overhead that is damageable for the hash-consing of small [constr]s
-   (the most common case). One can think of an heterogeneous
-   distribution of caches on smartly chosen nodes, but this is forbidden
-   by the use of generic equality in Coq source code. (Indeed, this forces
-   each [constr] to have a unique canonical representation.)
-
-   Given that hash-consing proceeds inductively, we can nonetheless
-   computes the hash key incrementally during hash-consing by changing
-   a little the signature of the hash-consing function: it now returns
-   both the hash-consed term and its hash key. This simple solution is
-   implemented in the following code: it does not introduce a space
-   overhead in [constr], that's why the efficiency is unchanged for
-   small [constr]s. Besides, it does handle deep [constr]s without
-   introducing an unreasonable number of collisions in the hash table.
-   Some benchmarks make us think that this implementation of
-   hash-consing is linear in the size of the hash-consed data
-   structure for our daily use of Coq.
-*)
-
-let array_eqeq t1 t2 =
-  t1 == t2 ||
-  (Int.equal (Array.length t1) (Array.length t2) &&
-   let rec aux i =
-     (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1))
-   in aux 0)
-
-let equals_constr t1 t2 =
-  match t1, t2 with
-    | Rel n1, Rel n2 -> n1 == n2
-    | Meta m1, Meta m2 -> m1 == m2
-    | Var id1, Var id2 -> id1 == id2
-    | Sort s1, Sort s2 -> s1 == s2
-    | Cast (c1,k1,t1), Cast (c2,k2,t2) -> c1 == c2 & k1 == k2 & t1 == t2
-    | Prod (n1,t1,c1), Prod (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2
-    | Lambda (n1,t1,c1), Lambda (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2
-    | LetIn (n1,b1,t1,c1), LetIn (n2,b2,t2,c2) ->
-      n1 == n2 & b1 == b2 & t1 == t2 & c1 == c2
-    | App (c1,l1), App (c2,l2) -> c1 == c2 & array_eqeq l1 l2
-    | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 & array_eqeq l1 l2
-    | Const c1, Const c2 -> c1 == c2
-    | Ind (sp1,i1), Ind (sp2,i2) -> sp1 == sp2 && Int.equal i1 i2
-    | Construct ((sp1,i1),j1), Construct ((sp2,i2),j2) ->
-      sp1 == sp2 && Int.equal i1 i2 && Int.equal j1 j2
-    | Case (ci1,p1,c1,bl1), Case (ci2,p2,c2,bl2) ->
-      ci1 == ci2 & p1 == p2 & c1 == c2 & array_eqeq bl1 bl2
-    | Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) ->
-      Int.equal i1 i2
-      && Array.equal Int.equal ln1 ln2
-      && array_eqeq lna1 lna2
-      && array_eqeq tl1 tl2
-      && array_eqeq bl1 bl2
-    | CoFix(ln1,(lna1,tl1,bl1)), CoFix(ln2,(lna2,tl2,bl2)) ->
-      Int.equal ln1 ln2
-      & array_eqeq lna1 lna2
-      & array_eqeq tl1 tl2
-      & array_eqeq bl1 bl2
-    | _ -> false
-
-(** Note that the following Make has the side effect of creating
-    once and for all the table we'll use for hash-consing all constr *)
-
-module HashsetTerm = Hashset.Make(struct type t = constr let equal = equals_constr end)
-
-let term_table = HashsetTerm.create 19991
-(* The associative table to hashcons terms. *)
-
-open Hashset.Combine
-
-(* [hcons_term hash_consing_functions constr] computes an hash-consed
-   representation for [constr] using [hash_consing_functions] on
-   leaves. *)
-let hcons_term (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
-
-  (* Note : we hash-cons constr arrays *in place* *)
-
-  let rec hash_term_array t =
-    let accu = ref 0 in
-    for i = 0 to Array.length t - 1 do
-      let x, h = sh_rec t.(i) in
-      accu := combine !accu h;
-      t.(i) <- x
-    done;
-    !accu
-
-  and hash_term t =
-    match t with
-      | Var i ->
-	(Var (sh_id i), combinesmall 1 (Hashtbl.hash i))
-      | Sort s ->
-	(Sort (sh_sort s), combinesmall 2 (Hashtbl.hash s))
-      | Cast (c, k, t) ->
-	let c, hc = sh_rec c in
-	let t, ht = sh_rec t in
-	(Cast (c, k, t), combinesmall 3 (combine3 hc (Hashtbl.hash k) ht))
-      | Prod (na,t,c) ->
-	let t, ht = sh_rec t
-	and c, hc = sh_rec c in
-	(Prod (sh_na na, t, c), combinesmall 4 (combine3 (Hashtbl.hash na) ht hc))
-      | Lambda (na,t,c) ->
-	let t, ht = sh_rec t
-	and c, hc = sh_rec c in
-	(Lambda (sh_na na, t, c), combinesmall 5 (combine3 (Hashtbl.hash na) ht hc))
-      | LetIn (na,b,t,c) ->
-	let b, hb = sh_rec b in
-	let t, ht = sh_rec t in
-	let c, hc = sh_rec c in
-	(LetIn (sh_na na, b, t, c), combinesmall 6 (combine4 (Hashtbl.hash na) hb ht hc))
-      | App (c,l) ->
-	let c, hc = sh_rec c in
-	let hl = hash_term_array l in
-	(App (c, l), combinesmall 7 (combine hl hc))
-      | Evar (e,l) ->
-	let hl = hash_term_array l in
-	(* since the array have been hashed in place : *)
-	(t, combinesmall 8 (combine (Hashtbl.hash e) hl))
-      | Const c ->
-	(Const (sh_con c), combinesmall 9 (Hashtbl.hash c))
-      | Ind ((kn,i) as ind) ->
-	(Ind (sh_ind ind), combinesmall 10 (combine (Hashtbl.hash kn) i))
-      | Construct (((kn,i),j) as c)->
-	(Construct (sh_construct c), combinesmall 11 (combine3 (Hashtbl.hash kn) i j))
-      | Case (ci,p,c,bl) ->
-	let p, hp = sh_rec p
-	and c, hc = sh_rec c in
-	let hbl = hash_term_array bl in
-	let hbl = combine (combine hc hp) hbl in
-	(Case (sh_ci ci, p, c, bl), combinesmall 12 hbl)
-      | Fix (ln,(lna,tl,bl)) ->
-	let hbl = hash_term_array  bl in
-	let htl = hash_term_array  tl in
-	Array.iteri (fun i x -> lna.(i) <- sh_na x) lna;
-	(* since the three arrays have been hashed in place : *)
-	(t, combinesmall 13 (combine (Hashtbl.hash lna) (combine hbl htl)))
-      | CoFix(ln,(lna,tl,bl)) ->
-	let hbl = hash_term_array bl in
-	let htl = hash_term_array tl in
-	Array.iteri (fun i x -> lna.(i) <- sh_na x) lna;
-	(* since the three arrays have been hashed in place : *)
-	(t, combinesmall 14 (combine (Hashtbl.hash lna) (combine hbl htl)))
-      | Meta n ->
-	(t, combinesmall 15 n)
-      | Rel n ->
-	(t, combinesmall 16 n)
-
-  and sh_rec t =
-    let (y, h) = hash_term t in
-    (* [h] must be positive. *)
-    let h = h land 0x3FFFFFFF in
-    (HashsetTerm.repr h y term_table, h)
+(** Kind of type *)
 
-  in
-  (* Make sure our statically allocated Rels (1 to 16) are considered
-     as canonical, and hence hash-consed to themselves *)
-  ignore (hash_term_array rels);
-
-  fun t -> fst (sh_rec t)
-
-(* Exported hashing fonction on constr, used mainly in plugins.
-   Appears to have slight differences from [snd (hash_term t)] above ? *)
-
-let rec hash_constr t =
-  match kind_of_term t with
-    | Var i -> combinesmall 1 (Hashtbl.hash i)
-    | Sort s -> combinesmall 2 (Hashtbl.hash s)
-    | Cast (c, _, _) -> hash_constr c
-    | Prod (_, t, c) -> combinesmall 4 (combine (hash_constr t) (hash_constr c))
-    | Lambda (_, t, c) -> combinesmall 5 (combine (hash_constr t) (hash_constr c))
-    | LetIn (_, b, t, c) ->
-      combinesmall 6 (combine3 (hash_constr b) (hash_constr t) (hash_constr c))
-    | App (c,l) when isCast c -> hash_constr (mkApp (pi1 (destCast c),l))
-    | App (c,l) ->
-      combinesmall 7 (combine (hash_term_array l) (hash_constr c))
-    | Evar (e,l) ->
-      combinesmall 8 (combine (Hashtbl.hash e) (hash_term_array l))
-    | Const c ->
-      combinesmall 9 (Hashtbl.hash c)	(* TODO: proper hash function for constants *)
-    | Ind (kn,i) ->
-      combinesmall 10 (combine (Hashtbl.hash kn) i)
-    | Construct ((kn,i),j) ->
-      combinesmall 11 (combine3 (Hashtbl.hash kn) i j)
-    | Case (_ , p, c, bl) ->
-      combinesmall 12 (combine3 (hash_constr c) (hash_constr p) (hash_term_array bl))
-    | Fix (ln ,(_, tl, bl)) ->
-      combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl))
-    | CoFix(ln, (_, tl, bl)) ->
-       combinesmall 14 (combine (hash_term_array bl) (hash_term_array tl))
-    | Meta n -> combinesmall 15 n
-    | Rel n -> combinesmall 16 n
-
-and hash_term_array t =
-  Array.fold_left (fun acc t -> combine (hash_constr t) acc) 0 t
-
-module Hsorts =
-  Hashcons.Make(
-    struct
-      type t = sorts
-      type u = universe -> universe
-      let hashcons huniv = function
-          Prop c -> Prop c
-        | Type u -> Type (huniv u)
-      let equal s1 s2 =
-        match (s1,s2) with
-            (Prop c1, Prop c2) -> c1 == c2
-          | (Type u1, Type u2) -> u1 == u2
-          |_ -> false
-      let hash = Hashtbl.hash
-    end)
-
-module Hcaseinfo =
-  Hashcons.Make(
-    struct
-      type t = case_info
-      type u = inductive -> inductive
-      let hashcons hind ci = { ci with ci_ind = hind ci.ci_ind }
-      let pp_info_equal info1 info2 =
-        Int.equal info1.ind_nargs info2.ind_nargs &&
-        info1.style == info2.style
-      let equal ci ci' =
-	ci.ci_ind == ci'.ci_ind &&
-	Int.equal ci.ci_npar ci'.ci_npar &&
-	Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *)
-	pp_info_equal ci.ci_pp_info ci'.ci_pp_info  (* we use (=) on purpose *)
-      let hash = Hashtbl.hash
-    end)
-
-let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ
-let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate hcons_ind
-
-let hcons_constr =
-  hcons_term
-    (hcons_sorts,
-     hcons_caseinfo,
-     hcons_construct,
-     hcons_ind,
-     hcons_con,
-     Name.hcons,
-     Id.hcons)
-
-let hcons_types = hcons_constr
-
-(*******)
-(* Type of abstract machine values *)
-type values
+(* Experimental, used in Presburger contrib *)
+type ('constr, 'types) kind_of_type =
+  | SortType   of sorts
+  | CastType   of 'types * 'types
+  | ProdType   of Name.t * 'types * 'types
+  | LetInType  of Name.t * 'constr * 'types * 'types
+  | AtomicType of 'constr * 'constr array
+
+let kind_of_type t = match kind_of_term t with
+  | Sort s -> SortType s
+  | Cast (c,_,t) -> CastType (c, t)
+  | Prod (na,t,c) -> ProdType (na, t, c)
+  | LetIn (na,b,t,c) -> LetInType (na, b, t, c)
+  | App (c,l) -> AtomicType (c, l)
+  | (Rel _ | Meta _ | Var _ | Evar _ | Const _ | Case _ | Fix _ | CoFix _ | Ind _)
+    -> AtomicType (t,[||])
+  | (Lambda _ | Construct _) -> failwith "Not a type"
diff --git a/kernel/term.mli b/kernel/term.mli
index e585e66b7..a3745d5e3 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -7,195 +7,61 @@
 (************************************************************************)
 
 open Names
+open Context
 
+(** {5 Redeclaration of types from module Constr and Sorts}
 
-(** {6 The sorts of CCI. } *)
+    This reexports constructors of inductive types defined in module [Constr],
+    for compatibility purposes. Refer to this module for further info.
 
-type contents = Pos | Null
+*)
+
+type contents = Sorts.contents = Pos | Null
 
-type sorts =
+type sorts = Sorts.t =
   | Prop of contents       (** Prop and Set *)
   | Type of Univ.universe  (** Type *)
 
-val set_sort  : sorts
-val prop_sort : sorts
-val type1_sort  : sorts
-
-val sorts_ord : sorts -> sorts -> int
-val is_prop_sort : sorts -> bool
+type sorts_family = Sorts.family = InProp | InSet | InType
 
-(** {6 The sorts family of CCI. } *)
+type constr = Constr.constr
+(** Alias types, for compatibility. *)
 
-type sorts_family = InProp | InSet | InType
+type types = Constr.types
+(** Same as [constr], for documentation purposes. *)
 
-val family_of_sort : sorts -> sorts_family
+type existential_key = Constr.existential_key
 
-(** {6 Useful types } *)
+type existential = Constr.existential
 
-(** {6 Existential variables } *)
-type existential_key = int
+type metavariable = Constr.metavariable
 
-(** {6 Existential variables } *)
-type metavariable = int
+type case_style = Constr.case_style =
+  LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
 
-(** {6 Case annotation } *)
-type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle 
-  | RegularStyle (** infer printing form from number of constructor *)
-type case_printing =
-  { ind_nargs : int; (** length of the arity of the inductive type *)
-    style     : case_style }
+type case_printing = Constr.case_printing =
+  { ind_nargs : int; style     : case_style }
 
-(** the integer is the number of real args, needed for reduction *)
-type case_info =
+type case_info = Constr.case_info =
   { ci_ind        : inductive;
     ci_npar       : int;
-    ci_cstr_ndecls : int array; (** number of real args of each constructor *)
-    ci_pp_info    : case_printing (** not interpreted by the kernel *)
+    ci_cstr_ndecls : int array;
+    ci_pp_info    : case_printing
   }
 
-(** {6 The type of constructions } *)
-
-type constr
-
-(** [eq_constr a b] is true if [a] equals [b] modulo alpha, casts,
-   and application grouping *)
-val eq_constr : constr -> constr -> bool
-
-(** [types] is the same as [constr] but is intended to be used for
-   documentation to indicate that such or such function specifically works
-   with {e types} (i.e. terms of type a sort).
-   (Rem:plurial form since [type] is a reserved ML keyword) *)
-
-type types = constr
-
-(** {5 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. *)
-
-(** {6 Term constructors. } *)
-
-(** Constructs a DeBrujin index (DB indices begin at 1) *)
-val mkRel : int -> constr
-
-(** Constructs a Variable *)
-val mkVar : Id.t -> constr
-
-(** Constructs an patvar named "?n" *)
-val mkMeta : metavariable -> constr
-
-(** Constructs an existential variable *)
-type existential = existential_key * constr array
-val mkEvar : existential -> constr
-
-(** Construct a sort *)
-val mkSort : sorts -> types
-val mkProp : types
-val mkSet  : types
-val mkType : Univ.universe -> types
-
-
-(** This defines the strategy to use for verifiying a Cast *)
-type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast
-
-(** Constructs the term [t1::t2], i.e. the term t{_ 1} casted with the
-   type t{_ 2} (that means t2 is declared as the type of t1). *)
-val mkCast : constr * cast_kind * constr -> constr
-
-(** Constructs the product [(x:t1)t2] *)
-val mkProd : Name.t * types * types -> types
-val mkNamedProd : Id.t -> types -> types -> types
-
-(** non-dependent product [t1 -> t2], an alias for
-   [forall (_:t1), t2]. Beware [t_2] is NOT lifted.
-   Eg: in context [A:Prop], [A->A] is built by [(mkArrow (mkRel 0) (mkRel 1))]
-*)
-val mkArrow : types -> types -> constr
-
-(** Constructs the abstraction \[x:t{_ 1}\]t{_ 2} *)
-val mkLambda : Name.t * types * constr -> constr
-val mkNamedLambda : Id.t -> types -> constr -> constr
-
-(** Constructs the product [let x = t1 : t2 in t3] *)
-val mkLetIn : Name.t * constr * types * constr -> constr
-val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr
-
-(** [mkApp (f,[| t_1; ...; t_n |]] constructs the application
-   {% $(f~t_1~\dots~t_n)$ %}. *)
-val mkApp : constr * constr array -> constr
-
-(** Constructs a constant 
-   The array of terms correspond to the variables introduced in the section *)
-val mkConst : constant -> constr
-
-(** Inductive types *)
-
-(** Constructs the ith (co)inductive type of the block named kn 
-   The array of terms correspond to the variables introduced in the section *)
-val mkInd : inductive -> constr
+type cast_kind = Constr.cast_kind =
+  VMcast | NATIVEcast | DEFAULTcast | REVERTcast
 
-(** Constructs the jth constructor of the ith (co)inductive type of the
-   block named kn. The array of terms correspond to the variables
-   introduced in the section *)
-val mkConstruct : constructor -> constr
-
-(** Constructs a destructor of inductive type.
-    
-    [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] 
-    presented as describe in [ci].
-
-    [p] stucture is [fun args x -> "return clause"]
-
-    [ac]{^ ith} element is ith constructor case presented as 
-    {e lambda construct_args (without params). case_term } *)
-val mkCase : case_info * constr * constr * constr array -> constr
-
-(** If [recindxs = [|i1,...in|]]
-      [funnames = [|f1,.....fn|]]
-      [typarray = [|t1,...tn|]]
-      [bodies   = [|b1,.....bn|]]
-   then [mkFix ((recindxs,i), funnames, typarray, bodies) ]
-   constructs the {% $ %}i{% $ %}th function of the block (counting from 0)
-
-    [Fixpoint f1 [ctx1] = b1
-     with     f2 [ctx2] = b2
-     ...
-     with     fn [ctxn] = bn.]
-
-   where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}.
-*)
-type rec_declaration = Name.t array * types array * constr array
-type fixpoint = (int array * int) * rec_declaration
-val mkFix : fixpoint -> constr
-
-(** If [funnames = [|f1,.....fn|]]
-      [typarray = [|t1,...tn|]]
-      [bodies   = [b1,.....bn]] 
-   then [mkCoFix (i, (funnames, typarray, bodies))]
-   constructs the ith function of the block
-   
-    [CoFixpoint f1 = b1
-     with       f2 = b2
-     ...
-     with       fn = bn.]
- *)
-type cofixpoint = int * rec_declaration
-val mkCoFix : cofixpoint -> constr
-
-
-(** {6 Concrete type for making pattern-matching. } *)
-
-(** [constr array] is an instance matching definitional [named_context] in
-   the same order (i.e. last argument first) *)
-type 'constr pexistential = existential_key * 'constr array
+type rec_declaration = Constr.rec_declaration
+type fixpoint = Constr.fixpoint
+type cofixpoint = Constr.cofixpoint
+type 'constr pexistential = 'constr Constr.pexistential
 type ('constr, 'types) prec_declaration =
-    Name.t array * 'types array * 'constr array
-type ('constr, 'types) pfixpoint =
-    (int array * int) * ('constr, 'types) prec_declaration
-type ('constr, 'types) pcofixpoint =
-    int * ('constr, 'types) prec_declaration
+  ('constr, 'types) Constr.prec_declaration
+type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint
+type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint
 
-type ('constr, 'types) kind_of_term =
+type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term =
   | Rel       of int
   | Var       of Id.t
   | Meta      of metavariable
@@ -213,23 +79,9 @@ type ('constr, 'types) kind_of_term =
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
 
-(** User view of [constr]. For [App], it is ensured there is at
-   least one argument and the function is not itself an applicative
-   term *)
-
-val kind_of_term : constr -> (constr, types) kind_of_term
-
-(** Experimental, used in Presburger contrib *)
-type ('constr, 'types) kind_of_type =
-  | SortType   of sorts
-  | CastType   of 'types * 'types
-  | ProdType   of Name.t * 'types * 'types
-  | LetInType  of Name.t * 'constr * 'types * 'types
-  | AtomicType of 'constr * 'constr array
-
-val kind_of_type : types -> (constr, types) kind_of_type
+type values = Constr.values
 
-(** {6 Simple term case analysis. } *)
+(** {5 Simple term case analysis. } *)
 
 val isRel  : constr -> bool
 val isRelN : int -> constr -> bool
@@ -260,7 +112,7 @@ val iskind : constr -> bool
 val is_small : sorts -> bool
 
 
-(** {6 Term destructors } *)
+(** {5 Term destructors } *)
 (** Destructor operations are partial functions and
     @raise DestKO if the term has not the expected form. *)
 
@@ -331,56 +183,18 @@ val destFix : constr -> fixpoint
 val destCoFix : constr -> cofixpoint
 
 
-(** {6 Local context} *)
-(** A {e declaration} has the form [(name,body,type)]. It is either an
-    {e assumption} if [body=None] or a {e definition} if
-    [body=Some actualbody]. It is referred by {e name} if [na] is an
-    identifier or by {e relative index} if [na] is not an identifier
-    (in the latter case, [na] is of type [name] but just for printing
-    purpose) *)
-
-type named_declaration = Id.t * constr option * types
-type rel_declaration = Name.t * constr option * types
+(** {5 Derived constructors} *)
 
-val map_named_declaration :
-  (constr -> constr) -> named_declaration -> named_declaration
-val map_rel_declaration :
-  (constr -> constr) -> rel_declaration -> rel_declaration
-
-val fold_named_declaration :
-  (constr -> 'a -> 'a) -> named_declaration -> 'a -> 'a
-val fold_rel_declaration :
-  (constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a
-
-val exists_named_declaration :
-  (constr -> bool) -> named_declaration -> bool
-val exists_rel_declaration :
-  (constr -> bool) -> rel_declaration -> bool
-
-val for_all_named_declaration :
-  (constr -> bool) -> named_declaration -> bool
-val for_all_rel_declaration :
-  (constr -> bool) -> rel_declaration -> bool
-
-val eq_named_declaration :
-  named_declaration -> named_declaration -> bool
-
-val eq_rel_declaration :
-    rel_declaration -> rel_declaration -> bool
-
-(** {6 Contexts of declarations referred to by de Bruijn indices } *)
-
-(** In [rel_context], more recent declaration is on top *)
-type rel_context = rel_declaration list
-
-val empty_rel_context : rel_context
-val add_rel_decl : rel_declaration -> rel_context -> rel_context
+(** non-dependent product [t1 -> t2], an alias for
+   [forall (_:t1), t2]. Beware [t_2] is NOT lifted.
+   Eg: in context [A:Prop], [A->A] is built by [(mkArrow (mkRel 0) (mkRel 1))]
+*)
+val mkArrow : types -> types -> constr
 
-val lookup_rel : int -> rel_context -> rel_declaration
-(** Size of the [rel_context] including LetIns *)
-val rel_context_length : rel_context -> int
-(** Size of the [rel_context] without LetIns *)
-val rel_context_nhyps : rel_context -> int
+(** Named version of the functions from [Term]. *)
+val mkNamedLambda : Id.t -> types -> constr -> constr
+val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr
+val mkNamedProd : Id.t -> types -> types -> types
 
 (** Constructs either [(x:t)c] or [[x=b:t]c] *)
 val mkProd_or_LetIn : rel_declaration -> types -> types
@@ -392,7 +206,7 @@ val mkNamedProd_wo_LetIn : named_declaration -> types -> types
 val mkLambda_or_LetIn : rel_declaration -> constr -> constr
 val mkNamedLambda_or_LetIn : named_declaration -> constr -> constr
 
-(** {6 Other term constructors. } *)
+(** {5 Other term constructors. } *)
 
 (** [applist (f,args)] and its variants work as [mkApp] *)
 
@@ -441,7 +255,7 @@ val prod_applist : constr -> constr list -> constr
 val it_mkLambda_or_LetIn : constr -> rel_context -> constr
 val it_mkProd_or_LetIn : types -> rel_context -> types
 
-(** {6 Other term destructors. } *)
+(** {5 Other term destructors. } *)
 
 (** Transforms a product term {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %} into the pair
    {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a product. *)
@@ -512,7 +326,7 @@ val under_casts : (constr -> constr) -> constr -> constr
 (** Apply a function under components of Cast if any *)
 val under_outer_cast : (constr -> constr) -> constr -> constr
 
-(** {6 ... } *)
+(** {5 ... } *)
 (** An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort.
     Such a term can canonically be seen as the pair of a context of types
     and of a sort *)
@@ -528,117 +342,102 @@ val destArity : types -> arity
 (** Tells if a term has the form of an arity *)
 val isArity : types -> bool
 
-(** {6 Occur checks } *)
+(** {5 Kind of type} *)
 
-(** [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *)
-val closedn : int -> constr -> bool
-
-(** [closed0 M] is true iff [M] is a (deBruijn) closed term *)
-val closed0 : constr -> bool
+type ('constr, 'types) kind_of_type =
+  | SortType   of sorts
+  | CastType   of 'types * 'types
+  | ProdType   of Name.t * 'types * 'types
+  | LetInType  of Name.t * 'constr * 'types * 'types
+  | AtomicType of 'constr * 'constr array
 
-(** [noccurn n M] returns true iff [Rel n] does NOT occur in term [M]  *)
-val noccurn : int -> constr -> bool
+val kind_of_type : types -> (constr, types) kind_of_type
 
-(** [noccur_between n m M] returns true iff [Rel p] does NOT occur in term [M]
-  for n <= p < n+m *)
-val noccur_between : int -> int -> constr -> bool
+(** {5 Redeclaration of stuff from module [Sorts]} *)
 
-(** Checking function for terms containing existential- or
-   meta-variables.  The function [noccur_with_meta] does not consider
-   meta-variables applied to some terms (intended to be its local
-   context) (for existential variables, it is necessarily the case) *)
-val noccur_with_meta : int -> int -> constr -> bool
+val set_sort  : sorts
+(** Alias for Sorts.set *)
 
-(** {6 Relocation and substitution } *)
+val prop_sort : sorts
+(** Alias for Sorts.prop *)
 
-(** [exliftn el c] lifts [c] with lifting [el] *)
-val exliftn : Esubst.lift -> constr -> constr
+val type1_sort  : sorts
+(** Alias for Sorts.type1 *)
 
-(** [liftn n k c] lifts by [n] indexes above or equal to [k] in [c] *)
-val liftn : int -> int -> constr -> constr
+val sorts_ord : sorts -> sorts -> int
+(** Alias for Sorts.compare *)
 
-(** [lift n c] lifts by [n] the positive indexes in [c] *)
-val lift : int -> constr -> constr
+val is_prop_sort : sorts -> bool
+(** Alias for Sorts.is_prop *)
 
-(** [substnl [a1;...;an] k c] substitutes in parallel [a1],...,[an]
-    for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates
-    accordingly indexes in [a1],...,[an] *)
-val substnl : constr list -> int -> constr -> constr
-val substl : constr list -> constr -> constr
-val subst1 : constr -> constr -> constr
+val family_of_sort : sorts -> sorts_family
+(** Alias for Sorts.family *)
 
-val substnl_decl : constr list -> int -> rel_declaration -> rel_declaration
-val substl_decl : constr list -> rel_declaration -> rel_declaration
-val subst1_decl : constr -> rel_declaration -> rel_declaration
+(** {5 Redeclaration of stuff from module [Constr]}
 
-val subst1_named_decl : constr -> named_declaration -> named_declaration
-val substl_named_decl : constr list -> named_declaration -> named_declaration
+    See module [Constr] for further info. *)
 
-val replace_vars : (Id.t * constr) list -> constr -> constr
-val subst_var : Id.t -> constr -> constr
+(** {6 Term constructors. } *)
 
-(** [subst_vars [id1;...;idn] t] substitute [VAR idj] by [Rel j] in [t]
-   if two names are identical, the one of least indice is kept *)
-val subst_vars : Id.t list -> constr -> constr
+val mkRel : int -> constr
+val mkVar : Id.t -> constr
+val mkMeta : metavariable -> constr
+val mkEvar : existential -> constr
+val mkSort : sorts -> types
+val mkProp : types
+val mkSet  : types
+val mkType : Univ.universe -> types
+val mkCast : constr * cast_kind * constr -> constr
+val mkProd : Name.t * types * types -> types
+val mkLambda : Name.t * types * constr -> constr
+val mkLetIn : Name.t * constr * types * constr -> constr
+val mkApp : constr * constr array -> constr
+val mkConst : constant -> constr
+val mkInd : inductive -> constr
+val mkConstruct : constructor -> constr
+val mkCase : case_info * constr * constr * constr array -> constr
+val mkFix : fixpoint -> constr
+val mkCoFix : cofixpoint -> constr
 
-(** [substn_vars n [id1;...;idn] t] substitute [VAR idj] by [Rel j+n-1] in [t]
-   if two names are identical, the one of least indice is kept *)
-val substn_vars : int -> Id.t list -> constr -> constr
+(** {6 Aliases} *)
 
+val eq_constr : constr -> constr -> bool
+(** Alias for [Constr.eq] *)
 
-(** {6 Functionals working on the immediate subterm of a construction } *)
+val kind_of_term : constr -> (constr, types) kind_of_term
+(** Alias for [Constr.kind] *)
 
-(** [fold_constr f acc c] folds [f] on the immediate subterms of [c]
-   starting from [acc] and proceeding from left to right according to
-   the usual representation of the constructions; it is not recursive *)
+val constr_ord : constr -> constr -> int
+(** Alias for [Constr.compare] *)
 
 val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a
-
-(** [map_constr f c] maps [f] on the immediate subterms of [c]; it is
-   not recursive and the order with which subterms are processed is
-   not specified *)
+(** Alias for [Constr.fold] *)
 
 val map_constr : (constr -> constr) -> constr -> constr
-
-(** [map_constr_with_binders g f n c] maps [f n] on the immediate
-   subterms of [c]; it carries an extra data [n] (typically a lift
-   index) which is processed by [g] (which typically add 1 to [n]) at
-   each binder traversal; it is not recursive and the order with which
-   subterms are processed is not specified *)
+(** Alias for [Constr.map] *)
 
 val map_constr_with_binders :
   ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
-
-(** [iter_constr f c] iters [f] on the immediate subterms of [c]; it is
-   not recursive and the order with which subterms are processed is
-   not specified *)
+(** Alias for [Constr.map_with_binders] *)
 
 val iter_constr : (constr -> unit) -> constr -> unit
-
-(** [iter_constr_with_binders g f n c] iters [f n] on the immediate
-   subterms of [c]; it carries an extra data [n] (typically a lift
-   index) which is processed by [g] (which typically add 1 to [n]) at
-   each binder traversal; it is not recursive and the order with which
-   subterms are processed is not specified *)
+(** Alias for [Constr.iter] *)
 
 val iter_constr_with_binders :
   ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
-
-(** [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare
-   the immediate subterms of [c1] of [c2] if needed; Cast's, binders
-   name and Cases annotations are not taken into account *)
+(** Alias for [Constr.iter_with_binders] *)
 
 val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
+(** Alias for [Constr.compare_head] *)
 
-val constr_ord : constr -> constr -> int
 val hash_constr : constr -> int
-
-(*********************************************************************)
+(** Alias for [Constr.hash] *)
 
 val hcons_sorts : sorts -> sorts
-val hcons_constr : constr -> constr
-val hcons_types : types -> types
+(** Alias for [Constr.hashcons_sorts] *)
 
-(**************************************)
+val hcons_constr : constr -> constr
+(** Alias for [Constr.hashcons] *)
 
-type values
+val hcons_types : types -> types
+(** Alias for [Constr.hashcons] *)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 67d80fa50..3653e1954 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -17,6 +17,7 @@ open Util
 open Names
 open Univ
 open Term
+open Context
 open Declarations
 open Environ
 open Entries
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 18e6fec79..a27ce1c47 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -11,6 +11,8 @@ open Util
 open Names
 open Univ
 open Term
+open Vars
+open Context
 open Declarations
 open Environ
 open Entries
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 7617e8219..14ba95ec6 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -9,6 +9,7 @@
 open Names
 open Univ
 open Term
+open Context
 open Environ
 open Entries
 open Declarations
diff --git a/kernel/vars.ml b/kernel/vars.ml
new file mode 100644
index 000000000..1469192b1
--- /dev/null
+++ b/kernel/vars.ml
@@ -0,0 +1,186 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Esubst
+open Context
+
+(*********************)
+(*     Occurring     *)
+(*********************)
+
+exception LocalOccur
+
+(* (closedn n M) raises FreeVar if a variable of height greater than n
+   occurs in M, returns () otherwise *)
+
+let closedn n c =
+  let rec closed_rec n c = match Constr.kind c with
+    | Constr.Rel m -> if m>n then raise LocalOccur
+    | _ -> Constr.iter_with_binders succ closed_rec n c
+  in
+  try closed_rec n c; true with LocalOccur -> false
+
+(* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
+
+let closed0 = closedn 0
+
+(* (noccurn n M) returns true iff (Rel n) does NOT occur in term M  *)
+
+let noccurn n term =
+  let rec occur_rec n c = match Constr.kind c with
+    | Constr.Rel m -> if Int.equal m n then raise LocalOccur
+    | _ -> Constr.iter_with_binders succ occur_rec n c
+  in
+  try occur_rec n term; true with LocalOccur -> false
+
+(* (noccur_between n m M) returns true iff (Rel p) does NOT occur in term M
+  for n <= p < n+m *)
+
+let noccur_between n m term =
+  let rec occur_rec n c = match Constr.kind c with
+    | Constr.Rel p -> if n<=p && p<n+m then raise LocalOccur
+    | _        -> Constr.iter_with_binders succ occur_rec n c
+  in
+  try occur_rec n term; true with LocalOccur -> false
+
+(* Checking function for terms containing existential variables.
+ The function [noccur_with_meta] considers the fact that
+ each existential variable (as well as each isevar)
+ in the term appears applied to its local context,
+ which may contain the CoFix variables. These occurrences of CoFix variables
+ are not considered *)
+
+let isMeta c = match Constr.kind c with
+| Constr.Meta _ -> true
+| _ -> false
+
+let noccur_with_meta n m term =
+  let rec occur_rec n c = match Constr.kind c with
+    | Constr.Rel p -> if n<=p & p<n+m then raise LocalOccur
+    | Constr.App(f,cl) ->
+        (match Constr.kind f with
+           | Constr.Cast (c,_,_) when isMeta c -> ()
+           | Constr.Meta _ -> ()
+           | _ -> Constr.iter_with_binders succ occur_rec n c)
+    | Constr.Evar (_, _) -> ()
+    | _ -> Constr.iter_with_binders succ occur_rec n c
+  in
+  try (occur_rec n term; true) with LocalOccur -> false
+
+(*********************)
+(*      Lifting      *)
+(*********************)
+
+(* The generic lifting function *)
+let rec exliftn el c = match Constr.kind c with
+  | Constr.Rel i -> Constr.mkRel(reloc_rel i el)
+  | _ -> Constr.map_with_binders el_lift exliftn el c
+
+(* Lifting the binding depth across k bindings *)
+
+let liftn n k =
+  match el_liftn (pred k) (el_shft n el_id) with
+    | ELID -> (fun c -> c)
+    | el -> exliftn el
+
+let lift n = liftn n 1
+
+(*********************)
+(*   Substituting    *)
+(*********************)
+
+(* (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 c =
+  let lv = Array.length lamv in
+  if Int.equal lv 0 then c
+  else
+    let rec substrec depth c = match Constr.kind c with
+      | Constr.Rel k     ->
+          if k<=depth then c
+          else if k-depth <= lv then lift_substituend depth lamv.(k-depth-1)
+          else Constr.mkRel (k-lv)
+      | _ -> Constr.map_with_binders succ substrec depth c in
+    substrec n c
+
+(*
+let substkey = Profile.declare_profile "substn_many";;
+let substn_many lamv n c = Profile.profile3 substkey substn_many lamv n c;;
+*)
+
+let substnl laml n =
+  substn_many (Array.map make_substituend (Array.of_list laml)) n
+let substl laml = substnl laml 0
+let subst1 lam = substl [lam]
+
+let substnl_decl laml k = map_rel_declaration (substnl laml k)
+let substl_decl laml = substnl_decl laml 0
+let subst1_decl lam = substl_decl [lam]
+
+let substnl_named_decl laml k = map_named_declaration (substnl laml k)
+let substl_named_decl laml = substnl_named_decl laml 0
+let subst1_named_decl lam = substl_named_decl [lam]
+
+(* (thin_val sigma) removes identity substitutions from sigma *)
+
+let rec thin_val = function
+  | [] -> []
+  | s :: tl ->
+    let id, { sit = c } = s in
+    match Constr.kind c with
+    | Constr.Var v -> if Id.equal id v then thin_val tl else s::(thin_val tl)
+    | _ -> s :: (thin_val tl)
+
+(* (replace_vars sigma M) applies substitution sigma to term M *)
+let replace_vars var_alist =
+  let var_alist =
+    List.map (fun (str,c) -> (str,make_substituend c)) var_alist in
+  let var_alist = thin_val var_alist in
+  let rec substrec n c = match Constr.kind c with
+    | Constr.Var x ->
+        (try lift_substituend n (List.assoc x var_alist)
+         with Not_found -> c)
+    | _ -> Constr.map_with_binders succ substrec n c
+  in
+  match var_alist with
+  | [] -> (function x -> x)
+  | _ -> substrec 0
+
+(*
+let repvarkey = Profile.declare_profile "replace_vars";;
+let replace_vars vl c = Profile.profile2 repvarkey replace_vars vl c ;;
+*)
+
+(* (subst_var str t) substitute (VAR str) by (Rel 1) in t *)
+let subst_var str = replace_vars [(str, Constr.mkRel 1)]
+
+(* (subst_vars [id1;...;idn] t) substitute (VAR idj) by (Rel j) in t *)
+let substn_vars p vars =
+  let _,subst =
+    List.fold_left (fun (n,l) var -> ((n+1),(var,Constr.mkRel n)::l)) (p,[]) vars
+  in replace_vars (List.rev subst)
+
+let subst_vars = substn_vars 1
diff --git a/kernel/vars.mli b/kernel/vars.mli
new file mode 100644
index 000000000..240d4d413
--- /dev/null
+++ b/kernel/vars.mli
@@ -0,0 +1,69 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Term
+open Context
+open Sign
+
+(** {6 Occur checks } *)
+
+(** [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *)
+val closedn : int -> constr -> bool
+
+(** [closed0 M] is true iff [M] is a (deBruijn) closed term *)
+val closed0 : constr -> bool
+
+(** [noccurn n M] returns true iff [Rel n] does NOT occur in term [M]  *)
+val noccurn : int -> constr -> bool
+
+(** [noccur_between n m M] returns true iff [Rel p] does NOT occur in term [M]
+  for n <= p < n+m *)
+val noccur_between : int -> int -> constr -> bool
+
+(** Checking function for terms containing existential- or
+   meta-variables.  The function [noccur_with_meta] does not consider
+   meta-variables applied to some terms (intended to be its local
+   context) (for existential variables, it is necessarily the case) *)
+val noccur_with_meta : int -> int -> constr -> bool
+
+(** {6 Relocation and substitution } *)
+
+(** [exliftn el c] lifts [c] with lifting [el] *)
+val exliftn : Esubst.lift -> constr -> constr
+
+(** [liftn n k c] lifts by [n] indexes above or equal to [k] in [c] *)
+val liftn : int -> int -> constr -> constr
+
+(** [lift n c] lifts by [n] the positive indexes in [c] *)
+val lift : int -> constr -> constr
+
+(** [substnl [a1;...;an] k c] substitutes in parallel [a1],...,[an]
+    for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates
+    accordingly indexes in [a1],...,[an] *)
+val substnl : constr list -> int -> constr -> constr
+val substl : constr list -> constr -> constr
+val subst1 : constr -> constr -> constr
+
+val substnl_decl : constr list -> int -> rel_declaration -> rel_declaration
+val substl_decl : constr list -> rel_declaration -> rel_declaration
+val subst1_decl : constr -> rel_declaration -> rel_declaration
+
+val subst1_named_decl : constr -> named_declaration -> named_declaration
+val substl_named_decl : constr list -> named_declaration -> named_declaration
+
+val replace_vars : (Id.t * constr) list -> constr -> constr
+val subst_var : Id.t -> constr -> constr
+
+(** [subst_vars [id1;...;idn] t] substitute [VAR idj] by [Rel j] in [t]
+   if two names are identical, the one of least indice is kept *)
+val subst_vars : Id.t list -> constr -> constr
+
+(** [substn_vars n [id1;...;idn] t] substitute [VAR idj] by [Rel j+n-1] in [t]
+   if two names are identical, the one of least indice is kept *)
+val substn_vars : int -> Id.t list -> constr -> constr
diff --git a/library/global.mli b/library/global.mli
index b1184da11..a06d4640e 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -9,6 +9,7 @@
 open Names
 open Univ
 open Term
+open Context
 open Declarations
 open Entries
 open Indtypes
diff --git a/library/heads.ml b/library/heads.ml
index 022e61156..2a42888d5 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -10,6 +10,7 @@ open Pp
 open Util
 open Names
 open Term
+open Vars
 open Mod_subst
 open Environ
 open Globnames
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 473199cb2..aba908d48 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -15,6 +15,7 @@ open Pp
 open Goptions
 open Names
 open Term
+open Vars
 open Tacmach
 open Evd
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index a5baa00f9..a7800667f 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -13,6 +13,7 @@ open Names
 open Inductiveops
 open Declarations
 open Term
+open Vars
 open Tacmach
 open Tactics
 open Tacticals
@@ -226,7 +227,7 @@ let build_projection intype outtype (cstr:constructor) special default gls=
   let lp=Array.length types in
   let ci=pred (snd cstr) in
   let branch i=
-    let ti=Term.prod_appvect types.(i) argv in
+    let ti= prod_appvect types.(i) argv in
     let rc=fst (decompose_prod_assum ti) in
     let head=
       if i=ci then special else default in
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 9d34dc99a..b9334801c 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -17,6 +17,7 @@ open Decl_mode
 open Pretyping
 open Glob_term
 open Term
+open Vars
 open Pp
 open Decl_kinds
 open Misctypes
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 2ef2c9756..5e55bcfb2 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -25,6 +25,7 @@ open Declarations
 open Tactics
 open Tacticals
 open Term
+open Vars
 open Termops
 open Namegen
 open Reductionops
@@ -301,7 +302,7 @@ let enstack_subsubgoals env se stack gls=
 	    let constructor = mkConstruct(ind,succ i)
 	      (* constructors numbering*) in
 	    let appterm = applist (constructor,params) in
-	    let apptype = Term.prod_applist gentyp params in
+	    let apptype = prod_applist gentyp params in
 	    let rc,_ = Reduction.dest_prod env apptype in
 	    let rec meta_aux last lenv = function
 		[] -> (last,lenv,[])
@@ -638,7 +639,7 @@ let rec build_applist prod = function
     [] -> [],prod
   | n::q ->
       let (_,typ,_) = destProd prod in
-      let ctx,head = build_applist (Term.prod_applist prod [mkMeta n]) q in
+      let ctx,head = build_applist (prod_applist prod [mkMeta n]) q in
 	(n,typ)::ctx,head
 
 let instr_suffices _then cut gls0 =
@@ -671,7 +672,7 @@ let conjunction_arity id gls =
           let gentypes=
             Inductive.arities_of_constructors ind (mib,oib) in
 	  let _ = if Array.length gentypes <> 1 then raise Not_found in
-	  let apptype = Term.prod_applist gentypes.(0) params in
+	  let apptype = prod_applist gentypes.(0) params in
 	  let rc,_ = Reduction.dest_prod env apptype in
 	    List.length rc
       | _ -> raise Not_found
@@ -1218,7 +1219,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	let gen_arities = Inductive.arities_of_constructors ind spec in
 	let f_ids typ =
 	  let sign =
-	    (prod_assum (Term.prod_applist typ params)) in
+	    (prod_assum (prod_applist typ params)) in
 	    find_intro_names sign gls in
 	let constr_args_ids = Array.map f_ids gen_arities in
 	let case_term =
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 903a647fc..a6a9838ae 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -10,6 +10,8 @@
 open Util
 open Names
 open Term
+open Vars
+open Context
 open Declarations
 open Declareops
 open Environ
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 557e9c25d..89ba7b259 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -9,6 +9,7 @@
 open Hipattern
 open Names
 open Term
+open Vars
 open Termops
 open Tacmach
 open Util
@@ -50,12 +51,11 @@ let construct_nhyps ind gls =
 (* indhyps builds the array of arrays of constructor hyps for (ind largs)*)
 let ind_hyps nevar ind largs gls=
   let types= Inductiveops.arities_of_constructors (pf_env gls) ind in
-  let lp=Array.length types in
-  let myhyps i=
-    let t1=Term.prod_applist types.(i) largs in
+  let myhyps t =
+    let t1=prod_applist t largs in
     let t2=snd (decompose_prod_n_assum nevar t1) in
       fst (decompose_prod_assum t2) in
-    Array.init lp myhyps
+    Array.map myhyps types
 
 let special_nf gl=
   let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index f1f04fdb5..59b363393 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -6,8 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open Names
+open Term
+open Context
 open Globnames
 
 val qflag : bool ref
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 6c1709140..5133801ee 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -11,6 +11,7 @@ open Sequent
 open Rules
 open Instances
 open Term
+open Vars
 open Tacmach
 open Tacticals
 
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 12b2304ac..4b15dcae5 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -11,6 +11,7 @@ open Rules
 open Errors
 open Util
 open Term
+open Vars
 open Glob_term
 open Tacmach
 open Tactics
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 8abf9d7e2..02a0dd20d 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -10,6 +10,7 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
 open Tacmach
 open Tactics
 open Tacticals
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 75fd0261a..e59f0419e 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -8,6 +8,7 @@
 
 open Util
 open Term
+open Vars
 open Termops
 open Reductionops
 
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 74d719438..6913b40ea 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -2,6 +2,8 @@ open Printer
 open Errors
 open Util
 open Term
+open Vars
+open Context
 open Namegen
 open Names
 open Declarations
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 50a4703f6..f70ce0092 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -2,6 +2,8 @@ open Printer
 open Errors
 open Util
 open Term
+open Vars
+open Context
 open Namegen
 open Names
 open Declarations
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 1ccfe3c31..088b4a0cd 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -9,6 +9,7 @@
 open Compat
 open Util
 open Term
+open Vars
 open Names
 open Pp
 open Constrexpr
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index fe48cbd88..2b4b6245a 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -2,6 +2,7 @@ open Printer
 open Pp
 open Names
 open Term
+open Vars
 open Glob_term
 open Glob_ops
 open Globnames
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 16b1881f4..e46c1a15a 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -11,6 +11,7 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
 open Pp
 open Globnames
 open Tacticals
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index bf5eba63a..65b4101a0 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -18,6 +18,8 @@ open Vernacexpr
 open Pp
 open Names
 open Term
+open Vars
+open Context
 open Termops
 open Declarations
 open Glob_term
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index a8ffd51ef..34085dca2 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Term
+open Vars
 open Namegen
 open Environ
 open Declarations
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 597b6afb6..5a77bf967 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -298,7 +298,7 @@ let rtauto_tac gls=
 		      build_form formula;
 		      build_proof [] 0 prf|]) in
   let term=
-    Term.applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in
+    applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in
   let build_end_time=System.get_time () in
   let _ = if !verbose then
     begin
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 48741525d..670cd2c47 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -13,6 +13,7 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
 open Closure
 open Environ
 open Libnames
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index 98c485dba..a7a181aa6 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -170,6 +170,7 @@ let family_of_term ty =
 module CPropRetyping =
  struct
   module T = Term
+  module V = Vars
 
   let outsort env sigma t =
    family_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma t)
@@ -178,7 +179,7 @@ module CPropRetyping =
   | [] -> typ
   | h::rest ->
       match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma typ) with
-        | T.Prod (na,c1,c2) -> subst_type env sigma (T.subst1 h c2) rest
+        | T.Prod (na,c1,c2) -> subst_type env sigma (V.subst1 h c2) rest
         | _ -> Errors.anomaly (Pp.str "Non-functional construction")
 
 
@@ -198,7 +199,7 @@ let typeur sigma metamap =
            with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "this is not a well-typed term"))
     | T.Rel n ->
         let (_,_,ty) = Environ.lookup_rel n env in
-        T.lift n ty
+        V.lift n ty
     | T.Var id ->
         (try
           let (_,_,ty) = Environ.lookup_named id env in
@@ -222,7 +223,7 @@ let typeur sigma metamap =
     | T.Lambda (name,c1,c2) ->
           T.mkProd (name, c1, type_of (Environ.push_rel (name,None,c1) env) c2)
     | T.LetIn (name,b,c1,c2) ->
-         T.subst1 b (type_of (Environ.push_rel (name,Some b,c1) env) c2)
+         V.subst1 b (type_of (Environ.push_rel (name,Some b,c1) env) c2)
     | T.Fix ((_,i),(_,tys,_)) -> tys.(i)
     | T.CoFix (i,(_,tys,_)) -> tys.(i)
     | T.App(f,args)->
@@ -326,6 +327,7 @@ let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids
  let module N = Names in
  let module A = Acic in
  let module T = Term in
+ let module V = Vars in
   let fresh_id' = fresh_id seed ids_to_terms constr_to_ids ids_to_father_ids in
    (* CSC: do you have any reasonable substitute for 503? *)
    let terms_to_types = Acic.CicHash.create 503 in
@@ -473,7 +475,7 @@ print_endline "PASSATO" ; flush stdout ;
              in
               let eta_expanded =
                let arguments =
-                List.map (T.lift uninst_vars_length) t @
+                List.map (V.lift uninst_vars_length) t @
                  Termops.rel_list 0 uninst_vars_length
                in
                 Unshare.unshare
@@ -528,7 +530,7 @@ print_endline "PASSATO" ; flush stdout ;
                match n with
                   N.Anonymous -> N.Anonymous
                 | _ ->
-                  if not fake_dependent_products && T.noccurn 1 t then
+                  if not fake_dependent_products && V.noccurn 1 t then
                    N.Anonymous
                   else
                    N.Name
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index c95cf94b6..5a3880b01 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -59,6 +59,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
  (*CSC: functions used do checks that we do not need                       *)
  let rec execute env sigma cstr expectedty =
   let module T = Term in
+  let module V = Vars in
   let module E = Environ in
    (* the type part is the synthesized type *)
    let judgement =
@@ -84,7 +85,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
                 (function (m,bo,ty) ->
                   (* Warning: the substitution should be performed also on bo *)
                   (* This is not done since bo is not used later yet          *)
-                  (m,bo,Unshare.unshare (T.replace_vars [n,he1] ty))
+                  (m,bo,Unshare.unshare (V.replace_vars [n,he1] ty))
                 ) tl2
               in
                iter tl1 tl2'
@@ -161,7 +162,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
               match T.kind_of_term (Reduction.whd_betadeltaiota env typ) with
                  T.Prod (_,c1,c2) ->
                   (Some (Reductionops.nf_beta sigma c1)) ::
-                   (aux (T.subst1 hj c2) restjl)
+                   (aux (V.subst1 hj c2) restjl)
                | _ -> assert false
          in
           Array.of_list (aux j.Environ.uj_type (Array.to_list args))
@@ -249,7 +250,7 @@ if Acic.CicHash.mem subterms_to_types cstr then
    let lara = Array.map (assumption_of_judgment env sigma) larj in
    let env1 = Environ.push_rec_types (names,lara,vdef) env in
    let expectedtypes =
-    Array.map (function i -> Some (Term.lift length i)) lar
+    Array.map (function i -> Some (Vars.lift length i)) lar
    in
    let vdefj = execute_array env1 sigma vdef expectedtypes in
    let vdefv = Array.map Environ.j_val vdefj in
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index e16e8e1cc..5d11dbc81 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -12,6 +12,8 @@ open Util
 open Names
 open Nameops
 open Term
+open Vars
+open Context
 open Termops
 open Namegen
 open Declarations
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index d9f9b9d76..3e4b09148 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -9,6 +9,7 @@
 open Pp
 open Names
 open Term
+open Context
 open Evd
 open Environ
 open Inductiveops
@@ -57,11 +58,11 @@ val compile_cases :
 val constr_of_pat : 
            Environ.env ->
            Evd.evar_map ref ->
-           Term.rel_declaration list ->
+           rel_declaration list ->
            Glob_term.cases_pattern ->
            Names.Id.t list ->
            Glob_term.cases_pattern *
-           (Term.rel_declaration list * Term.constr *
+           (rel_declaration list * Term.constr *
             (Term.types * Term.constr list) * Glob_term.cases_pattern) *
            Names.Id.t list
 
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index a84bbcc54..1334fb285 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -7,8 +7,9 @@
 (************************************************************************)
 
 open Util
-open Term
 open Names
+open Term
+open Vars
 open Closure
 open Esubst
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 7d2ad487c..e97e45580 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -18,6 +18,7 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
 open Reductionops
 open Environ
 open Typeops
@@ -80,7 +81,7 @@ let disc_subset x =
        Ind i ->
 	 let len = Array.length l in
 	 let sigty = delayed_force sig_typ in
-	   if Int.equal len 2 && eq_ind i (Term.destInd sigty)
+	   if Int.equal len 2 && eq_ind i (destInd sigty)
 	   then
 	     let (a, b) = pair_of_array l in
 	       Some (a, b)
@@ -190,7 +191,7 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
 		   (fun f ->
 		      mkLambda (name', a',
 				app_opt env' isevars c2
-				  (mkApp (Term.lift 1 f, [| coec1 |])))))
+				  (mkApp (lift 1 f, [| coec1 |])))))
 
       | App (c, l), App (c', l') ->
 	  (match kind_of_term c, kind_of_term c' with
@@ -200,9 +201,9 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
 	     let prod = delayed_force prod_typ in
 	       (* Sigma types *)
 	       if Int.equal len (Array.length l') && Int.equal len 2 && eq_ind i i'
-		 && (eq_ind i (Term.destInd sigT) || eq_ind i (Term.destInd prod))
+		 && (eq_ind i (destInd sigT) || eq_ind i (destInd prod))
 	       then
-		 if eq_ind i (Term.destInd sigT)
+		 if eq_ind i (destInd sigT)
 		 then
 		   begin
 		     let (a, pb), (a', pb') =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index cc900adb4..9483f0220 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -11,6 +11,8 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
+open Context
 open Inductiveops
 open Environ
 open Glob_term
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 3a8f54904..f2f5c9eff 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -10,6 +10,7 @@ open Errors
 open Pp
 open Names
 open Term
+open Context
 open Sign
 open Environ
 open Glob_term
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 19bced344..39e262a3c 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -10,6 +10,7 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
 open Closure
 open Reduction
 open Reductionops
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b3a2e2a39..1d5dda69f 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -11,6 +11,8 @@ open Util
 open Errors
 open Names
 open Term
+open Vars
+open Context
 open Environ
 open Termops
 open Evd
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 82dda8e0f..5719d750e 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -11,6 +11,8 @@ open Util
 open Pp
 open Names
 open Term
+open Vars
+open Context
 open Termops
 open Namegen
 open Pre_env
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 4db6fdd3e..26d85ac94 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -11,6 +11,7 @@ open Util
 open Names
 open Glob_term
 open Term
+open Context
 open Sign
 open Evd
 open Environ
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 6efdf0455..28b6ac93b 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -12,6 +12,7 @@ open Util
 open Names
 open Nameops
 open Term
+open Vars
 open Termops
 open Environ
 open Globnames
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 8904e2b7b..c0c20a1e3 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -18,6 +18,8 @@ open Libnames
 open Globnames
 open Nameops
 open Term
+open Vars
+open Context
 open Namegen
 open Declarations
 open Declareops
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 610bde687..b0637a972 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -11,6 +11,8 @@ open Util
 open Names
 open Univ
 open Term
+open Vars
+open Context
 open Termops
 open Namegen
 open Declarations
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 4fcc6c6bd..038bf465a 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Term
+open Context
 open Declarations
 open Environ
 open Evd
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 5460d8ba1..ab90b5601 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -16,6 +16,8 @@ open Nameops
 open Termops
 open Reductionops
 open Term
+open Vars
+open Context
 open Pattern
 open Patternops
 open Misctypes
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index bf1adb3cf..a2fa81750 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -15,6 +15,7 @@
 open Util
 open Names
 open Term
+open Vars
 open Nametab
 open Nameops
 open Libnames
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index 6c982451a..095c7a59f 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Term
+open Context
 open Environ
 
 (*********************************************************************
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 9a2a8dce7..ed52f574f 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -8,6 +8,7 @@
 open Pp
 open Errors
 open Term
+open Vars
 open Environ
 open Reduction
 open Univ
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index ef0869fe6..d227e1f2a 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -12,6 +12,7 @@ open Names
 open Globnames
 open Nameops
 open Term
+open Vars
 open Glob_term
 open Glob_ops
 open Pp
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 72cc6502a..d1a0aaf8d 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -9,6 +9,7 @@
 open Util
 open Names
 open Term
+open Vars
 open Termops
 open Namegen
 open Environ
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d4afb3a5f..26325872f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -28,6 +28,8 @@ open Names
 open Sign
 open Evd
 open Term
+open Vars
+open Context
 open Termops
 open Reductionops
 open Environ
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 6a94fa109..b2a9bdcc5 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -10,6 +10,8 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
+open Context
 open Termops
 open Univ
 open Evd
@@ -54,7 +56,7 @@ let compare_stack_shape stk1 stk2 =
 let fold_stack2 f o sk1 sk2 =
   let rec aux o lft1 sk1 lft2 sk2 =
   let fold_array =
-    Array.fold_left2 (fun a x y -> f a (Term.lift lft1 x) (Term.lift lft2 y))
+    Array.fold_left2 (fun a x y -> f a (Vars.lift lft1 x) (Vars.lift lft2 y))
   in
   match sk1,sk2 with
   | [], [] -> o,lft1,lft2
@@ -63,11 +65,11 @@ let fold_stack2 f o sk1 sk2 =
   | Zapp [] :: q1, _ -> aux o lft1 q1 lft2 sk2
   | _, Zapp [] :: q2 -> aux o lft1 sk1 lft2 q2
   | Zapp (t1::l1) :: q1, Zapp (t2::l2) :: q2 ->
-    aux (f o (Term.lift lft1 t1) (Term.lift lft2 t2))
+    aux (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2))
       lft1 (Zapp l1 :: q1) lft2 (Zapp l2 :: q2)
   | Zcase (_,t1,a1,_) :: q1, Zcase (_,t2,a2,_) :: q2 ->
     aux (fold_array
-	   (f o (Term.lift lft1 t1) (Term.lift lft2 t2))
+	   (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2))
 	   a1 a2) lft1 q1 lft2 q2
   | Zfix ((_,(_,a1,b1)),s1,_) :: q1, Zfix ((_,(_,a2,b2)),s2,_) :: q2 ->
     let (o',_,_) = aux (fold_array (fold_array o b1 b2) a1 a2)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 1914b3b1e..e95fc41c0 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Term
+open Context
 open Univ
 open Evd
 open Environ
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index d290d0a47..a49e2026a 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -10,6 +10,7 @@ open Pp
 open Errors
 open Util
 open Term
+open Vars
 open Inductive
 open Inductiveops
 open Names
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index efc2a7467..08d2c7cdf 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -11,6 +11,7 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
 open Libnames
 open Globnames
 open Termops
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 5056c3123..0128f8bde 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -12,6 +12,8 @@ open Util
 open Names
 open Nameops
 open Term
+open Vars
+open Context
 open Environ
 open Locus
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 97ac88183..9547231af 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -10,10 +10,13 @@ open Util
 open Pp
 open Names
 open Term
+open Context
 open Sign
 open Environ
 open Locus
 
+(** TODO: merge this with Term *)
+
 (** Universes *)
 val new_univ_level : unit -> Univ.universe_level
 val new_univ : unit -> Univ.universe
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 86ff2a28f..53171d02c 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -11,6 +11,8 @@ open Names
 open Globnames
 open Decl_kinds
 open Term
+open Vars
+open Context
 open Sign
 open Evd
 open Environ
@@ -109,7 +111,7 @@ let dest_class_app env c =
     global_class_of_constr env cl, args
 
 let dest_class_arity env c =
-  let rels, c = Term.decompose_prod_assum c in
+  let rels, c = decompose_prod_assum c in
     rels, dest_class_app env c
 
 let class_of_constr c =
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 3f10200c0..af6824924 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -10,6 +10,7 @@ open Names
 open Globnames
 open Decl_kinds
 open Term
+open Context
 open Sign
 open Evd
 open Environ
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index d0d90017f..89eb217d2 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -9,6 +9,7 @@
 (*i*)
 open Names
 open Term
+open Context
 open Evd
 open Environ
 open Constrexpr
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 5155b7163..f80ff00fc 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -10,6 +10,7 @@ open Loc
 open Names
 open Decl_kinds
 open Term
+open Context
 open Sign
 open Evd
 open Environ
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 7cf7e5889..008b8b9a3 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -10,6 +10,7 @@ open Pp
 open Errors
 open Util
 open Term
+open Vars
 open Environ
 open Reductionops
 open Type_errors
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 31148ee39..f3014424c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -10,6 +10,7 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
 open Termops
 open Namegen
 open Environ
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index fb8a05a97..4b08f7517 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -9,6 +9,7 @@
 open Names
 open Declarations
 open Term
+open Vars
 open Environ
 open Inductive
 open Reduction
diff --git a/printing/printer.ml b/printing/printer.ml
index 531614e50..27266cfe1 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -11,7 +11,9 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
 open Sign
+open Context
 open Environ
 open Globnames
 open Nametab
diff --git a/printing/printer.mli b/printing/printer.mli
index b99a9f9ab..55058ae16 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -11,6 +11,7 @@ open Names
 open Libnames
 open Globnames
 open Term
+open Context
 open Sign
 open Environ
 open Glob_term
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 6177040cc..156629c19 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -12,6 +12,7 @@ open Util
 open Names
 open Nameops
 open Term
+open Vars
 open Termops
 open Namegen
 open Environ
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 7948020a9..6b794c147 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -9,6 +9,8 @@
 open Util
 open Pp
 open Term
+open Vars
+open Context
 
 (* This module implements the abstract interface to goals *)
 (* A general invariant of the module, is that a goal whose associated
@@ -64,7 +66,7 @@ let rec advance sigma g =
       | Evd.Evar_defined c -> c
       | _ -> Errors.anomaly (Pp.str "Some goal is marked as 'cleared' but is uninstantiated")
     in
-    let (e,_) = Term.destEvar v in
+    let (e,_) = destEvar v in
     let g' = { g with content = e } in
     advance sigma g'
   else
@@ -141,7 +143,7 @@ module Refinable = struct
 
   let mkEvar handle env typ _ rdefs _ _ =
     let ev = Evarutil.e_new_evar rdefs env typ in
-    let (e,_) = Term.destEvar ev in
+    let (e,_) = destEvar ev in
     handle := e::!handle;
     ev
 
@@ -260,7 +262,7 @@ let clear ids env rdefs gl info =
   let (hyps,concl) = Evarutil.clear_hyps_in_evi rdefs hyps concl ids in
   let cleared_env = Environ.reset_with_named_context hyps env in
   let cleared_concl = Evarutil.e_new_evar rdefs cleared_env concl in
-  let (cleared_evar,_) = Term.destEvar cleared_concl in
+  let (cleared_evar,_) = destEvar cleared_concl in
   let cleared_goal = descendent gl cleared_evar in
   rdefs := Evd.define gl.content cleared_concl !rdefs;
   { subgoals = [cleared_goal] }
@@ -396,7 +398,7 @@ let convert_hyp check (id,b,bt as d) env rdefs gl info =
   let new_constr =
     Evarutil.e_new_evar rdefs new_env (concl env rdefs gl info)
   in
-  let (new_evar,_) = Term.destEvar new_constr in
+  let (new_evar,_) = destEvar new_constr in
   let new_goal = descendent gl new_evar in
   rdefs := Evd.define gl.content new_constr !rdefs;
   { subgoals = [new_goal] }
@@ -409,7 +411,7 @@ let convert_concl check cl' env rdefs gl info =
     let new_constr =
       Evarutil.e_new_evar rdefs env cl'
     in
-    let (new_evar,_) = Term.destEvar new_constr in
+    let (new_evar,_) = destEvar new_constr in
     let new_goal = descendent gl new_evar in
     rdefs := Evd.define gl.content new_constr !rdefs;
     { subgoals = [new_goal] }
@@ -431,10 +433,10 @@ let rename_hyp id1 id2 env rdefs gl info =
        Errors.error ((Names.Id.to_string id2)^" is already used.");
   let new_hyps = rename_hyp_sign id1 id2 hyps in
   let new_env = Environ.reset_with_named_context new_hyps env in
-  let new_concl = Term.replace_vars [id1,mkVar id2] (concl env rdefs gl info) in
+  let new_concl = Vars.replace_vars [id1,mkVar id2] (concl env rdefs gl info) in
   let new_subproof = Evarutil.e_new_evar rdefs new_env new_concl in
-  let new_subproof = Term.replace_vars [id2,mkVar id1] new_subproof in
-  let (new_evar,_) = Term.destEvar new_subproof in
+  let new_subproof = Vars.replace_vars [id2,mkVar id1] new_subproof in
+  let (new_evar,_) = destEvar new_subproof in
   let new_goal = descendent gl new_evar in
   rdefs := Evd.define gl.content new_subproof !rdefs;
   { subgoals = [new_goal] }
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 6b587959a..4cd3e4746 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -111,7 +111,7 @@ val clear_body : Names.Id.t list -> subgoals sensitive
 
 (* Changes an hypothesis of the goal with a convertible type and body.
    Checks convertibility if the boolean argument is true. *)
-val convert_hyp : bool -> Term.named_declaration -> subgoals sensitive
+val convert_hyp : bool -> Context.named_declaration -> subgoals sensitive
 
 (* Changes the conclusion of the goal with a convertible type and body.
    Checks convertibility if the boolean argument is true. *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 7ec1b684b..a0781ae6a 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -12,6 +12,8 @@ open Util
 open Names
 open Nameops
 open Term
+open Vars
+open Context
 open Termops
 open Environ
 open Reductionops
@@ -538,7 +540,7 @@ let prim_refiner r sigma goal =
 	     push_named_context_val (id,None,t) sign,cl,sigma) in
         let (sg2,ev2,sigma) = 
 	  Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
-	let oterm = Term.mkApp (Term.mkNamedLambda id t ev2 , [| ev1 |]) in
+	let oterm = Term.mkApp (mkNamedLambda id t ev2 , [| ev1 |]) in
 	let sigma = Goal.V82.partial_solution sigma goal oterm in
         if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
 
@@ -579,7 +581,7 @@ let prim_refiner r sigma goal =
 	let (gls_evs,sigma) =  mk_sign sign all in
 	let (gls,evs) = List.split gls_evs in
 	let ids = List.map pi1 all in
-	let evs = List.map (Term.subst_vars (List.rev ids)) evs in
+	let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
 	let indxs = Array.of_list (List.map (fun n -> n-1) (List.map pi2 all)) in
 	let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
 	let typarray = Array.of_list (List.map pi3 all) in
@@ -622,7 +624,7 @@ let prim_refiner r sigma goal =
 	let (gls_evs,sigma) =  mk_sign sign all in
 	let (gls,evs) = List.split gls_evs in
 	let (ids,types) = List.split all in
-	let evs = List.map (Term.subst_vars (List.rev ids)) evs in
+	let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
 	let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
 	let typarray = Array.of_list types in
 	let bodies = Array.of_list evs in
@@ -695,7 +697,7 @@ let prim_refiner r sigma goal =
         let sign' = rename_hyp id1 id2 sign in
         let cl' = replace_vars [id1,mkVar id2] cl in
 	let (gl,ev,sigma) = mk_goal sign' cl' in
-	let ev = Term.replace_vars [(id2,mkVar id1)] ev in
+	let ev = Vars.replace_vars [(id2,mkVar id1)] ev in
 	let sigma = Goal.V82.partial_solution sigma goal ev in
           ([gl], sigma)
 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index af50059b8..954e2fdb7 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -10,6 +10,7 @@
 open Evd
 open Names
 open Term
+open Context
 open Tacexpr
 open Glob_term
 open Nametab
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 063599535..33945052f 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -11,6 +11,7 @@ open Evd
 open Names
 open Libnames
 open Term
+open Context
 open Pp
 open Tacexpr
 open Glob_term
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 328a3d65b..5b502f2c9 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Term
+open Context
 open Sign
 open Environ
 open Evd
diff --git a/tactics/auto.ml b/tactics/auto.ml
index e05c5384a..470d2e6cf 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -13,6 +13,7 @@ open Names
 open Nameops
 open Namegen
 open Term
+open Vars
 open Termops
 open Inductiveops
 open Environ
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 2ec0c877d..a93f9be26 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Term
+open Context
 open Sign
 open Proof_type
 open Tacmach
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index f86c22bcf..cc1162168 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -48,6 +48,8 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
+open Context
 open Declarations
 open Environ
 open Inductive
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 0e4415344..18e582b31 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -12,6 +12,7 @@ open Util
 open Names
 open Nameops
 open Term
+open Vars
 open Termops
 open Namegen
 open Inductive
diff --git a/tactics/equality.mli b/tactics/equality.mli
index ddef64502..d341db4f4 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -10,6 +10,7 @@
 open Pp
 open Names
 open Term
+open Context
 open Sign
 open Evd
 open Environ
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 0ec167873..af04dcacb 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -271,6 +271,7 @@ END
 (* Hint Resolve                                                       *)
 
 open Term
+open Vars
 open Coqlib
 
 let project_hint pri l2r r =
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 7308b7091..b508fb83b 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -12,6 +12,8 @@ open Util
 open Names
 open Nameops
 open Term
+open Vars
+open Context
 open Termops
 open Namegen
 open Environ
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index c8a3ffd55..86651e76c 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -11,6 +11,7 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
 open Termops
 open Namegen
 open Sign
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 160bcfc70..03b697e8f 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -51,6 +51,7 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
 open Termops
 open Namegen
 open Tacmach
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 19a2f390b..30daa03ea 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -15,6 +15,7 @@ open Names
 open Nameops
 open Namegen
 open Term
+open Vars
 open Termops
 open Reduction
 open Tacticals
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 1d97e2b94..3ab04dcbd 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -10,6 +10,7 @@ open Loc
 open Pp
 open Names
 open Term
+open Context
 open Sign
 open Tacmach
 open Proof_type
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c531a34fa..a4b89f865 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -13,6 +13,8 @@ open Names
 open Nameops
 open Sign
 open Term
+open Vars
+open Context
 open Termops
 open Namegen
 open Declarations
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 84040722e..f39ed97f8 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -10,6 +10,7 @@ open Loc
 open Pp
 open Names
 open Term
+open Context
 open Environ
 open Sign
 open Tacmach
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 3ba32da3c..56bdc810d 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -13,9 +13,10 @@ open Tacmach
 open Errors
 open Util
 open Pp
+open Term
+open Vars
 open Termops
 open Declarations
-open Term
 open Names
 open Globnames
 open Inductiveops
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index b2a9aebdc..f8a76f874 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -12,6 +12,8 @@ open Pp
 open Printer
 open Names
 open Term
+open Vars
+open Context
 open Evd
 open Globnames
 (*i*)
diff --git a/toplevel/autoinstance.mli b/toplevel/autoinstance.mli
index 0be19e4e0..fcd46c3e8 100644
--- a/toplevel/autoinstance.mli
+++ b/toplevel/autoinstance.mli
@@ -11,6 +11,7 @@ open Globnames
 open Typeclasses
 open Names
 open Evd
+open Context
 open Sign
 
 (** {6 Automatic detection of (some) record instances } *)
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 8f8f70816..14473e46f 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -11,6 +11,7 @@ open Util
 open Pp
 open Names
 open Term
+open Vars
 open Termops
 open Entries
 open Environ
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 640bd0b08..78848f1c2 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -9,6 +9,8 @@
 (*i*)
 open Names
 open Term
+open Vars
+open Context
 open Evd
 open Environ
 open Nametab
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 736ba62a9..d05eff126 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -9,6 +9,7 @@
 open Names
 open Decl_kinds
 open Term
+open Context
 open Sign
 open Evd
 open Environ
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 420de5d20..6a3d9a11a 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -11,6 +11,8 @@ open Errors
 open Util
 open Flags
 open Term
+open Vars
+open Context
 open Termops
 open Entries
 open Environ
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 4dd00301f..aeb63c348 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -11,6 +11,7 @@ open Errors
 open Util
 open Sign
 open Term
+open Vars
 open Entries
 open Declarations
 open Cooking
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 2aa2cc36f..7a826c1da 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -182,7 +182,7 @@ let process_goal sigma g =
     let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
     string_of_ppcmds (pr_goal_concl_style_env env norm_constr) in
   let process_hyp h_env d acc =
-    let d = Term.map_named_declaration (Reductionops.nf_evar sigma) d in
+    let d = Context.map_named_declaration (Reductionops.nf_evar sigma) d in
     (string_of_ppcmds (pr_var_decl h_env d)) :: acc in
   let hyps =
     List.rev (Environ.fold_named_context process_hyp env ~init: []) in
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 8c7c377bf..53ee27f3b 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -14,6 +14,7 @@ open Declare
 
 open Term
 open Sign
+open Vars
 open Names
 open Evd
 open Pp
@@ -386,7 +387,7 @@ let obl_substitution expand obls deps =
 
 let subst_deps expand obls deps t =
   let subst = obl_substitution expand obls deps in
-    Term.replace_vars (List.map (fun (n, (_, b)) -> n, b) subst) t
+    Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) subst) t
 
 let rec prod_app t n =
   match kind_of_term (strip_outer_cast t) with
@@ -420,8 +421,8 @@ let subst_prog expand obls ints prg =
        replace_appvars subst (Termops.refresh_universes prg.prg_type))
     else 
       let subst' = List.map (fun (n, (_, b)) -> n, b) subst in
-	(Term.replace_vars subst' prg.prg_body,
-	 Term.replace_vars subst' (Termops.refresh_universes prg.prg_type))
+	(Vars.replace_vars subst' prg.prg_body,
+	 Vars.replace_vars subst' (Termops.refresh_universes prg.prg_type))
 
 let subst_deps_obl obls obl =
   let t' = subst_deps true obls obl.obl_deps obl.obl_type in
@@ -518,7 +519,7 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype =
 	 but doing it properly involves delta-reduction, and it finally
          doesn't seem to worth the effort (except for huge mutual
 	 fixpoints ?) *)
-      let m = Term.nb_prod fixtype in
+      let m = nb_prod fixtype in
       let ctx = fst (decompose_prod_n_assum m fixtype) in
 	List.map_i (fun i _ -> i) 0 ctx
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index b6181590e..c5ec2d7e9 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -13,6 +13,7 @@ open Names
 open Globnames
 open Nameops
 open Term
+open Vars
 open Environ
 open Declarations
 open Entries
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 9e3781fd5..331bf9ed5 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Term
+open Context
 open Sign
 open Vernacexpr
 open Constrexpr
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b1afb3b3e..8cf3767cb 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -170,7 +170,7 @@ let make_cases s =
 	      = Global.lookup_inductive i in
 	Util.Array.fold_right2
 	  (fun consname typ l ->
-	     let al = List.rev (fst (Term.decompose_prod typ)) in
+	     let al = List.rev (fst (decompose_prod typ)) in
 	     let al = Util.List.skipn np al in
 	     let rec rename avoid = function
 	       | [] -> []
@@ -303,7 +303,7 @@ let print_namespace ns =
   let print_constant k body =
     let t =
       match body.Declarations.const_type with
-      | Declarations.PolymorphicArity (ctx,a) -> Term.mkArity (ctx, Term.Type a.Declarations.poly_level)
+      | Declarations.PolymorphicArity (ctx,a) -> mkArity (ctx, Term.Type a.Declarations.poly_level)
       | Declarations.NonPolymorphicType t -> t
     in
     print_kn k ++ str":" ++ spc() ++ Printer.pr_type t