[api] Move structures deprecated in the API to the core.

We do up to `Term` which is the main bulk of the changes.

61 files changed, 652 insertions, 566 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index e8cce0841..e1b086b75 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -23,7 +23,7 @@ open CErrors
 open Util
 open Pp
 open Names
-open Term
+open Constr
 open Vars
 open Environ
 open Esubst
@@ -516,7 +516,7 @@ let zupdate m s =
   else s
 
 let mk_lambda env t =
-  let (rvars,t') = decompose_lam t in
+  let (rvars,t') = Term.decompose_lam t in
   FLambda(List.length rvars, List.rev rvars, t', env)
 
 let destFLambda clos_fun t =
@@ -530,7 +530,7 @@ let destFLambda clos_fun t =
 (* Optimization: do not enclose variables in a closure.
    Makes variable access much faster *)
 let mk_clos e t =
-  match kind_of_term t with
+  match kind t with
     | Rel i -> clos_rel e i
     | Var x -> { norm = Red; term = FFlex (VarKey x) }
     | Const c -> { norm = Red; term = FFlex (ConstKey c) }
@@ -556,7 +556,7 @@ let mk_clos_vect env v = match v with
    subterms.
    Could be used insted of mk_clos. *)
 let mk_clos_deep clos_fun env t =
-  match kind_of_term t with
+  match kind t with
     | (Rel _|Ind _|Const _|Construct _|Var _|Meta _ | Sort _) ->
         mk_clos env t
     | Cast (a,k,b) ->
@@ -655,7 +655,7 @@ let term_of_fconstr =
     match v.term with
       | FCLOS(t,env) when is_subs_id env && is_lift_id lfts -> t
       | FLambda(_,tys,f,e) when is_subs_id e && is_lift_id lfts ->
-          compose_lam (List.rev tys) f
+          Term.compose_lam (List.rev tys) f
       | FFix(fx,e) when is_subs_id e && is_lift_id lfts -> mkFix fx
       | FCoFix(cfx,e) when is_subs_id e && is_lift_id lfts -> mkCoFix cfx
       | _ -> to_constr term_of_fconstr_lift lfts v in
@@ -891,7 +891,7 @@ let rec knh info m stk =
 
 (* The same for pure terms *)
 and knht info e t stk =
-  match kind_of_term t with
+  match kind t with
     | App(a,b) ->
         knht info e a (append_stack (mk_clos_vect e b) stk)
     | Case(ci,p,t,br) ->
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index de1bb120e..28136e1fc 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Environ
 open Esubst
 
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 63b0e6929..9febc6449 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -13,7 +13,7 @@
 (* This file defines the type of bytecode instructions *)
 
 open Names
-open Term
+open Constr
 
 type tag = int
 
@@ -32,13 +32,13 @@ let cofix_evaluated_tag = 7
 let last_variant_tag = 245 
 
 type structured_constant =
-  | Const_sorts of sorts
+  | Const_sorts of Sorts.t
   | Const_ind of inductive
   | Const_proj of Constant.t
   | Const_b0 of tag
   | Const_bn of tag * structured_constant array
-  | Const_univ_level of Univ.universe_level
-  | Const_type of Univ.universe
+  | Const_univ_level of Univ.Level.t
+  | Const_type of Univ.Universe.t
 
 type reloc_table = (tag * int) array
 
@@ -186,7 +186,8 @@ open Pp
 open Util
 
 let pp_sort s =
-  match family_of_sort s with
+  let open Sorts in
+  match family s with
   | InSet -> str "Set"
   | InProp -> str "Prop"
   | InType -> str "Type"
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index e9070b26a..5d37a5840 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -9,7 +9,7 @@
 (* $Id$ *)
 
 open Names
-open Term
+open Constr
 
 type tag = int
 
@@ -26,13 +26,13 @@ val cofix_evaluated_tag : tag
 val last_variant_tag : tag
 
 type structured_constant =
-  | Const_sorts of sorts
+  | Const_sorts of Sorts.t
   | Const_ind of inductive
   | Const_proj of Constant.t
   | Const_b0 of tag
   | Const_bn of tag * structured_constant array
-  | Const_univ_level of Univ.universe_level
-  | Const_type of Univ.universe
+  | Const_univ_level of Univ.Level.t
+  | Const_type of Univ.Universe.t
 
 val pp_struct_const : structured_constant -> Pp.t
 
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 5bac26bf9..5dab2932d 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -14,7 +14,7 @@ open Util
 open Names
 open Cbytecodes
 open Cemitcodes
-open Term
+open Constr
 open Declarations
 open Pre_env
 
@@ -438,12 +438,12 @@ let get_strcst = function
   | _ -> raise Not_found
 
 let rec str_const c =
-  match kind_of_term c with
+  match kind c with
   | Sort s -> Bstrconst (Const_sorts s)
   | Cast(c,_,_) -> str_const c
   | App(f,args) ->
       begin
-	match kind_of_term f with
+	match kind f with
 	| Construct(((kn,j),i),u) -> 
             begin
 	    let oib = lookup_mind kn !global_env in
@@ -596,7 +596,7 @@ let rec get_alias env kn =
 (* sz is the size of the local stack *)
 let rec compile_constr reloc c sz cont =
   set_max_stack_size sz;
-  match kind_of_term c with
+  match kind c with
   | Meta _ -> invalid_arg "Cbytegen.compile_constr : Meta"
   | Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar"
   | Proj (p,c) ->
@@ -621,9 +621,9 @@ let rec compile_constr reloc c sz cont =
 	   (Univ.Instance.to_array u)
 	   sz
 	   cont
-  | Sort (Prop _) | Construct _ ->
+  | Sort (Sorts.Prop _) | Construct _ ->
       compile_str_cst reloc (str_const c) sz cont
-  | Sort (Type u) ->
+  | Sort (Sorts.Type u) ->
      (* We separate global and local universes in [u]. The former will be part
         of the structured constant, while the later (if any) will be applied as
         arguments. *)
@@ -641,7 +641,7 @@ let rec compile_constr reloc c sz cont =
 	LSet.fold (fun lvl u -> Universe.sup u (Universe.make lvl)) global_levels Universe.type0m
       in
       if local_levels = [] then
-	compile_str_cst reloc (Bstrconst (Const_sorts (Type uglob))) sz cont
+	compile_str_cst reloc (Bstrconst (Const_sorts (Sorts.Type uglob))) sz cont
       else
 	let compile_get_univ reloc idx sz cont =
           set_max_stack_size sz;
@@ -659,7 +659,7 @@ let rec compile_constr reloc c sz cont =
 	Kpush :: compile_constr reloc dom (sz+1) (Kmakeprod :: cont) in
       compile_constr reloc (mkLambda(id,dom,codom)) sz cont1
   | Lambda _ ->
-      let params, body = decompose_lam c in
+      let params, body = Term.decompose_lam c in
       let arity = List.length params in
       let r_fun = comp_env_fun arity in
       let lbl_fun = Label.create() in
@@ -672,7 +672,7 @@ let rec compile_constr reloc c sz cont =
 
   | App(f,args) ->
       begin
-	match kind_of_term f with
+	match kind f with
 	| Construct _ -> compile_str_cst reloc (str_const c) sz cont
         | Const (kn,u) -> compile_const reloc kn u args sz cont
 	| _ -> comp_app compile_constr compile_constr reloc f args sz cont
@@ -694,7 +694,7 @@ let rec compile_constr reloc c sz cont =
       done;
       (* Compiling bodies *)
       for i = 0 to ndef - 1 do
-	let params,body = decompose_lam rec_bodies.(i) in
+	let params,body = Term.decompose_lam rec_bodies.(i) in
 	let arity = List.length params in
 	let env_body = comp_env_fix ndef i arity rfv in
 	let cont1 =
@@ -726,7 +726,7 @@ let rec compile_constr reloc c sz cont =
       done;
       (* Compiling bodies *)
       for i = 0 to ndef - 1 do
-	let params,body = decompose_lam rec_bodies.(i) in
+	let params,body = Term.decompose_lam rec_bodies.(i) in
 	let arity = List.length params in
 	let env_body = comp_env_cofix ndef arity rfv in
 	let lbl = Label.create () in
@@ -792,7 +792,7 @@ let rec compile_constr reloc c sz cont =
 	  lbl_consts.(tag) <- lbl_b;
 	  c := code_b
 	else
-	  let args, body = decompose_lam branchs.(i) in
+	  let args, body = Term.decompose_lam branchs.(i) in
 	  let nargs = List.length args in
          
           let code_b =  
@@ -953,9 +953,9 @@ let compile fail_on_error ?universes:(universes=0) env c =
          *)
         let reloc = empty_comp_env () in
         let arity , body =
-          match kind_of_term c with
+          match kind c with
           | Lambda _ ->
-            let params, body = decompose_lam c in
+            let params, body = Term.decompose_lam c in
             List.length params , body
           | _ -> 0 , c
         in
@@ -995,7 +995,7 @@ let compile_constant_body fail_on_error env univs = function
         | Monomorphic_const _ -> 0
         | Polymorphic_const univ -> Univ.AUContext.size univ
       in
-      match kind_of_term body with
+      match kind body with
 	| Const (kn',u) when is_univ_copy instance_size u ->
 	    (* we use the canonical name of the constant*)
 	    let con= Constant.make1 (Constant.canonical kn') in
@@ -1024,7 +1024,7 @@ let compile_structured_int31 fc args =
   if not fc then raise Not_found else
   Const_b0
     (Array.fold_left
-       (fun temp_i -> fun t -> match kind_of_term t with
+       (fun temp_i -> fun t -> match kind t with
           | Construct ((_,d),_) -> 2*temp_i+d-1
           | _ -> raise NotClosed)
        0 args
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 9209e8460..c117d3fb5 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -1,6 +1,14 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 open Cbytecodes
 open Cemitcodes
-open Term
+open Constr
 open Declarations
 open Pre_env
 
diff --git a/kernel/constr.mli b/kernel/constr.mli
index da074d85c..474ab3884 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -87,7 +87,7 @@ val mkEvar : existential -> constr
 val mkSort : Sorts.t -> types
 val mkProp : types
 val mkSet  : types
-val mkType : Univ.universe -> types
+val mkType : Univ.Universe.t -> types
 
 
 (** This defines the strategy to use for verifiying a Cast *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 08fff0ca4..2579ac045 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -17,6 +17,7 @@ open CErrors
 open Util
 open Names
 open Term
+open Constr
 open Declarations
 open Univ
 
@@ -100,42 +101,42 @@ let expmod_constr cache modlist c =
   let share_univs = share_univs cache in
   let update_case_info = update_case_info cache in
   let rec substrec c =
-    match kind_of_term c with
+    match kind c with
       | Case (ci,p,t,br) ->
-	  map_constr substrec (mkCase (update_case_info ci modlist,p,t,br))
+	  Constr.map substrec (mkCase (update_case_info ci modlist,p,t,br))
 
       | Ind (ind,u) ->
 	  (try
 	    share_univs (IndRef ind) u modlist
 	   with
-	    | Not_found -> map_constr substrec c)
+	    | Not_found -> Constr.map substrec c)
 
       | Construct (cstr,u) ->
 	  (try
 	     share_univs (ConstructRef cstr) u modlist
 	   with
-	    | Not_found -> map_constr substrec c)
+	    | Not_found -> Constr.map substrec c)
 
       | Const (cst,u) ->
 	  (try
 	    share_univs (ConstRef cst) u modlist
 	   with
-	    | Not_found -> map_constr substrec c)
+	    | Not_found -> Constr.map substrec c)
 
       | Proj (p, c') ->
           (try 
 	     let p' = share_univs (ConstRef (Projection.constant p)) Univ.Instance.empty modlist in
 	     let make c = Projection.make c (Projection.unfolded p) in
-	     match kind_of_term p' with
+	     match kind p' with
 	     | Const (p',_) -> mkProj (make p', substrec c')
 	     | App (f, args) -> 
-	       (match kind_of_term f with 
+	       (match kind f with 
 	       | Const (p', _) -> mkProj (make p', substrec c')
 	       | _ -> assert false)
 	     | _ -> assert false
-	   with Not_found -> map_constr substrec c)
+	   with Not_found -> Constr.map substrec c)
 
-  | _ -> map_constr substrec c
+  | _ -> Constr.map substrec c
 
   in
   if is_empty_modlist modlist then c
@@ -203,7 +204,7 @@ let cook_constant ~hcons env { from = cb; info } =
   let hyps = Context.Named.map expmod abstract in
   let map c =
     let c = abstract_constant_body (expmod c) hyps in
-    if hcons then hcons_constr c else c
+    if hcons then Constr.hcons c else c
   in
   let body = on_body modlist (hyps, usubst, abs_ctx)
     map
@@ -222,7 +223,7 @@ let cook_constant ~hcons env { from = cb; info } =
     let ((mind, _), _), n' =
       try 
 	let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in
-	  match kind_of_term c' with
+	  match kind c' with
 	  | App (f,l) -> (destInd f, Array.length l)
 	  | Ind ind -> ind, 0
 	  | _ -> assert false 
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 6d1b776c0..7696d7545 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
+open Constr
 open Declarations
 open Environ
 
@@ -26,7 +26,7 @@ type result = {
 }
 
 val cook_constant : hcons:bool -> env -> recipe -> result
-val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr
+val cook_constr : Opaqueproof.cooking_info -> constr -> constr
 
 (** {6 Utility functions used in module [Discharge]. } *)
 
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index d21ea9670..2ffe36fcf 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -14,7 +14,7 @@
 
 open Util
 open Names
-open Term
+open Constr
 open Vm
 open Cemitcodes
 open Cbytecodes
@@ -68,7 +68,7 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with
 | Const_bn (t1, a1), Const_bn (t2, a2) ->
   Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2
 | Const_bn _, _ -> false
-| Const_univ_level l1 , Const_univ_level l2 -> Univ.eq_levels l1 l2
+| Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2
 | Const_univ_level _ , _ -> false
 | Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2
 | Const_type _ , _ -> false
diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli
index 30d0e5588..91bb30e7e 100644
--- a/kernel/csymtable.mli
+++ b/kernel/csymtable.mli
@@ -9,7 +9,7 @@
 (* $Id$ *)
 
 open Names
-open Term
+open Constr
 open Pre_env
 
 val val_of_constr : env -> constr -> values
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 8b949f928..b95796fd8 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 
 (** This module defines the internal representation of global
    declarations. This includes global constants/axioms, mutual
@@ -28,8 +28,8 @@ type engagement = set_predicativity
 *)
 
 type template_arity = {
-  template_param_levels : Univ.universe_level option list;
-  template_level : Univ.universe;
+  template_param_levels : Univ.Level.t option list;
+  template_level : Univ.Universe.t;
 }
 
 type ('a, 'b) declaration_arity = 
@@ -63,8 +63,8 @@ type constant_def =
   | OpaqueDef of Opaqueproof.opaque       (** or an opaque global definition *)
 
 type constant_universes =
-  | Monomorphic_const of Univ.universe_context
-  | Polymorphic_const of Univ.abstract_universe_context
+  | Monomorphic_const of Univ.UContext.t
+  | Polymorphic_const of Univ.AUContext.t
 
 (** The [typing_flags] are instructions to the type-checker which
     modify its behaviour. The typing flags used in the type-checking
@@ -119,7 +119,7 @@ type record_body = (Id.t * Constant.t array * projection_body array) option
 
 type regular_inductive_arity = {
   mind_user_arity : types;
-  mind_sort : sorts;
+  mind_sort : Sorts.t;
 }
 
 type inductive_arity = (regular_inductive_arity, template_arity) declaration_arity
@@ -146,7 +146,7 @@ type one_inductive_body = {
 
     mind_nrealdecls : int; (** Length of realargs context (with let, no params) *)
 
-    mind_kelim : sorts_family list; (** List of allowed elimination sorts *)
+    mind_kelim : Sorts.family list; (** List of allowed elimination sorts *)
 
     mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *)
 
@@ -168,9 +168,9 @@ type one_inductive_body = {
   }
 
 type abstract_inductive_universes =
-  | Monomorphic_ind of Univ.universe_context
-  | Polymorphic_ind of Univ.abstract_universe_context
-  | Cumulative_ind of Univ.abstract_cumulativity_info
+  | Monomorphic_ind of Univ.UContext.t
+  | Polymorphic_ind of Univ.AUContext.t
+  | Cumulative_ind  of Univ.ACumulativityInfo.t
 
 type mutual_inductive_body = {
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index d7329a319..f5c26b33d 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -112,7 +112,7 @@ let subst_const_body sub cb =
     themselves. But would it really bring substantial gains ? *)
 
 let hcons_rel_decl =
-  RelDecl.map_name Names.Name.hcons %> RelDecl.map_value Term.hcons_constr %> RelDecl.map_type Term.hcons_types
+  RelDecl.map_name Names.Name.hcons %> RelDecl.map_value Constr.hcons %> RelDecl.map_type Constr.hcons
 
 let hcons_rel_context l = List.smartmap hcons_rel_decl l
 
@@ -120,7 +120,7 @@ let hcons_const_def = function
   | Undef inl -> Undef inl
   | Def l_constr ->
     let constr = force_constr l_constr in
-    Def (from_val (Term.hcons_constr constr))
+    Def (from_val (Constr.hcons constr))
   | OpaqueDef _ as x -> x (* hashconsed when turned indirect *)
 
 let hcons_const_universes cbu =
@@ -133,7 +133,7 @@ let hcons_const_universes cbu =
 let hcons_const_body cb =
   { cb with
     const_body = hcons_const_def cb.const_body;
-    const_type = Term.hcons_constr cb.const_type;
+    const_type = Constr.hcons cb.const_type;
     const_universes = hcons_const_universes cb.const_universes }
 
 (** {6 Inductive types } *)
@@ -249,8 +249,8 @@ let inductive_is_cumulative mib =
 (** {6 Hash-consing of inductive declarations } *)
 
 let hcons_regular_ind_arity a =
-  { mind_user_arity = Term.hcons_constr a.mind_user_arity;
-    mind_sort = Term.hcons_sorts a.mind_sort }
+  { mind_user_arity = Constr.hcons a.mind_user_arity;
+    mind_sort = Sorts.hcons a.mind_sort }
 
 (** Just as for constants, this hash-consing is quite partial *)
 
@@ -260,8 +260,8 @@ let hcons_ind_arity =
 (** Substitution of inductive declarations *)
 
 let hcons_mind_packet oib =
-  let user = Array.smartmap Term.hcons_types oib.mind_user_lc in
-  let nf = Array.smartmap Term.hcons_types oib.mind_nf_lc in
+  let user = Array.smartmap Constr.hcons oib.mind_user_lc in
+  let nf = Array.smartmap Constr.hcons oib.mind_nf_lc in
   (* Special optim : merge [mind_user_lc] and [mind_nf_lc] if possible *)
   let nf = if Array.equal (==) user nf then user else nf in
   { oib with
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index b2d29759d..198831848 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -27,7 +27,7 @@ val subst_const_body : substitution -> constant_body -> constant_body
 
 val constant_has_body : constant_body -> bool
 
-val constant_polymorphic_context : constant_body -> abstract_universe_context
+val constant_polymorphic_context : constant_body -> AUContext.t
 
 (** Is the constant polymorphic? *)
 val constant_is_polymorphic : constant_body -> bool
@@ -57,7 +57,7 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
 
 val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body
 
-val inductive_polymorphic_context : mutual_inductive_body -> abstract_universe_context
+val inductive_polymorphic_context : mutual_inductive_body -> AUContext.t
 
 (** Is the inductive polymorphic? *)
 val inductive_is_polymorphic : mutual_inductive_body -> bool
diff --git a/kernel/entries.ml b/kernel/entries.ml
index f294c4ce4..185dba409 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 
 (** This module defines the entry types for global declarations. This
    information is entered in the environments. This includes global
@@ -35,9 +35,9 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
 *)
 
 type inductive_universes =
-  | Monomorphic_ind_entry of Univ.universe_context
-  | Polymorphic_ind_entry of Univ.universe_context
-  | Cumulative_ind_entry of Univ.cumulativity_info
+  | Monomorphic_ind_entry of Univ.UContext.t
+  | Polymorphic_ind_entry of Univ.UContext.t
+  | Cumulative_ind_entry  of Univ.CumulativityInfo.t
 
 type one_inductive_entry = {
   mind_entry_typename : Id.t;
@@ -65,8 +65,8 @@ type 'a proof_output = constr Univ.in_universe_context_set * 'a
 type 'a const_entry_body = 'a proof_output Future.computation
 
 type constant_universes_entry =
-  | Monomorphic_const_entry of Univ.universe_context
-  | Polymorphic_const_entry of Univ.universe_context
+  | Monomorphic_const_entry of Univ.UContext.t
+  | Polymorphic_const_entry of Univ.UContext.t
 
 type 'a definition_entry = {
   const_entry_body   : 'a const_entry_body;
@@ -112,7 +112,7 @@ type seff_env =
   [ `Nothing
   (* The proof term and its universes.
      Same as the constant_body's but not in an ephemeron *)
-  | `Opaque of Constr.t * Univ.universe_context_set ]
+  | `Opaque of Constr.t * Univ.ContextSet.t ]
 
 type side_eff =
   | SEsubproof of Constant.t * Declarations.constant_body * seff_env
diff --git a/kernel/environ.ml b/kernel/environ.ml
index c3fd8962e..1afab453a 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -23,7 +23,7 @@
 open CErrors
 open Util
 open Names
-open Term
+open Constr
 open Vars
 open Declarations
 open Pre_env
@@ -391,7 +391,7 @@ let lookup_constructor_variables (ind,_) env =
 (* Returns the list of global variables in a term *)
 
 let vars_of_global env constr =
-  match kind_of_term constr with
+  match kind constr with
       Var id -> Id.Set.singleton id
     | Const (kn, _) -> lookup_constant_variables kn env
     | Ind (ind, _) -> lookup_inductive_variables ind env
@@ -402,12 +402,12 @@ let vars_of_global env constr =
 let global_vars_set env constr =
   let rec filtrec acc c =
     let acc =
-      match kind_of_term c with
+      match kind c with
       | Var _ | Const _ | Ind _ | Construct _ ->
 	  Id.Set.union (vars_of_global env c) acc
       | _ ->
 	  acc in
-    Term.fold_constr filtrec acc c
+    Constr.fold filtrec acc c
   in
     filtrec Id.Set.empty constr
 
@@ -478,7 +478,7 @@ let j_type j = j.uj_type
 
 type 'types punsafe_type_judgment = {
   utj_val : 'types;
-  utj_type : sorts }
+  utj_type : Sorts.t }
 
 type unsafe_type_judgment = types punsafe_type_judgment
 
@@ -538,7 +538,7 @@ let register_one env field entry =
 let register env field entry =
   match field with
     | KInt31 (grp, Int31Type) ->
-        let i31c = match kind_of_term entry with
+        let i31c = match kind entry with
                      | Ind i31t -> mkConstructUi (i31t, 1)
 		     | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.")
 	in
@@ -584,7 +584,7 @@ let dispatch =
 fun rk value field ->
   (* subfunction which shortens the (very common) dispatch of operations *)
   let int31_op_from_const n op prim =
-    match kind_of_term value with
+    match kind value with
       | Const kn ->  int31_op n op prim kn
       | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.")
   in
@@ -601,13 +601,13 @@ fun rk value field ->
               (Pp.str "add_int31_decompilation_from_type called with an abnormal field.")
         in
         let i31bit_type =
-          match kind_of_term int31bit with
+          match kind int31bit with
           | Ind (i31bit_type,_) -> i31bit_type
           |  _ -> anomaly ~label:"Environ.register"
               (Pp.str "Int31Bits should be an inductive type.")
         in
         let int31_decompilation =
-          match kind_of_term value with
+          match kind value with
           | Ind (i31t,_) ->
               constr_of_int31 i31t i31bit_type
           | _ -> anomaly ~label:"Environ.register"
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 37816f1e5..f2066b065 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -7,9 +7,9 @@
 (************************************************************************)
 
 open Names
-open Term
-open Declarations
 open Univ
+open Constr
+open Declarations
 
 (** Unsafe environments. We define here a datatype for environments.
    Since typing is not yet defined, it is not possible to check the
@@ -157,7 +157,7 @@ val constant_value_and_type : env -> Constant.t puniverses ->
   constr option * types * Univ.constraints
 (** The universe context associated to the constant, empty if not 
     polymorphic *)
-val constant_context : env -> Constant.t -> Univ.abstract_universe_context
+val constant_context : env -> Constant.t -> Univ.AUContext.t
 
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
@@ -207,8 +207,8 @@ val add_constraints : Univ.constraints -> env -> env
 
 (** Check constraints are satifiable in the environment. *)
 val check_constraints : Univ.constraints -> env -> bool
-val push_context : ?strict:bool -> Univ.universe_context -> env -> env
-val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env
+val push_context : ?strict:bool -> Univ.UContext.t -> env -> env
+val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env
 val push_constraints_to_env : 'a Univ.constrained -> env -> env
 
 val set_engagement : engagement -> env -> env
@@ -247,7 +247,7 @@ val j_type : ('constr, 'types) punsafe_judgment -> 'types
 
 type 'types punsafe_type_judgment = {
   utj_val : 'types;
-  utj_type : sorts }
+  utj_type : Sorts.t }
 
 type unsafe_type_judgment = types punsafe_type_judgment
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index c0f564dc3..f4e611c19 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -11,6 +11,7 @@ open Util
 open Names
 open Univ
 open Term
+open Constr
 open Vars
 open Declarations
 open Declareops
@@ -55,7 +56,7 @@ let weaker_noccur_between env x nvars t =
    else None
 
 let is_constructor_head t =
-  isRel(fst(decompose_app t))
+  Term.isRel(fst(Term.decompose_app t))
 
 (************************************************************************)
 (* Various well-formedness check for inductive declarations            *)
@@ -130,11 +131,11 @@ let is_unit constrsinfos =
 let infos_and_sort env t =
   let rec aux env t max =
     let t = whd_all env t in
-      match kind_of_term t with
+      match kind t with
       | Prod (name,c1,c2) ->
         let varj = infer_type env c1 in
 	let env1 = Environ.push_rel (LocalAssum (name,varj.utj_val)) env in
-	let max = Universe.sup max (univ_of_sort varj.utj_type) in
+	let max = Universe.sup max (Term.univ_of_sort varj.utj_type) in
 	  aux env1 c2 max
     | _ when is_constructor_head t -> max
     | _ -> (* don't fail if not positive, it is tested later *) max
@@ -168,7 +169,7 @@ let infer_constructor_packet env_ar_par params lc =
   let jlc = List.map (infer_type env_ar_par) lc in
   let jlc = Array.of_list jlc in
   (* generalize the constructor over the parameters *)
-  let lc'' = Array.map (fun j -> it_mkProd_or_LetIn j.utj_val params) jlc in
+  let lc'' = Array.map (fun j -> Term.it_mkProd_or_LetIn j.utj_val params) jlc in
   (* compute the max of the sorts of the products of the constructors types *)
   let levels = List.map (infos_and_sort env_ar_par) lc in
   let isunit = is_unit levels in
@@ -183,7 +184,7 @@ let cumulate_arity_large_levels env sign =
      match d with
      | LocalAssum (_,t) ->
 	let tj = infer_type env t in
-	let u = univ_of_sort tj.utj_type in
+	let u = Term.univ_of_sort tj.utj_type in
 	  (Universe.sup u lev, push_rel d env)
      | LocalDef _ ->
 	lev, push_rel d env)
@@ -199,8 +200,8 @@ let is_impredicative env u =
 let param_ccls paramsctxt =
   let fold acc = function
     | (LocalAssum (_, p)) ->
-      (let c = strip_prod_assum p in
-      match kind_of_term c with
+      (let c = Term.strip_prod_assum p in
+      match kind c with
         | Sort (Type u) -> Univ.Universe.level u
         | _ -> None) :: acc
     | LocalDef _ -> acc
@@ -208,7 +209,7 @@ let param_ccls paramsctxt =
   List.fold_left fold [] paramsctxt
 
 (* Check arities and constructors *)
-let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Term.types) numparams is_arity =
+let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : types) numparams is_arity =
   let numchecked = ref 0 in
   let basic_check ev tp =
     if !numchecked < numparams then () else conv_leq ev tp (subst tp);
@@ -288,7 +289,7 @@ let typecheck_inductive env mie =
 	         (** We have an algebraic universe as the conclusion of the arity,
 		     typecheck the dummy Π ctx, Prop and do a special case for the conclusion.
 		 *)
-	         let proparity = infer_type env_params (mkArity (ctx, prop_sort)) in
+	         let proparity = infer_type env_params (mkArity (ctx, Sorts.prop)) in
 		 let (cctx, _) = destArity proparity.utj_val in
 		   (* Any universe is well-formed, we don't need to check [s] here *)
 		   mkArity (cctx, s)
@@ -468,7 +469,7 @@ let check_correct_par (env,n,ntypes,_) paramdecls ind_index args =
     | LocalDef _ :: paramdecls ->
       check param_index (paramdecl_index+1) paramdecls
     | _::paramdecls ->
-        match kind_of_term (whd_all env params.(param_index)) with
+        match kind (whd_all env params.(param_index)) with
 	  | Rel w when Int.equal w paramdecl_index ->
             check (param_index-1) (paramdecl_index+1) paramdecls
 	  | _ ->
@@ -495,7 +496,7 @@ if Int.equal nmr 0 then 0 else
 	| (_,[]) -> assert false (* |paramsctxt|>=nmr *)
 	| (lp, LocalDef _ :: paramsctxt) -> find k (index-1) (lp,paramsctxt)
 	| (p::lp,_::paramsctxt) ->
-       ( match kind_of_term (whd_all env p) with
+       ( match kind (whd_all env p) with
 	  | Rel w when Int.equal w index -> find (k+1) (index-1) (lp,paramsctxt)
           | _ -> k)
   in find 0 (n-1) (lpar,List.rev paramsctxt)
@@ -526,7 +527,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) =
 let rec ienv_decompose_prod (env,_,_,_ as ienv) n c =
   if Int.equal n 0 then (ienv,c) else
     let c' = whd_all env c in
-    match kind_of_term c' with
+    match kind c' with
 	Prod(na,a,b) ->
 	  let ienv' = ienv_push_var ienv (na,a,mk_norec) in
 	  ienv_decompose_prod ienv' (n-1) b
@@ -554,8 +555,8 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
       constructor [cn] has a type of the shape [… -> c … -> P], where,
       more generally, the arrows may be dependent). *)
   let rec check_pos (env, n, ntypes, ra_env as ienv) nmr c =
-    let x,largs = decompose_app (whd_all env c) in
-      match kind_of_term x with
+    let x,largs = Term.decompose_app (whd_all env c) in
+      match kind x with
 	| Prod (na,b,d) ->
 	    let () = assert (List.is_empty largs) in
             (** If one of the inductives of the mutually inductive
@@ -662,8 +663,8 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
       inductive type. *)
   and check_constructors ienv check_head nmr c =
     let rec check_constr_rec (env,n,ntypes,ra_env as ienv) nmr lrec c =
-      let x,largs = decompose_app (whd_all env c) in
-	match kind_of_term x with
+      let x,largs = Term.decompose_app (whd_all env c) in
+	match kind x with
 
           | Prod (na,b,d) ->
 	      let () = assert (List.is_empty largs) in
@@ -746,7 +747,7 @@ let allowed_sorts is_smashed s =
 	   as well. *)
       all_sorts
   else 
-    match family_of_sort s with
+    match Sorts.family s with
     (* Type: all elimination allowed: above and below *)
     | InType -> all_sorts
     (* Smashed Set is necessarily impredicative: forbids large elimination *)
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index f5d0ed3f2..9a9380adb 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Declarations
 open Environ
 open Entries
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index a39307368..cb03a4d6b 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -10,7 +10,7 @@ open CErrors
 open Util
 open Names
 open Univ
-open Term
+open Constr
 open Vars
 open Declarations
 open Declareops
@@ -29,21 +29,21 @@ let lookup_mind_specif env (kn,tyi) =
   (mib, mib.mind_packets.(tyi))
 
 let find_rectype env c =
-  let (t, l) = decompose_app (whd_all env c) in
-  match kind_of_term t with
+  let (t, l) = Term.decompose_app (whd_all env c) in
+  match kind t with
   | Ind ind -> (ind, l)
   | _ -> raise Not_found
 
 let find_inductive env c =
-  let (t, l) = decompose_app (whd_all env c) in
-  match kind_of_term t with
+  let (t, l) = Term.decompose_app (whd_all env c) in
+  match kind t with
     | Ind ind
         when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> Decl_kinds.CoFinite -> (ind, l)
     | _ -> raise Not_found
 
 let find_coinductive env c =
-  let (t, l) = decompose_app (whd_all env c) in
-  match kind_of_term t with
+  let (t, l) = Term.decompose_app (whd_all env c) in
+  match kind t with
     | Ind ind
         when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == Decl_kinds.CoFinite -> (ind, l)
     | _ -> raise Not_found
@@ -81,7 +81,7 @@ let instantiate_params full t u args sign =
   let (rem_args, subs, ty) =
     Context.Rel.fold_outside
       (fun decl (largs,subs,ty) ->
-        match (decl, largs, kind_of_term ty) with
+        match (decl, largs, kind ty) with
           | (LocalAssum _, a::args, Prod(_,_,t)) -> (args, a::subs, t)
           | (LocalDef (_,b,_), _, LetIn(_,_,_,t))    ->
 	     (largs, (substl subs (subst_instance_constr u b))::subs, t)
@@ -94,9 +94,9 @@ let instantiate_params full t u args sign =
   substl subs ty
 
 let full_inductive_instantiate mib u params sign =
-  let dummy = prop_sort in
-  let t = mkArity (Vars.subst_instance_context u sign,dummy) in
-    fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
+  let dummy = Sorts.prop in
+  let t = Term.mkArity (Vars.subst_instance_context u sign,dummy) in
+    fst (Term.destArity (instantiate_params true t u params mib.mind_params_ctxt))
 
 let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
   let inst_ind = constructor_instantiate mind u mib t in
@@ -128,7 +128,7 @@ where
 Remark: Set (predicative) is encoded as Type(0)
 *)
 
-let sort_as_univ = function
+let sort_as_univ = let open Sorts in function
 | Type u -> u
 | Prop Null -> Universe.type0m
 | Prop Pos -> Universe.type0
@@ -192,11 +192,11 @@ let instantiate_universes env ctx ar argsorts =
   let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
   let ty =
     (* Singleton type not containing types are interpretable in Prop *)
-    if is_type0m_univ level then prop_sort
+    if is_type0m_univ level then Sorts.prop
     (* Non singleton type not containing types are interpretable in Set *)
-    else if is_type0_univ level then set_sort
+    else if is_type0_univ level then Sorts.set
     (* This is a Type with constraints *)
-    else Type level
+    else Sorts.Type level
   in
     (ctx, ty)
 
@@ -211,9 +211,9 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
       (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
          the situation where a non-Prop singleton inductive becomes Prop
          when applied to Prop params *)
-      if not polyprop && not (is_type0m_univ ar.template_level) && is_prop_sort s
+      if not polyprop && not (is_type0m_univ ar.template_level) && Sorts.is_prop s
       then raise (SingletonInductiveBecomesProp mip.mind_typename);
-      mkArity (List.rev ctx,s)
+      Term.mkArity (List.rev ctx,s)
 
 let type_of_inductive env pind = 
   type_of_inductive_gen env pind [||]
@@ -233,7 +233,7 @@ let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args =
 
 (* The max of an array of universes *)
 
-let cumulate_constructor_univ u = function
+let cumulate_constructor_univ u = let open Sorts in function
   | Prop Null -> u
   | Prop Pos -> Universe.sup Universe.type0 u
   | Type u' -> Universe.sup u u'
@@ -276,8 +276,8 @@ let type_of_constructors (ind,u) (mib,mip) =
 
 let inductive_sort_family mip =
   match mip.mind_arity with
-  | RegularArity s -> family_of_sort s.mind_sort
-  | TemplateArity _ -> InType
+  | RegularArity s -> Sorts.family s.mind_sort
+  | TemplateArity _ -> Sorts.InType
 
 let mind_arity mip =
   mip.mind_arity_ctxt, inductive_sort_family mip
@@ -296,19 +296,20 @@ let is_primitive_record (mib,_) =
 
 let build_dependent_inductive ind (_,mip) params =
   let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
-  applist
+  Term.applist
     (mkIndU ind,
        List.map (lift mip.mind_nrealdecls) params
        @ Context.Rel.to_extended_list mkRel 0 realargs)
 
 (* This exception is local *)
-exception LocalArity of (sorts_family * sorts_family * arity_error) option
+exception LocalArity of (Sorts.family * Sorts.family * arity_error) option
 
 let check_allowed_sort ksort specif =
+  let open Sorts in
   let eq_ksort s = match ksort, s with
   | InProp, InProp | InSet, InSet | InType, InType -> true
   | _ -> false in
-  if not (List.exists eq_ksort (elim_sorts specif)) then
+  if not (CList.exists eq_ksort (elim_sorts specif)) then
     let s = inductive_sort_family (snd specif) in
     raise (LocalArity (Some(ksort,s,error_elim_explain ksort s)))
 
@@ -316,7 +317,7 @@ let is_correct_arity env c pj ind specif params =
   let arsign,_ = get_instantiated_arity ind specif params in
   let rec srec env pt ar =
     let pt' = whd_all env pt in
-    match kind_of_term pt', ar with
+    match kind pt', ar with
       | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
           let () =
             try conv env a1 a1'
@@ -325,8 +326,8 @@ let is_correct_arity env c pj ind specif params =
       (* The last Prod domain is the type of the scrutinee *)
       | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
 	 let env' = push_rel (LocalAssum (na1,a1)) env in
-	 let ksort = match kind_of_term (whd_all env' a2) with
-	 | Sort s -> family_of_sort s
+	 let ksort = match kind (whd_all env' a2) with
+	 | Sort s -> Sorts.family s
 	 | _ -> raise (LocalArity None) in
 	 let dep_ind = build_dependent_inductive ind specif params in
 	 let _ =
@@ -351,22 +352,22 @@ let is_correct_arity env c pj ind specif params =
 let build_branches_type (ind,u) (_,mip as specif) params p =
   let build_one_branch i cty =
     let typi = full_constructor_instantiate (ind,u,specif,params) cty in
-    let (cstrsign,ccl) = decompose_prod_assum typi in
+    let (cstrsign,ccl) = Term.decompose_prod_assum typi in
     let nargs = Context.Rel.length cstrsign in
-    let (_,allargs) = decompose_app ccl in
+    let (_,allargs) = Term.decompose_app ccl in
     let (lparams,vargs) = List.chop (inductive_params specif) allargs in
     let cargs =
       let cstr = ith_constructor_of_inductive ind (i+1) in
-      let dep_cstr = applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list mkRel 0 cstrsign)) in
+      let dep_cstr = Term.applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list mkRel 0 cstrsign)) in
       vargs @ [dep_cstr] in
-    let base = lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in
-    it_mkProd_or_LetIn base cstrsign in
+    let base = Term.lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in
+    Term.it_mkProd_or_LetIn base cstrsign in
   Array.mapi build_one_branch mip.mind_nf_lc
 
 (* [p] is the predicate, [c] is the match object, [realargs] is the
    list of real args of the inductive type *)
 let build_case_type env n p c realargs =
-  whd_betaiota env (lambda_appvect_assum (n+1) p (Array.of_list (realargs@[c])))
+  whd_betaiota env (Term.lambda_appvect_assum (n+1) p (Array.of_list (realargs@[c])))
 
 let type_case_branches env (pind,largs) pj c =
   let specif = lookup_mind_specif env (fst pind) in
@@ -565,8 +566,8 @@ let check_inductive_codomain env p =
   let env = push_rel_context absctx env in
   let arctx, s = dest_prod_assum env ar in
   let env = push_rel_context arctx env in
-  let i,l' = decompose_app (whd_all env s) in
-  isInd i
+  let i,l' = Term.decompose_app (whd_all env s) in
+  Term.isInd i
 
 (* The following functions are almost duplicated from indtypes.ml, except
 that they carry here a poorer environment (containing less information). *)
@@ -589,7 +590,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
 let rec ienv_decompose_prod (env,_ as ienv) n c =
  if Int.equal n 0 then (ienv,c) else
    let c' = whd_all env c in
-   match kind_of_term c' with
+   match kind c' with
    Prod(na,a,b) ->
      let ienv' = ienv_push_var ienv (na,a,mk_norec) in
      ienv_decompose_prod ienv' (n-1) b
@@ -620,8 +621,8 @@ close to check_positive in indtypes.ml, but does no positivity check and does no
 compute the number of recursive arguments. *)
 let get_recargs_approx env tree ind args =
   let rec build_recargs (env, ra_env as ienv) tree c =
-    let x,largs = decompose_app (whd_all env c) in
-    match kind_of_term x with
+    let x,largs = Term.decompose_app (whd_all env c) in
+    match kind x with
     | Prod (na,b,d) ->
        assert (List.is_empty largs);
        build_recargs (ienv_push_var ienv (na, b, mk_norec)) tree d
@@ -679,8 +680,8 @@ let get_recargs_approx env tree ind args =
 
   and build_recargs_constructors ienv trees c =
     let rec recargs_constr_rec (env,ra_env as ienv) trees lrec c =
-      let x,largs = decompose_app (whd_all env c) in
-	match kind_of_term x with
+      let x,largs = Term.decompose_app (whd_all env c) in
+	match kind x with
 
           | Prod (na,b,d) ->
 	     let () = assert (List.is_empty largs) in
@@ -708,8 +709,8 @@ let restrict_spec env spec p =
   let env = push_rel_context absctx env in
   let arctx, s = dest_prod_assum env ar in
   let env = push_rel_context arctx env in
-  let i,args = decompose_app (whd_all env s) in
-  match kind_of_term i with
+  let i,args = Term.decompose_app (whd_all env s) in
+  match kind i with
   | Ind i ->
      begin match spec with
 	   | Dead_code -> spec
@@ -729,8 +730,8 @@ let restrict_spec env spec p =
 
 let rec subterm_specif renv stack t =
   (* maybe reduction is not always necessary! *)
-  let f,l = decompose_app (whd_all renv.env t) in
-    match kind_of_term f with
+  let f,l = Term.decompose_app (whd_all renv.env t) in
+    match kind f with
     | Rel k -> subterm_var k renv
     | Case (ci,p,c,lbr) ->
        let stack' = push_stack_closures renv l stack in
@@ -773,7 +774,7 @@ let rec subterm_specif renv stack t =
 	let decrArg = recindxs.(i) in
 	let theBody = bodies.(i)   in
 	let nbOfAbst = decrArg+1 in
-	let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in
+	let sign,strippedBody = Term.decompose_lam_n_assum nbOfAbst theBody in
 		   (* pushing the fix parameters *)
 	let stack' = push_stack_closures renv l stack in
 	let renv'' = push_ctxt_renv renv' sign in
@@ -857,13 +858,13 @@ let filter_stack_domain env ci p stack =
   else let env = push_rel_context absctx env in
   let rec filter_stack env ar stack =
     let t = whd_all env ar in
-    match stack, kind_of_term t with
+    match stack, kind t with
     | elt :: stack', Prod (n,a,c0) ->
       let d = LocalAssum (n,a) in
       let ctx, a = dest_prod_assum env a in
       let env = push_rel_context ctx env in
-      let ty, args = decompose_app (whd_all env a) in
-      let elt = match kind_of_term ty with
+      let ty, args = Term.decompose_app (whd_all env a) in
+      let elt = match kind ty with
       | Ind ind -> 
         let spec' = stack_element_specif elt in
         (match (Lazy.force spec') with
@@ -893,8 +894,8 @@ let check_one_fix renv recpos trees def =
     (* if [t] does not make recursive calls, it is guarded: *)
     if noccur_with_meta renv.rel_min nfi t then ()
     else
-      let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in
-      match kind_of_term f with
+      let (f,l) = Term.decompose_app (whd_betaiotazeta renv.env t) in
+      match kind f with
         | Rel p ->
             (* Test if [p] is a fixpoint (recursive call) *)
 	    if renv.rel_min <= p && p < renv.rel_min+nfi then
@@ -924,7 +925,7 @@ let check_one_fix renv recpos trees def =
                 | LocalDef (_,c,_) ->
                     try List.iter (check_rec_call renv []) l
                     with FixGuardError _ ->
-                      check_rec_call renv stack (applist(lift p c,l))
+                      check_rec_call renv stack (Term.applist(lift p c,l))
               end
 		
         | Case (ci,p,c_0,lrest) ->
@@ -970,7 +971,7 @@ let check_one_fix renv recpos trees def =
             if evaluable_constant kn renv.env then
               try List.iter (check_rec_call renv []) l
               with (FixGuardError _ ) ->
-		let value = (applist(constant_value_in renv.env cu, l)) in
+		let value = (Term.applist(constant_value_in renv.env cu, l)) in
 	        check_rec_call renv stack value
 	    else List.iter (check_rec_call renv []) l
 
@@ -1007,7 +1008,7 @@ let check_one_fix renv recpos trees def =
               | LocalDef (_,c,_) ->
                   try List.iter (check_rec_call renv []) l
                   with (FixGuardError _) -> 
-		    check_rec_call renv stack (applist(c,l))
+		    check_rec_call renv stack (Term.applist(c,l))
             end
 
 	| Sort _ ->
@@ -1022,7 +1023,7 @@ let check_one_fix renv recpos trees def =
     if Int.equal decr 0 then
       check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body
     else
-      match kind_of_term body with
+      match kind body with
 	| Lambda (x,a,b) ->
 	    check_rec_call renv [] a;
             let renv' = push_var_renv renv (x,a) in
@@ -1053,7 +1054,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
     (* check fi does not appear in the k+1 first abstractions,
        gives the type of the k+1-eme abstraction (must be an inductive)  *)
     let rec check_occur env n def =
-      match kind_of_term (whd_all env def) with
+      match kind (whd_all env def) with
         | Lambda (x,a,b) ->
 	    if noccur_with_meta n nbfix a then
 	      let env' = push_rel (LocalAssum (x,a)) env in
@@ -1108,7 +1109,7 @@ let anomaly_ill_typed () =
 
 let rec codomain_is_coind env c =
   let b = whd_all env c in
-  match kind_of_term b with
+  match kind b with
     | Prod (x,a,b) ->
 	codomain_is_coind (push_rel (LocalAssum (x,a)) env) b
     | _ ->
@@ -1119,8 +1120,8 @@ let rec codomain_is_coind env c =
 let check_one_cofix env nbfix def deftype =
   let rec check_rec_call env alreadygrd n tree vlra  t =
     if not (noccur_with_meta n nbfix t) then
-      let c,args = decompose_app (whd_all env t) in
-      match kind_of_term c with
+      let c,args = Term.decompose_app (whd_all env t) in
+      match kind c with
 	| Rel p when  n <= p && p < n+nbfix ->
 	    (* recursive call: must be guarded and no nested recursive
                call allowed *)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 1caede857..601422a10 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -7,8 +7,8 @@
 (************************************************************************)
 
 open Names
-open Term
 open Univ
+open Constr
 open Declarations
 open Environ
 
@@ -32,23 +32,23 @@ type mind_specif = mutual_inductive_body * one_inductive_body
 val lookup_mind_specif : env -> inductive -> mind_specif
 
 (** {6 Functions to build standard types related to inductive } *)
-val ind_subst : MutInd.t -> mutual_inductive_body -> universe_instance -> constr list
+val ind_subst : MutInd.t -> mutual_inductive_body -> Instance.t -> constr list
 
 val inductive_paramdecls : mutual_inductive_body puniverses -> Context.Rel.t
 
-val instantiate_inductive_constraints : 
-  mutual_inductive_body -> universe_instance -> constraints
+val instantiate_inductive_constraints :
+  mutual_inductive_body -> Instance.t -> constraints
 
 val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained
-val constrained_type_of_inductive_knowing_parameters : 
+val constrained_type_of_inductive_knowing_parameters :
   env -> mind_specif puniverses -> types Lazy.t array -> types constrained
 
 val type_of_inductive : env -> mind_specif puniverses -> types
 
-val type_of_inductive_knowing_parameters : 
+val type_of_inductive_knowing_parameters :
   env -> ?polyprop:bool -> mind_specif puniverses -> types Lazy.t array -> types
 
-val elim_sorts : mind_specif -> sorts_family list
+val elim_sorts : mind_specif -> Sorts.family list
 
 val is_private : mind_specif -> bool
 val is_primitive_record : mind_specif -> bool
@@ -85,9 +85,9 @@ val build_branches_type :
     constr list -> constr -> types array
 
 (** Return the arity of an inductive type *)
-val mind_arity : one_inductive_body -> Context.Rel.t * sorts_family
+val mind_arity : one_inductive_body -> Context.Rel.t * Sorts.family
 
-val inductive_sort_family : one_inductive_body -> sorts_family
+val inductive_sort_family : one_inductive_body -> Sorts.family
 
 (** Check a [case_info] actually correspond to a Case expression on the
    given inductive type. *)
@@ -111,10 +111,10 @@ val check_cofix : env -> cofixpoint -> unit
 
 exception SingletonInductiveBecomesProp of Id.t
 
-val max_inductive_sort : sorts array -> universe
+val max_inductive_sort : Sorts.t array -> Universe.t
 
 val instantiate_universes : env -> Context.Rel.t ->
-  template_arity -> constr Lazy.t array -> Context.Rel.t * sorts
+  template_arity -> constr Lazy.t array -> Context.Rel.t * Sorts.t
 
 (** {6 Debug} *)
 
@@ -135,6 +135,6 @@ type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t
 
 val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec
 
-val lambda_implicit_lift : int -> Constr.constr -> Term.constr
+val lambda_implicit_lift : int -> constr -> constr
 
-val abstract_mind_lc : int -> Int.t -> Constr.constr array -> Constr.constr array
+val abstract_mind_lc : int -> Int.t -> constr array -> constr array
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 1793e4f71..2c8ef477f 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -16,7 +16,7 @@
 open Pp
 open Util
 open Names
-open Term
+open Constr
 
 (* For Inline, the int is an inlining level, and the constr (if present)
    is the term into which we should inline. *)
@@ -340,7 +340,7 @@ let subst_evaluable_reference subst = function
 
 let rec map_kn f f' c =
   let func = map_kn f f' in
-    match kind_of_term c with
+    match kind c with
       | Const kn -> (try snd (f' kn) with No_subst -> c)
       | Proj (p,t) -> 
           let p' = 
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 1d7012ce5..1aa7ba519 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -9,7 +9,7 @@
 (** {6 [Mod_subst] } *)
 
 open Names
-open Term
+open Constr
 
 (** {6 Delta resolver} *)
 
@@ -171,6 +171,5 @@ val occur_mbid : MBId.t -> substitution -> bool
 
 val repr_substituted : 'a substituted -> substitution list option * 'a
 
-val force_constr : Term.constr substituted -> Term.constr
-val subst_constr :
-  substitution -> Term.constr substituted -> Term.constr substituted
+val force_constr : constr substituted -> constr
+val subst_constr : substitution -> constr substituted -> constr substituted
diff --git a/kernel/modops.ml b/kernel/modops.ml
index c10af0725..b1df1a187 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -17,7 +17,7 @@
 
 open Util
 open Names
-open Term
+open Constr
 open Declarations
 open Declareops
 open Environ
@@ -266,7 +266,7 @@ let subst_structure subst = subst_structure subst do_delta_codom
 (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *)
 let add_retroknowledge mp =
   let perform rkaction env = match rkaction with
-    |Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) ->
+    |Retroknowledge.RKRegister (f, e) when (Term.isConst e || Term.isInd e) ->
       Environ.register env f e
     |_ ->
       CErrors.anomaly ~label:"Modops.add_retroknowledge"
diff --git a/kernel/modops.mli b/kernel/modops.mli
index e1bba21d3..bbb4c918c 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Environ
 open Declarations
 open Entries
diff --git a/kernel/names.mli b/kernel/names.mli
index 531a0cccb..ba0637c8a 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -300,7 +300,6 @@ module KNset  : CSig.SetS with type elt = KerName.t
 module KNpred : Predicate.S with type elt = KerName.t
 module KNmap  : Map.ExtS with type key = KerName.t and module Set := KNset
 
-
 (** {6 Constant Names } *)
 
 module Constant:
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index bb4c2585d..c558e9ed0 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -8,7 +8,7 @@
 
 open CErrors
 open Names
-open Term
+open Constr
 open Declarations
 open Util
 open Nativevalues
@@ -142,7 +142,7 @@ let fresh_gnormtbl l =
 
 type symbol =
   | SymbValue of Nativevalues.t
-  | SymbSort of sorts
+  | SymbSort of Sorts.t
   | SymbName of Name.t
   | SymbConst of Constant.t
   | SymbMatch of annot_sw
@@ -163,7 +163,7 @@ let eq_symbol sy1 sy2 =
   | SymbInd ind1, SymbInd ind2 -> eq_ind ind1 ind2
   | SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2
   | SymbEvar (evk1,args1), SymbEvar (evk2,args2) ->
-     Evar.equal evk1 evk2 && Array.for_all2 eq_constr args1 args2
+     Evar.equal evk1 evk2 && Array.for_all2 Constr.equal args1 args2
   | SymbLevel l1, SymbLevel l2 -> Univ.Level.equal l1 l2
   | _, _ -> false
 
@@ -2016,7 +2016,7 @@ let compile_mind_deps env prefix ~interactive
 (* This function compiles all necessary dependencies of t, and generates code in
    reverse order, as well as linking information updates *)
 let rec compile_deps env sigma prefix ~interactive init t =
-  match kind_of_term t with
+  match kind t with
   | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind
   | Const c ->
       let c,u = get_alias env c in
@@ -2048,8 +2048,8 @@ let rec compile_deps env sigma prefix ~interactive init t =
   | Case (ci, p, c, ac) ->
       let mind = fst ci.ci_ind in
       let init = compile_mind_deps env prefix ~interactive init mind in
-      fold_constr (compile_deps env sigma prefix ~interactive) init t
-  | _ -> fold_constr (compile_deps env sigma prefix ~interactive) init t
+      Constr.fold (compile_deps env sigma prefix ~interactive) init t
+  | _ -> Constr.fold (compile_deps env sigma prefix ~interactive) init t
 
 let compile_constant_field env prefix con acc cb =
     let (gl, _) =
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 764598097..d08f49095 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -5,8 +5,8 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-open Term
 open Names
+open Constr
 open Declarations
 open Pre_env
 open Nativelambda
@@ -32,7 +32,7 @@ val clear_symbols : unit -> unit
 
 val get_value : symbols -> int -> Nativevalues.t
 
-val get_sort : symbols -> int -> sorts
+val get_sort : symbols -> int -> Sorts.t
 
 val get_name : symbols -> int -> Name.t
 
diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli
index fbbcce744..769deacae 100644
--- a/kernel/nativeconv.mli
+++ b/kernel/nativeconv.mli
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-open Term
+open Constr
 open Reduction
 open Nativelambda
 
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli
index b2c8662da..928283a4d 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 open Names
-open Term
+open Constr
 open Nativevalues
 
 (** This file defines the lambda code for the native compiler. It has been
@@ -43,7 +43,7 @@ and lambda =
 	(* A partially applied constructor *)
   | Luint         of uint
   | Lval          of Nativevalues.t
-  | Lsort         of sorts
+  | Lsort         of Sorts.t
   | Lind          of prefix * pinductive
   | Llazy
   | Lforce
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index aaa9f9b00..de4dc2107 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -8,7 +8,7 @@
 open Util
 open Names
 open Esubst
-open Term
+open Constr
 open Declarations
 open Pre_env
 open Nativevalues
@@ -417,9 +417,9 @@ module Renv =
 
 (* What about pattern matching ?*)
 let is_lazy prefix t =
-  match kind_of_term t with
+  match kind t with
   | App (f,args) ->
-     begin match kind_of_term f with
+     begin match kind f with
      | Construct (c,_) ->
 	let entry = mkInd (fst c) in
 	(try
@@ -448,7 +448,7 @@ let empty_evars =
 let empty_ids = [||]
 
 let rec lambda_of_constr env sigma c =
-  match kind_of_term c with
+  match kind c with
   | Meta mv ->
      let ty = meta_type sigma mv in
      Lmeta (mv, lambda_of_constr env sigma ty)
@@ -480,7 +480,7 @@ let rec lambda_of_constr env sigma c =
       Lprod(ld,  Llam([|id|], lc))
 
   | Lambda _ ->
-      let params, body = decompose_lam c in
+      let params, body = Term.decompose_lam c in
       let ids = get_names (List.rev params) in
       Renv.push_rels env ids;
       let lb = lambda_of_constr env sigma body in
@@ -561,7 +561,7 @@ let rec lambda_of_constr env sigma c =
       Lcofix(init, (names, ltypes, lbodies))
 
 and lambda_of_app env sigma f args =
-  match kind_of_term f with
+  match kind f with
   | Const (kn,u as c) ->
       let kn,u = get_alias !global_env c in
       let cb = lookup_constant kn !global_env in
@@ -656,7 +656,7 @@ let compile_static_int31 fc args =
   if not fc then raise Not_found else
     Luint (UintVal
     (Uint31.of_int (Array.fold_left
-       (fun temp_i -> fun t -> match kind_of_term t with
+       (fun temp_i -> fun t -> match kind t with
           | Construct ((_,d),_) -> 2*temp_i+d-1
           | _ -> raise NotClosed)
        0 args)))
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index 392961f5d..933fbc660 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 open Names
-open Term
+open Constr
 open Pre_env
 open Nativeinstr
 
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 2f8920088..ae66362ca 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -5,10 +5,11 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-open Term
-open Names
-open CErrors
+
 open Util
+open CErrors
+open Names
+open Constr
 
 (** This module defines the representation of values internally used by
 the native compiler *)
@@ -51,7 +52,7 @@ type atom =
   | Arel of int
   | Aconstant of pconstant
   | Aind of pinductive
-  | Asort of sorts
+  | Asort of Sorts.t
   | Avar of Id.t
   | Acase of annot_sw * accumulator * t * (t -> t)
   | Afix of t array * t array * rec_pos * int
@@ -111,6 +112,7 @@ let mk_ind_accu ind u =
   mk_accu (Aind (ind,Univ.Instance.of_array u))
 
 let mk_sort_accu s u =
+  let open Sorts in
   match s with
   | Prop _ -> mk_accu (Asort s)
   | Type s ->
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 1368b4470..18b877745 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-open Term
+open Constr
 open Names
 
 (** This modules defines the representation of values internally used by
@@ -43,7 +43,7 @@ type atom =
   | Arel of int
   | Aconstant of pconstant
   | Aind of pinductive
-  | Asort of sorts
+  | Asort of Sorts.t
   | Avar of Id.t
   | Acase of annot_sw * accumulator * t * (t -> t) 
   | Afix of t array * t array * rec_pos * int 
@@ -61,7 +61,7 @@ val mk_rel_accu : int -> t
 val mk_rels_accu : int -> int -> t array
 val mk_constant_accu : Constant.t -> Univ.Level.t array -> t
 val mk_ind_accu : inductive -> Univ.Level.t array -> t
-val mk_sort_accu : sorts -> Univ.Level.t array -> t
+val mk_sort_accu : Sorts.t -> Univ.Level.t array -> t
 val mk_var_accu : Id.t -> t
 val mk_sw_accu : annot_sw -> accumulator -> t -> (t -> t)
 val mk_prod_accu : Name.t -> t -> t -> t
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 400f9feee..45a62d55a 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -8,7 +8,7 @@
 
 open Names
 open Univ
-open Term
+open Constr
 open Mod_subst
 
 type work_list = (Instance.t * Id.t array) Cmap.t * 
@@ -17,7 +17,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t *
 type cooking_info = { 
   modlist : work_list; 
   abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t } 
-type proofterm = (constr * Univ.universe_context_set) Future.computation
+type proofterm = (constr * Univ.ContextSet.t) Future.computation
 type opaque =
   | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
   | Direct of cooking_info list * proofterm
@@ -138,7 +138,7 @@ let get_proof { opaque_val = prfs; opaque_dir = odp } = function
  
 module FMap = Future.UUIDMap
 
-let a_constr = Future.from_val (Term.mkRel 1)
+let a_constr = Future.from_val (mkRel 1)
 let a_univ = Future.from_val Univ.ContextSet.empty
 let a_discharge : cooking_info list = []
 
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index a0418a022..20d76ce23 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Mod_subst
 
 (** This module implements the handling of opaque proof terms.
@@ -19,7 +19,7 @@ open Mod_subst
     When it is [turn_indirect] the data is relocated to an opaque table
     and the [opaque] is turned into an index. *)
 
-type proofterm = (constr * Univ.universe_context_set) Future.computation
+type proofterm = (constr * Univ.ContextSet.t) Future.computation
 type opaquetab
 type opaque
 
@@ -36,10 +36,10 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
 (** From a [opaque] back to a [constr]. This might use the
     indirect opaque accessor configured below. *)
 val force_proof : opaquetab -> opaque -> constr
-val force_constraints : opaquetab -> opaque -> Univ.universe_context_set
-val get_proof : opaquetab -> opaque -> Term.constr Future.computation
+val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
+val get_proof : opaquetab -> opaque -> constr Future.computation
 val get_constraints :
-  opaquetab -> opaque -> Univ.universe_context_set Future.computation option
+  opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
 
 val subst_opaque : substitution -> opaque -> opaque
 val iter_direct_opaque : (constr -> unit) -> opaque -> opaque
@@ -63,7 +63,7 @@ val join_opaque : opaquetab -> opaque -> unit
 
 val dump : opaquetab ->
   Constr.t Future.computation array *
-  Univ.universe_context_set Future.computation array *
+  Univ.ContextSet.t Future.computation array *
   cooking_info list array *
   int Future.UUIDMap.t
 
@@ -75,7 +75,7 @@ val dump : opaquetab ->
 *)
 
 val set_indirect_opaque_accessor :
-  (DirPath.t -> int -> Term.constr Future.computation) -> unit
+  (DirPath.t -> int -> constr Future.computation) -> unit
 val set_indirect_univ_accessor :
-  (DirPath.t -> int -> Univ.universe_context_set Future.computation option) -> unit
+  (DirPath.t -> int -> Univ.ContextSet.t Future.computation option) -> unit
 
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 94738d618..c5254b453 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -15,7 +15,7 @@
 
 open Util
 open Names
-open Term
+open Constr
 open Declarations
 
 module NamedDecl = Context.Named.Declaration
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 27f9511e1..054ae1743 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Declarations
 
 (** The type of environments. *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 79a35d292..b0510dc7c 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -18,7 +18,7 @@
 open CErrors
 open Util
 open Names
-open Term
+open Constr
 open Vars
 open Environ
 open CClosure
@@ -107,11 +107,11 @@ let pure_stack lfts stk =
 (****************************************************************************)
 
 let whd_betaiota env t =
-  match kind_of_term t with
+  match kind t with
     | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
        Prod _|Lambda _|Fix _|CoFix _) -> t
     | App (c, _) ->
-      begin match kind_of_term c with
+      begin match kind c with
       | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | LetIn _ -> t
       | _ -> whd_val (create_clos_infos betaiota env) (inject t)
       end
@@ -121,33 +121,33 @@ let nf_betaiota env t =
   norm_val (create_clos_infos betaiota env) (inject t)
 
 let whd_betaiotazeta env x =
-  match kind_of_term x with
+  match kind x with
     | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
        Prod _|Lambda _|Fix _|CoFix _) -> x
     | App (c, _) ->
-      begin match kind_of_term c with
+      begin match kind c with
       | Ind _ | Construct _ | Evar _ | Meta _ | Const _ -> x
       | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x)
       end
     | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x)
 
 let whd_all env t =
-  match kind_of_term t with
+  match kind t with
     | (Sort _|Meta _|Evar _|Ind _|Construct _|
        Prod _|Lambda _|Fix _|CoFix _) -> t
     | App (c, _) ->
-      begin match kind_of_term c with
+      begin match kind c with
       | Ind _ | Construct _ | Evar _ | Meta _ -> t
       | _ -> whd_val (create_clos_infos all env) (inject t)
       end
     | _ -> whd_val (create_clos_infos all env) (inject t)
 
 let whd_allnolet env t =
-  match kind_of_term t with
+  match kind t with
     | (Sort _|Meta _|Evar _|Ind _|Construct _|
        Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t
     | App (c, _) ->
-      begin match kind_of_term c with
+      begin match kind c with
       | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ -> t
       | _ -> whd_val (create_clos_infos allnolet env) (inject t)
       end
@@ -189,7 +189,7 @@ let is_cumul = function CUMUL -> true | CONV -> false
 
 type 'a universe_compare = 
   { (* Might raise NotConvertible *)
-    compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
+    compare : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
     compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
     conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int ->
       Univ.Instance.t -> int -> 'a -> 'a;
@@ -331,7 +331,7 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
   match (fterm_of hd1, fterm_of hd2) with
     (* case of leaves *)
     | (FAtom a1, FAtom a2) ->
-	(match kind_of_term a1, kind_of_term a2 with
+	(match kind a1, kind a2 with
 	   | (Sort s1, Sort s2) ->
 	       if not (is_empty_stack v1 && is_empty_stack v2) then
 		 anomaly (Pp.str "conversion was given ill-typed terms (Sort).");
@@ -615,6 +615,7 @@ let check_leq univs u u' =
   if not (UGraph.check_leq univs u u') then raise NotConvertible
 
 let check_sort_cmp_universes env pb s0 s1 univs =
+  let open Sorts in
   match (s0,s1) with
     | (Prop c1, Prop c2) when is_cumul pb ->
       begin match c1, c2 with
@@ -734,6 +735,7 @@ let infer_leq (univs, cstrs as cuniv) u u' =
       univs, cstrs'
 
 let infer_cmp_universes env pb s0 s1 univs =
+  let open Sorts in
   match (s0,s1) with
     | (Prop c1, Prop c2) when is_cumul pb ->
       begin match c1, c2 with
@@ -869,7 +871,7 @@ let warn_bytecode_compiler_failed =
          (fun () -> strbrk "Bytecode compiler failed, " ++
                       strbrk "falling back to standard conversion")
 
-let set_vm_conv (f:conv_pb -> Term.types kernel_conversion_function) = vm_conv := f
+let set_vm_conv (f:conv_pb -> types kernel_conversion_function) = vm_conv := f
 let vm_conv cv_pb env t1 t2 =
   try
     !vm_conv cv_pb env t1 t2
@@ -895,9 +897,9 @@ let conv env t1 t2 =
 
 let beta_applist c l =
   let rec app subst c l =
-    match kind_of_term c, l with
+    match kind c, l with
     | Lambda(_,_,c), arg::l -> app (arg::subst) c l
-    | _ -> applist (substl subst c, l) in
+    | _ -> Term.applist (substl subst c, l) in
   app [] c l
 
 let beta_appvect c v = beta_applist c (Array.to_list v)
@@ -905,7 +907,7 @@ let beta_appvect c v = beta_applist c (Array.to_list v)
 let beta_app c a = beta_applist c [a]
 
 (* Compatibility *)
-let betazeta_appvect = lambda_appvect_assum
+let betazeta_appvect = Term.lambda_appvect_assum
 
 (********************************************************************)
 (*             Special-Purpose Reduction                            *)
@@ -918,7 +920,7 @@ let betazeta_appvect = lambda_appvect_assum
  * error message. *)
 
 let hnf_prod_app env t n =
-  match kind_of_term (whd_all env t) with
+  match kind (whd_all env t) with
     | Prod (_,_,b) -> subst1 n b
     | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.")
 
@@ -930,7 +932,7 @@ let hnf_prod_applist env t nl =
 let dest_prod env =
   let rec decrec env m c =
     let t = whd_all env c in
-    match kind_of_term t with
+    match kind t with
       | Prod (n,a,c0) ->
 	  let d = LocalAssum (n,a) in
 	  decrec (push_rel d env) (Context.Rel.add d m) c0
@@ -942,7 +944,7 @@ let dest_prod env =
 let dest_prod_assum env =
   let rec prodec_rec env l ty =
     let rty = whd_allnolet env ty in
-    match kind_of_term rty with
+    match kind rty with
     | Prod (x,t,c)  ->
         let d = LocalAssum (x,t) in
 	prodec_rec (push_rel d env) (Context.Rel.add d l) c
@@ -952,7 +954,7 @@ let dest_prod_assum env =
     | Cast (c,_,_)    -> prodec_rec env l c
     | _               ->
       let rty' = whd_all env rty in
-	if Term.eq_constr rty' rty then l, rty
+	if Constr.equal rty' rty then l, rty
 	else prodec_rec env l rty'
   in
   prodec_rec env Context.Rel.empty
@@ -960,7 +962,7 @@ let dest_prod_assum env =
 let dest_lam_assum env =
   let rec lamec_rec env l ty =
     let rty = whd_allnolet env ty in
-    match kind_of_term rty with
+    match kind rty with
     | Lambda (x,t,c)  ->
         let d = LocalAssum (x,t) in
 	lamec_rec (push_rel d env) (Context.Rel.add d l) c
@@ -976,7 +978,7 @@ exception NotArity
 
 let dest_arity env c =
   let l, c = dest_prod_assum env c in
-  match kind_of_term c with
+  match kind c with
     | Sort s -> l,s
     | _ -> raise NotArity
 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 253c0874f..05a906e28 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
+open Constr
 open Environ
 
 (***********************************************************************
@@ -37,7 +37,7 @@ type conv_pb = CONV | CUMUL
 
 type 'a universe_compare = 
   { (* Might raise NotConvertible *)
-    compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
+    compare : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
     compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
     conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int ->
       Univ.Instance.t -> int -> 'a -> 'a;
@@ -51,7 +51,7 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a
 
 type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints
 
-val sort_cmp_universes : env -> conv_pb -> sorts -> sorts ->
+val sort_cmp_universes : env -> conv_pb -> Sorts.t -> Sorts.t ->
   'a * 'a universe_compare -> 'a * 'a universe_compare
 
 (* [flex] should be true for constants, false for inductive types and
@@ -115,7 +115,7 @@ val dest_lam_assum  : env -> types -> Context.Rel.t * types
 
 exception NotArity
 
-val dest_arity : env -> types -> arity (* raises NotArity if not an arity *)
+val dest_arity : env -> types -> Term.arity (* raises NotArity if not an arity *)
 val is_arity   : env -> types -> bool
 
 val warn_bytecode_compiler_failed : ?loc:Loc.t -> unit -> unit
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 5fbd914f3..88cf93acc 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -14,7 +14,7 @@
    for evaluation in the bytecode virtual machine *)
 
 open Names
-open Term
+open Constr
 
 (* The retroknowledge defines a bijective correspondance between some
    [entry]-s (which are, in fact, merely terms) and [field]-s which
@@ -102,7 +102,7 @@ module Reactive = Map.Make (EntryOrd)
 type reactive_info = {(*information required by the compiler of the VM *)
   vm_compiling :
       (*fastcomputation flag -> continuation -> result *)
-      (bool->Cbytecodes.comp_env->constr array ->
+      (bool -> Cbytecodes.comp_env -> constr array ->
        int->Cbytecodes.bytecodes->Cbytecodes.bytecodes)
       option;
   vm_constant_static :
@@ -117,7 +117,7 @@ type reactive_info = {(*information required by the compiler of the VM *)
   (* fastcomputation flag -> cont -> result *)
   vm_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option;
   (* tag (= compiled int for instance) -> result *)
-  vm_decompile_const : (int -> Term.constr) option;
+  vm_decompile_const : (int -> constr) option;
 
   native_compiling :
       (bool -> Nativeinstr.prefix -> Nativeinstr.lambda array ->
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 18a12a4ef..e4d78ba14 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 
 type retroknowledge
 
@@ -117,7 +117,7 @@ val get_vm_before_match_info : retroknowledge -> entry -> Cbytecodes.bytecodes
    recover the elements of that type from their compiled form if it's non
    standard (it is used (and can be used) only when the compiled form
    is not a block *)
-val get_vm_decompile_constant_info : retroknowledge -> entry -> int -> Term.constr
+val get_vm_decompile_constant_info : retroknowledge -> entry -> int -> constr
 
 
 val get_native_compiling_info  : retroknowledge -> entry -> Nativeinstr.prefix ->
@@ -163,7 +163,7 @@ type reactive_info = {(*information required by the compiler of the VM *)
   (* fastcomputation flag -> cont -> result *)
   vm_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option;
   (* tag (= compiled int for instance) -> result *)
-  vm_decompile_const : (int -> Term.constr) option;
+  vm_decompile_const : (int -> constr) option;
 
   native_compiling :
       (bool -> Nativeinstr.prefix -> Nativeinstr.lambda array ->
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index ee9632944..0bfe07486 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -69,7 +69,7 @@ val inline_private_constants_in_constr :
 val inline_private_constants_in_definition_entry :
   Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry
 
-val universes_of_private : private_constants -> Univ.universe_context_set list
+val universes_of_private : private_constants -> Univ.ContextSet.t list
 
 val is_curmod_library : safe_environment -> bool
 
@@ -84,13 +84,13 @@ val is_joined_environment : safe_environment -> bool
 (** Insertion of local declarations (Local or Variables) *)
 
 val push_named_assum :
-  (Id.t * Term.types * bool (* polymorphic *))
+  (Id.t * Constr.types * bool (* polymorphic *))
     Univ.in_universe_context_set -> safe_transformer0
 
 (** Returns the full universe context necessary to typecheck the definition
   (futures are forced) *)
 val push_named_def :
-  Id.t * private_constants Entries.definition_entry -> Univ.universe_context_set safe_transformer
+  Id.t * private_constants Entries.definition_entry -> Univ.ContextSet.t safe_transformer
 
 (** Insertion of global axioms or definitions *)
 
@@ -133,10 +133,10 @@ val add_modtype :
 (** Adding universe constraints *)
 
 val push_context_set :
-  bool -> Univ.universe_context_set -> safe_transformer0
+  bool -> Univ.ContextSet.t -> safe_transformer0
 
 val push_context :
-  bool -> Univ.universe_context -> safe_transformer0
+  bool -> Univ.UContext.t -> safe_transformer0
 
 val add_constraints :
   Univ.constraints -> safe_transformer0
@@ -194,18 +194,18 @@ val export :
     ModPath.t * compiled_library * native_library
 
 (* Constraints are non empty iff the file is a vi2vo *)
-val import : compiled_library -> Univ.universe_context_set -> vodigest ->
+val import : compiled_library -> Univ.ContextSet.t -> vodigest ->
   ModPath.t safe_transformer
 
 (** {6 Safe typing judgments } *)
 
 type judgment
 
-val j_val : judgment -> Term.constr
-val j_type : judgment -> Term.constr
+val j_val : judgment -> Constr.constr
+val j_type : judgment -> Constr.constr
 
 (** The safe typing of a term returns a typing judgment. *)
-val typing : safe_environment -> Term.constr -> judgment
+val typing : safe_environment -> Constr.constr -> judgment
 
 (** {6 Queries } *)
 
@@ -221,7 +221,7 @@ open Retroknowledge
 val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a
 
 val register :
-  field -> Retroknowledge.entry -> Term.constr -> safe_transformer0
+  field -> Retroknowledge.entry -> Constr.constr -> safe_transformer0
 
 val register_inline : Constant.t -> safe_transformer0
 
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index cf5207e8d..07688840d 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -14,7 +14,7 @@ type family = InProp | InSet | InType
 
 type t =
   | Prop of contents                      (* proposition types *)
-  | Type of universe
+  | Type of Universe.t
 
 let prop = Prop Null
 let set = Prop Pos
@@ -91,7 +91,7 @@ module Hsorts =
     struct
       type _t = t
       type t = _t
-      type u = universe -> universe
+      type u = Universe.t -> Universe.t
 
       let hashcons huniv = function
         | Type u as c -> 
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index 3426d6fd3..65ea75138 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -14,7 +14,7 @@ type family = InProp | InSet | InType
 
 type t =
 | Prop of contents       (** Prop and Set *)
-| Type of Univ.universe  (** Type *)
+| Type of Univ.Universe.t  (** Type *)
 
 val set  : t
 val prop : t
@@ -38,5 +38,5 @@ module List : sig
   val intersect : family list -> family list -> family list
 end
 
-val univ_of_sort : t -> Univ.universe
-val sort_of_univ : Univ.universe -> t
+val univ_of_sort : t -> Univ.Universe.t
+val sort_of_univ : Univ.Universe.t -> t
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index d8e281d52..2913c6dfa 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -12,10 +12,11 @@
 (* This module checks subtyping of module types *)
 
 (*i*)
-open Util
 open Names
 open Univ
+open Util
 open Term
+open Constr
 open Declarations
 open Declareops
 open Reduction
@@ -77,7 +78,7 @@ let make_labmap mp list =
     | SFBmodule mb -> { map with mods = Label.Map.add l (Module mb) map.mods }
     | SFBmodtype mtb -> { map with mods = Label.Map.add l (Modtype mtb) map.mods }
   in
-  List.fold_right add_one list empty_labmap
+  CList.fold_right add_one list empty_labmap
 
 
 let check_conv_error error why cst poly f env a1 a2 =
@@ -153,7 +154,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
     let (ctx2,s2) = dest_arity env t2 in
     let s1,s2 =
       match s1, s2 with
-      | Type _, Type _ -> (* shortcut here *) prop_sort, prop_sort
+      | Type _, Type _ -> (* shortcut here *) Sorts.prop, Sorts.prop
       | (Prop _, Type _) | (Type _,Prop _) ->
 	error (NotConvertibleInductiveField name)
       | _ -> (s1, s2) in
@@ -216,7 +217,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   (* we check that records and their field names are preserved. *)
   check (fun mib -> mib.mind_record <> None) (==) (fun x -> RecordFieldExpected x);
   if mib1.mind_record <> None then begin
-    let rec names_prod_letin t = match kind_of_term t with
+    let rec names_prod_letin t = match kind t with
       | Prod(n,_,t) -> n::(names_prod_letin t)
       | LetIn(n,_,_,t) -> n::(names_prod_letin t)
       | Cast(t,_,_) -> names_prod_letin t
@@ -272,13 +273,13 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
             | Type u when not (is_univ_variable u) ->
               (* Both types are inferred, no need to recheck them. We
                  cheat and collapse the types to Prop *)
-                mkArity (ctx1,prop_sort), mkArity (ctx2,prop_sort)
+                mkArity (ctx1,Sorts.prop), mkArity (ctx2,Sorts.prop)
             | Prop _ ->
               (* The type in the interface is inferred, it may be the case
                  that the type in the implementation is smaller because
                  the body is more reduced. We safely collapse the upper
                  type to Prop *)
-                mkArity (ctx1,prop_sort), mkArity (ctx2,prop_sort)
+                mkArity (ctx1,Sorts.prop), mkArity (ctx2,Sorts.prop)
             | Type _ ->
               (* The type in the interface is inferred and the type in the
                  implementation is not inferred or is inferred but from a
diff --git a/kernel/term.ml b/kernel/term.ml
index 161abfba1..1c970867a 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -20,7 +20,7 @@ type contents = Sorts.contents = Pos | Null
 
 type sorts = Sorts.t =
   | Prop of contents       (** Prop and Set *)
-  | Type of Univ.universe  (** Type *)
+  | Type of Univ.Universe.t  (** Type *)
 
 type sorts_family = Sorts.family = InProp | InSet | InType
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 051979180..cb782afac 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Names
+open Constr
 
 (** {5 Redeclaration of types from module Constr and Sorts}
 
@@ -15,83 +16,7 @@ open Names
 
 *)
 
-type contents = Sorts.contents = Pos | Null
-
-type sorts = Sorts.t =
-  | Prop of contents       (** Prop and Set *)
-  | Type of Univ.universe  (** Type *)
-
-type sorts_family = Sorts.family = InProp | InSet | InType
-
-type 'a puniverses = 'a Univ.puniverses
-
-(** Simply type aliases *)
-type pconstant = Constant.t puniverses
-type pinductive = inductive puniverses
-type pconstructor = constructor puniverses
-
-type constr = Constr.constr
-(** Alias types, for compatibility. *)
-
-type types = Constr.types
-(** Same as [constr], for documentation purposes. *)
-
-type existential_key = Constr.existential_key
-
-type existential = Constr.existential
-
-type metavariable = Constr.metavariable
-
-type case_style = Constr.case_style =
-  LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
-
-type case_printing = Constr.case_printing =
-  { ind_tags : bool list; cstr_tags : bool list array; style : case_style }
-
-type case_info = Constr.case_info =
-  { ci_ind        : inductive;
-    ci_npar       : int;
-    ci_cstr_ndecls : int array;
-    ci_cstr_nargs : int array;
-    ci_pp_info    : case_printing
-  }
-
-type cast_kind = Constr.cast_kind =
-  VMcast | NATIVEcast | DEFAULTcast | REVERTcast
-
-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 =
-  ('constr, 'types) Constr.prec_declaration
-type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint
-type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint
-
-type ('constr, 'types, 'sort, 'univs) kind_of_term =
-  ('constr, 'types, 'sort, 'univs) Constr.kind_of_term =
-  | Rel       of int
-  | Var       of Id.t
-  | Meta      of metavariable
-  | Evar      of 'constr pexistential
-  | Sort      of 'sort
-  | 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.t * 'univs)
-  | Ind       of (inductive * 'univs)
-  | Construct of (constructor * 'univs)
-  | Case      of case_info * 'constr * 'constr * 'constr array
-  | Fix       of ('constr, 'types) pfixpoint
-  | CoFix     of ('constr, 'types) pcofixpoint
-  | Proj      of projection * 'constr
-
-type values = Constr.values
-
 (** {5 Simple term case analysis. } *)
-
 val isRel  : constr -> bool
 val isRelN : int -> constr -> bool
 val isVar  : constr -> bool
@@ -118,7 +43,7 @@ val is_Set  : constr -> bool
 val isprop : constr -> bool
 val is_Type : constr -> bool
 val iskind : constr -> bool
-val is_small : sorts -> bool
+val is_small : Sorts.t -> bool
 
 
 (** {5 Term destructors } *)
@@ -138,7 +63,7 @@ val destVar : constr -> Id.t
 
 (** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether
    [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *)
-val destSort : constr -> sorts
+val destSort : constr -> Sorts.t
 
 (** Destructs a casted term *)
 val destCast : constr -> constr * cast_kind * constr
@@ -197,7 +122,6 @@ val destFix : constr -> fixpoint
 
 val destCoFix : constr -> cofixpoint
 
-
 (** {5 Derived constructors} *)
 
 (** non-dependent product [t1 -> t2], an alias for
@@ -354,7 +278,7 @@ val strip_lam_assum : constr -> constr
     Such a term can canonically be seen as the pair of a context of types
     and of a sort *)
 
-type arity = Context.Rel.t * sorts
+type arity = Context.Rel.t * Sorts.t
 
 (** Build an "arity" from its canonical form *)
 val mkArity : arity -> types
@@ -368,7 +292,7 @@ val isArity : types -> bool
 (** {5 Kind of type} *)
 
 type ('constr, 'types) kind_of_type =
-  | SortType   of sorts
+  | SortType   of Sorts.t
   | CastType   of 'types * 'types
   | ProdType   of Name.t * 'types * 'types
   | LetInType  of Name.t * 'constr * 'types * 'types
@@ -378,23 +302,23 @@ val kind_of_type : types -> (constr, types) kind_of_type
 
 (** {5 Redeclaration of stuff from module [Sorts]} *)
 
-val set_sort  : sorts
-(** Alias for Sorts.set *)
+val set_sort  : Sorts.t
+[@@ocaml.deprecated "Alias for Sorts.set"]
 
-val prop_sort : sorts
-(** Alias for Sorts.prop *)
+val prop_sort : Sorts.t
+[@@ocaml.deprecated "Alias for Sorts.prop"]
 
-val type1_sort  : sorts
-(** Alias for Sorts.type1 *)
+val type1_sort  : Sorts.t
+[@@ocaml.deprecated "Alias for Sorts.type1"]
 
-val sorts_ord : sorts -> sorts -> int
-(** Alias for Sorts.compare *)
+val sorts_ord : Sorts.t -> Sorts.t -> int
+[@@ocaml.deprecated "Alias for Sorts.compare"]
 
-val is_prop_sort : sorts -> bool
-(** Alias for Sorts.is_prop *)
+val is_prop_sort : Sorts.t -> bool
+[@@ocaml.deprecated "Alias for Sorts.is_prop"]
 
-val family_of_sort : sorts -> sorts_family
-(** Alias for Sorts.family *)
+val family_of_sort : Sorts.t -> Sorts.family
+[@@ocaml.deprecated "Alias for Sorts.family"]
 
 (** {5 Redeclaration of stuff from module [Constr]}
 
@@ -403,90 +327,212 @@ val family_of_sort : sorts -> sorts_family
 (** {6 Term constructors. } *)
 
 val mkRel : int -> constr
+[@@ocaml.deprecated "Alias for Constr.mkRel"]
 val mkVar : Id.t -> constr
+[@@ocaml.deprecated "Alias for Constr.mkVar"]
 val mkMeta : metavariable -> constr
+[@@ocaml.deprecated "Alias for Constr.mkMeta"]
 val mkEvar : existential -> constr
-val mkSort : sorts -> types
+[@@ocaml.deprecated "Alias for Constr.mkEvar"]
+val mkSort : Sorts.t -> types
+[@@ocaml.deprecated "Alias for Constr.mkSort"]
 val mkProp : types
+[@@ocaml.deprecated "Alias for Constr.mkProp"]
 val mkSet  : types
-val mkType : Univ.universe -> types
+[@@ocaml.deprecated "Alias for Constr.mkSet"]
+val mkType : Univ.Universe.t -> types
+[@@ocaml.deprecated "Alias for Constr.mkType"]
 val mkCast : constr * cast_kind * constr -> constr
+[@@ocaml.deprecated "Alias for Constr"]
 val mkProd : Name.t * types * types -> types
+[@@ocaml.deprecated "Alias for Constr"]
 val mkLambda : Name.t * types * constr -> constr
+[@@ocaml.deprecated "Alias for Constr"]
 val mkLetIn : Name.t * constr * types * constr -> constr
+[@@ocaml.deprecated "Alias for Constr"]
 val mkApp : constr * constr array -> constr
+[@@ocaml.deprecated "Alias for Constr"]
 val mkConst : Constant.t -> constr
+[@@ocaml.deprecated "Alias for Constr"]
 val mkProj : projection * constr -> constr
+[@@ocaml.deprecated "Alias for Constr"]
 val mkInd : inductive -> constr
+[@@ocaml.deprecated "Alias for Constr"]
 val mkConstruct : constructor -> constr
+[@@ocaml.deprecated "Alias for Constr"]
 val mkConstU : Constant.t puniverses -> constr
+[@@ocaml.deprecated "Alias for Constr"]
 val mkIndU : inductive puniverses -> constr
+[@@ocaml.deprecated "Alias for Constr"]
 val mkConstructU : constructor puniverses -> constr
+[@@ocaml.deprecated "Alias for Constr"]
 val mkConstructUi : (pinductive * int) -> constr
+[@@ocaml.deprecated "Alias for Constr"]
 val mkCase : case_info * constr * constr * constr array -> constr
+[@@ocaml.deprecated "Alias for Constr"]
 val mkFix : fixpoint -> constr
+[@@ocaml.deprecated "Alias for Constr"]
 val mkCoFix : cofixpoint -> constr
+[@@ocaml.deprecated "Alias for Constr"]
 
 (** {6 Aliases} *)
 
 val eq_constr : constr -> constr -> bool
-(** Alias for [Constr.equal] *)
+[@@ocaml.deprecated "Alias for Constr.equal"]
 
 (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
    application grouping and the universe constraints in [u]. *)
 val eq_constr_univs : constr UGraph.check_function
+[@@ocaml.deprecated "Alias for Constr.eq_constr_univs"]
 
 (** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo 
     alpha, casts, application grouping and the universe constraints in [u]. *)
 val leq_constr_univs : constr UGraph.check_function
+[@@ocaml.deprecated "Alias for Constr.leq_constr_univs"]
 
 (** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts,
    application grouping and ignoring universe instances. *)
 val eq_constr_nounivs : constr -> constr -> bool
+[@@ocaml.deprecated "Alias for Constr.qe_constr_nounivs"]
 
 val kind_of_term : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term
-(** Alias for [Constr.kind] *)
+[@@ocaml.deprecated "Alias for Constr.kind"]
 
 val compare : constr -> constr -> int
-(** Alias for [Constr.compare] *)
+[@@ocaml.deprecated "Alias for [Constr.compare]"]
 
 val constr_ord : constr -> constr -> int
-(** Alias for [Term.compare] *)
+[@@ocaml.deprecated "Alias for [Term.compare]"]
 
 val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a
-(** Alias for [Constr.fold] *)
+[@@ocaml.deprecated "Alias for [Constr.fold]"]
 
 val map_constr : (constr -> constr) -> constr -> constr
-(** Alias for [Constr.map] *)
+[@@ocaml.deprecated "Alias for [Constr.map]"]
 
 val map_constr_with_binders :
   ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
-(** Alias for [Constr.map_with_binders] *)
+[@@ocaml.deprecated "Alias for [Constr.map_with_binders]"]
 
 val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses
-val univ_of_sort : sorts -> Univ.universe
-val sort_of_univ : Univ.universe -> sorts
+val univ_of_sort : Sorts.t -> Univ.Universe.t
+val sort_of_univ : Univ.Universe.t -> Sorts.t
 
 val iter_constr : (constr -> unit) -> constr -> unit
-(** Alias for [Constr.iter] *)
+[@@ocaml.deprecated "Alias for [Constr.iter]"]
 
 val iter_constr_with_binders :
   ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
-(** Alias for [Constr.iter_with_binders] *)
+[@@ocaml.deprecated "Alias for [Constr.iter_with_binders]"]
 
 val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
-(** Alias for [Constr.compare_head] *)
+[@@ocaml.deprecated "Alias for [Constr.compare_head]"]
+
+type constr = Constr.constr
+[@@ocaml.deprecated "Alias for Constr.t"]
+
+(** Alias types, for compatibility. *)
+
+type types = Constr.types
+[@@ocaml.deprecated "Alias for Constr.types"]
+
+type contents = Sorts.contents = Pos | Null
+[@@ocaml.deprecated "Alias for Sorts.contents"]
+
+type sorts = Sorts.t =
+  | Prop of Sorts.contents   (** Prop and Set *)
+  | Type of Univ.Universe.t  (** Type *)
+[@@ocaml.deprecated "Alias for Sorts.t"]
+
+type sorts_family = Sorts.family = InProp | InSet | InType
+[@@ocaml.deprecated "Alias for Sorts.family"]
+
+type 'a puniverses = 'a Constr.puniverses
+[@@ocaml.deprecated "Alias for Constr.puniverses"]
+
+(** Simply type aliases *)
+type pconstant = Constr.pconstant
+[@@ocaml.deprecated "Alias for Constr.pconstant"]
+type pinductive = Constr.pinductive
+[@@ocaml.deprecated "Alias for Constr.pinductive"]
+type pconstructor = Constr.pconstructor
+[@@ocaml.deprecated "Alias for Constr.pconstructor"]
+type existential_key = Constr.existential_key
+[@@ocaml.deprecated "Alias for Constr.existential_key"]
+type existential = Constr.existential
+[@@ocaml.deprecated "Alias for Constr.existential"]
+type metavariable = Constr.metavariable
+[@@ocaml.deprecated "Alias for Constr.metavariable"]
+
+type case_style = Constr.case_style =
+  LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
+[@@ocaml.deprecated "Alias for Constr.case_style"]
+
+type case_printing = Constr.case_printing =
+  { ind_tags : bool list; cstr_tags : bool list array; style : Constr.case_style }
+[@@ocaml.deprecated "Alias for Constr.case_printing"]
+
+type case_info = Constr.case_info =
+  { ci_ind         : inductive;
+    ci_npar        : int;
+    ci_cstr_ndecls : int array;
+    ci_cstr_nargs  : int array;
+    ci_pp_info     : Constr.case_printing
+  }
+[@@ocaml.deprecated "Alias for Constr.case_info"]
+
+type cast_kind = Constr.cast_kind =
+  VMcast | NATIVEcast | DEFAULTcast | REVERTcast
+[@@ocaml.deprecated "Alias for Constr.cast_kind"]
+
+type rec_declaration = Constr.rec_declaration
+[@@ocaml.deprecated "Alias for Constr.rec_declaration"]
+type fixpoint = Constr.fixpoint
+[@@ocaml.deprecated "Alias for Constr.fixpoint"]
+type cofixpoint = Constr.cofixpoint
+[@@ocaml.deprecated "Alias for Constr.cofixpoint"]
+type 'constr pexistential = 'constr Constr.pexistential
+[@@ocaml.deprecated "Alias for Constr.pexistential"]
+type ('constr, 'types) prec_declaration =
+  ('constr, 'types) Constr.prec_declaration
+[@@ocaml.deprecated "Alias for Constr.prec_declaration"]
+type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint
+[@@ocaml.deprecated "Alias for Constr.pfixpoint"]
+type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint
+[@@ocaml.deprecated "Alias for Constr.pcofixpoint"]
+
+type ('constr, 'types, 'sort, 'univs) kind_of_term =
+  ('constr, 'types, 'sort, 'univs) Constr.kind_of_term =
+  | Rel       of int
+  | Var       of Id.t
+  | Meta      of Constr.metavariable
+  | Evar      of 'constr Constr.pexistential
+  | Sort      of 'sort
+  | Cast      of 'constr * 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.t * 'univs)
+  | Ind       of (inductive * 'univs)
+  | Construct of (constructor * 'univs)
+  | Case      of Constr.case_info * 'constr * 'constr * 'constr array
+  | Fix       of ('constr, 'types) Constr.pfixpoint
+  | CoFix     of ('constr, 'types) Constr.pcofixpoint
+  | Proj      of projection * 'constr
+[@@ocaml.deprecated "Alias for Constr.kind_of_term"]
 
-val hash_constr : constr -> int
-(** Alias for [Constr.hash] *)
+type values = Constr.values
+[@@ocaml.deprecated "Alias for Constr.values"]
 
-(*********************************************************************)
+val hash_constr : Constr.constr -> int
+[@@ocaml.deprecated "Alias for Constr.hash"]
 
-val hcons_sorts : sorts -> sorts
-(** Alias for [Constr.hashcons_sorts] *)
+val hcons_sorts : Sorts.t -> Sorts.t
+[@@ocaml.deprecated "Alias for [Sorts.hcons]"]
 
-val hcons_constr : constr -> constr
-(** Alias for [Constr.hashcons] *)
+val hcons_constr : Constr.constr -> Constr.constr
+[@@ocaml.deprecated "Alias for [Constr.hcons]"]
 
-val hcons_types : types -> types
-(** Alias for [Constr.hashcons] *)
+val hcons_types : Constr.types -> Constr.types
+[@@ocaml.deprecated "Alias for [Constr.hcons]"]
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index d50abf071..4617f2d5f 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -15,7 +15,7 @@
 open CErrors
 open Util
 open Names
-open Term
+open Constr
 open Declarations
 open Environ
 open Entries
@@ -154,7 +154,7 @@ let inline_side_effects env body ctx side_eff =
       (** Lift free rel variables *)
       if n <= k then t
       else mkRel (n + len - i - 1)
-    | _ -> map_constr_with_binders ((+) 1) (fun k t -> subst_const i k t) k t
+    | _ -> Constr.map_with_binders ((+) 1) (fun k t -> subst_const i k t) k t
     in
     let map_args i (na, b, ty, opaque) =
       (** Both the type and the body may mention other constants *)
@@ -199,13 +199,13 @@ let check_signatures curmb sl =
 let skip_trusted_seff sl b e =
   let rec aux sl b e acc =
     let open Context.Rel.Declaration in
-    match sl, kind_of_term b with
+    match sl, kind b with
     | (None|Some 0), _ -> b, e, acc
     | Some sl, LetIn (n,c,ty,bo) ->
        aux (Some (sl-1)) bo
          (Environ.push_rel (LocalDef (n,c,ty)) e) (`Let(n,c,ty)::acc)
     | Some sl, App(hd,arg) ->
-       begin match kind_of_term hd with
+       begin match kind hd with
        | Lambda (n,ty,bo) ->
            aux (Some (sl-1)) bo
              (Environ.push_rel (LocalAssum (n,ty)) e) (`Cut(n,ty,arg)::acc)
@@ -245,7 +245,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
         abstract_constant_universes abstract uctx
       in
       let c = Typeops.assumption_of_judgment env j in
-      let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in
+      let t = Constr.hcons (Vars.subst_univs_level_constr usubst c) in
       {
         Cooking.cook_body = Undef nl;
         cook_type = t;
@@ -283,7 +283,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
             let _ = judge_of_cast env j DEFAULTcast tyj in
             j, uctx
           in
-          let c = hcons_constr j.uj_val in
+          let c = Constr.hcons j.uj_val in
           feedback_completion_typecheck feedback_id;
           c, uctx) in
       let def = OpaqueDef (Opaqueproof.create proofterm) in
@@ -325,7 +325,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
            let _ = judge_of_cast env j DEFAULTcast tj in
            Vars.subst_univs_level_constr usubst t
       in
-      let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
+      let def = Constr.hcons (Vars.subst_univs_level_constr usubst j.uj_val) in
       let def = 
 	if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
 	else Def (Mod_subst.from_val def) 
@@ -359,7 +359,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
     in
     let term, typ = pb.proj_eta in
     {
-      Cooking.cook_body = Def (Mod_subst.from_val (hcons_constr term));
+      Cooking.cook_body = Def (Mod_subst.from_val (Constr.hcons term));
       cook_type = typ;
       cook_proj = Some pb;
       cook_universes = univs;
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 815269169..9b35bfc6e 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Environ
 open Declarations
 open Entries
@@ -19,7 +19,7 @@ type _ trust =
 | SideEffects : structure_body -> side_effects trust
 
 val translate_local_def : 'a trust -> env -> Id.t -> 'a definition_entry ->
-  constant_def * types * Univ.universe_context
+  constant_def * types * Univ.UContext.t
 
 val translate_local_assum : env -> types -> types
 
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 9813fc566..3a1f2ae00 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Environ
 open Reduction
 
@@ -45,8 +45,8 @@ type ('constr, 'types) ptype_error =
   | NotAType of ('constr, 'types) punsafe_judgment
   | BadAssumption of ('constr, 'types) punsafe_judgment
   | ReferenceVariables of Id.t * 'constr
-  | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment
-      * (sorts_family * sorts_family * arity_error) option
+  | ElimArity of pinductive * Sorts.family list * 'constr * ('constr, 'types) punsafe_judgment
+      * (Sorts.family * Sorts.family * arity_error) option
   | CaseNotInductive of ('constr, 'types) punsafe_judgment
   | WrongCaseInfo of pinductive * case_info
   | NumberBranches of ('constr, 'types) punsafe_judgment * int
@@ -115,6 +115,7 @@ let error_ill_typed_rec_body env i lna vdefj vargs =
   raise (TypeError (env, IllTypedRecBody (i,lna,vdefj,vargs)))
 
 let error_elim_explain kp ki =
+  let open Sorts in
   match kp,ki with
   | (InType | InSet), InProp -> NonInformativeToInformative
   | InType, InSet -> StrongEliminationOnNonSmallType (* if Set impredicative *)
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 95a963da2..e4fa65686 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Environ
 
 (** Type errors. {% \label{%}typeerrors{% }%} *)
@@ -46,8 +46,8 @@ type ('constr, 'types) ptype_error =
   | NotAType of ('constr, 'types) punsafe_judgment
   | BadAssumption of ('constr, 'types) punsafe_judgment
   | ReferenceVariables of Id.t * 'constr
-  | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment
-      * (sorts_family * sorts_family * arity_error) option
+  | ElimArity of pinductive * Sorts.family list * 'constr * ('constr, 'types) punsafe_judgment
+      * (Sorts.family * Sorts.family * arity_error) option
   | CaseNotInductive of ('constr, 'types) punsafe_judgment
   | WrongCaseInfo of pinductive * case_info
   | NumberBranches of ('constr, 'types) punsafe_judgment * int
@@ -77,8 +77,8 @@ val error_assumption : env -> unsafe_judgment -> 'a
 val error_reference_variables : env -> Id.t -> constr -> 'a
 
 val error_elim_arity :
-  env -> pinductive -> sorts_family list -> constr -> unsafe_judgment ->
-      (sorts_family * sorts_family * arity_error) option -> 'a
+  env -> pinductive -> Sorts.family list -> constr -> unsafe_judgment ->
+      (Sorts.family * Sorts.family * arity_error) option -> 'a
 
 val error_case_not_inductive : env -> unsafe_judgment -> 'a
 
@@ -103,6 +103,6 @@ val error_ill_formed_rec_body :
 val error_ill_typed_rec_body  :
   env -> int -> Name.t array -> unsafe_judgment array -> types array -> 'a
 
-val error_elim_explain : sorts_family -> sorts_family -> arity_error
+val error_elim_explain : Sorts.family -> Sorts.family -> arity_error
 
 val error_unsatisfied_constraints : env -> Univ.constraints -> 'a
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index f99f34b06..4ccef5c38 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -10,7 +10,8 @@ open CErrors
 open Util
 open Names
 open Univ
-open Term
+open Sorts
+open Constr
 open Vars
 open Declarations
 open Environ
@@ -38,7 +39,7 @@ let check_constraints cst env =
 
 (* This should be a type (a priori without intention to be an assumption) *)
 let check_type env c t =
-  match kind_of_term(whd_all env t) with
+  match kind(whd_all env t) with
   | Sort s -> s
   | _ -> error_not_type env (make_judge c t)
 
@@ -57,7 +58,7 @@ let check_assumption env t ty =
 
 (* Prop and Set *)
 
-let type1 = mkSort type1_sort
+let type1 = mkSort Sorts.type1
 
 (* Type of Type(i). *)
 
@@ -152,7 +153,7 @@ let type_of_apply env func funt argsv argstv =
   let rec apply_rec i typ = 
     if Int.equal i len then typ
     else 
-      (match kind_of_term (whd_all env typ) with
+      (match kind (whd_all env typ) with
       | Prod (_,c1,c2) ->
 	let arg = argsv.(i) and argt = argstv.(i) in
 	  (try
@@ -300,7 +301,7 @@ let type_of_projection env p c ct =
   in
   assert(MutInd.equal pb.proj_ind (fst ind));
   let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in
-  substl (c :: List.rev args) ty
+  substl (c :: CList.rev args) ty
       
 
 (* Fixpoints. *)
@@ -325,7 +326,7 @@ let check_fixpoint env lna lar vdef vdeft =
     arbitraires et non plus des variables *)
 let rec execute env cstr =
   let open Context.Rel.Declaration in
-  match kind_of_term cstr with
+  match kind cstr with
     (* Atomic terms *)
     | Sort s -> type_of_sort s
 
@@ -346,7 +347,7 @@ let rec execute env cstr =
     | App (f,args) ->
         let argst = execute_array env args in
 	let ft =
-	  match kind_of_term f with
+	  match kind f with
 	  | Ind ind when Environ.template_polymorphic_pind ind env ->
 	    let args = Array.map (fun t -> lazy t) argst in
               type_of_inductive_knowing_parameters env ind args
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 96be6c14a..3aaad5877 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -8,7 +8,7 @@
 
 open Names
 open Univ
-open Term
+open Constr
 open Environ
 open Entries
 
@@ -41,8 +41,8 @@ val type1 : types
 val type_of_sort : Sorts.t -> types
 val judge_of_prop : unsafe_judgment
 val judge_of_set  : unsafe_judgment
-val judge_of_prop_contents  : contents -> unsafe_judgment
-val judge_of_type           : universe -> unsafe_judgment
+val judge_of_prop_contents  : Sorts.contents -> unsafe_judgment
+val judge_of_type           : Universe.t -> unsafe_judgment
 
 (** {6 Type of a bound variable. } *)
 val type_of_relative : env -> int -> types
@@ -71,8 +71,8 @@ val judge_of_abstraction :
     -> unsafe_judgment
 
 (** {6 Type of a product. } *)
-val sort_of_product : env -> sorts -> sorts -> sorts
-val type_of_product : env -> Name.t -> sorts -> sorts -> types
+val sort_of_product : env -> Sorts.t -> Sorts.t -> Sorts.t
+val type_of_product : env -> Name.t -> Sorts.t -> Sorts.t -> types
 val judge_of_product :
   env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment
     -> unsafe_judgment
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 9793dd881..00c0ea70d 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -910,3 +910,4 @@ let check_leq =
     let check_leq_key = Profile.declare_profile "check_leq" in
       Profile.profile3 check_leq_key check_leq
   else check_leq
+
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 2fe555018..b95388ed0 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -9,63 +9,64 @@
 open Univ
 
 (** {6 Graphs of universes. } *)
-
 type t
-
 type universes = t
+[@@ocaml.deprecated "Use UGraph.t"]
 
-type 'a check_function = universes -> 'a -> 'a -> bool
-val check_leq : universe check_function
-val check_eq : universe check_function
-val check_eq_level : universe_level check_function
+type 'a check_function = t -> 'a -> 'a -> bool
 
-(** The empty graph of universes *)
-val empty_universes : universes
+val check_leq : Universe.t check_function
+val check_eq : Universe.t check_function
+val check_eq_level : Level.t check_function
 
 (** The initial graph of universes: Prop < Set *)
-val initial_universes : universes
+val initial_universes : t
+
+(** Check if we are in the initial case *)
+val is_initial_universes : t -> bool
+
+(** Check equality of instances w.r.t. a universe graph *)
+val check_eq_instances : Instance.t check_function
+
+(** {6 ... } *)
+(** Merge of constraints in a universes graph.
+  The function [merge_constraints] merges a set of constraints in a given
+  universes graph. It raises the exception [UniverseInconsistency] if the
+  constraints are not satisfiable. *)
 
-val is_initial_universes : universes -> bool
+val enforce_constraint : univ_constraint -> t -> t
+val merge_constraints : constraints -> t -> t
 
-val sort_universes : universes -> universes
+val check_constraint  : t -> univ_constraint -> bool
+val check_constraints : constraints -> t -> bool
 
 (** Adds a universe to the graph, ensuring it is >= or > Set.
    @raises AlreadyDeclared if the level is already declared in the graph. *)
 
 exception AlreadyDeclared
 
-val add_universe : universe_level -> bool -> universes -> universes
+val add_universe : Level.t -> bool -> t -> t
 
-(** {6 ... } *)
-(** Merge of constraints in a universes graph.
-  The function [merge_constraints] merges a set of constraints in a given
-  universes graph. It raises the exception [UniverseInconsistency] if the
-  constraints are not satisfiable. *)
+(** {6 Pretty-printing of universes. } *)
 
-val enforce_constraint : univ_constraint -> universes -> universes
-val merge_constraints : constraints -> universes -> universes
+val pr_universes : (Level.t -> Pp.t) -> t -> Pp.t
 
-val constraints_of_universes : universes -> constraints
+(** The empty graph of universes *)
+val empty_universes : t
+[@@ocaml.deprecated "Use UGraph.initial_universes"]
 
-val check_constraint  : universes -> univ_constraint -> bool
-val check_constraints : constraints -> universes -> bool
+val sort_universes : t -> t
 
-val check_eq_instances : Instance.t check_function
-(** Check equality of instances w.r.t. a universe graph *)
+val constraints_of_universes : t -> constraints
 
 val check_subtype : AUContext.t check_function
 (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
     [ctx1]. *)
 
-(** {6 Pretty-printing of universes. } *)
-
-val pr_universes : (Level.t -> Pp.t) -> universes -> Pp.t
-
 (** {6 Dumping to a file } *)
 
 val dump_universes :
-  (constraint_type -> string -> string -> unit) ->
-  universes -> unit
+  (constraint_type -> string -> string -> unit) -> t -> unit
 
 (** {6 Debugging} *)
-val check_universes_invariants : universes -> unit
+val check_universes_invariants : t -> unit
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 94116e473..8d46a8bee 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 (** Universes. *)
-
 module Level :
 sig
   type t
@@ -20,11 +19,11 @@ sig
 
   val is_small : t -> bool
   (** Is the universe set or prop? *)
-		       
+
   val is_prop : t -> bool
   val is_set : t -> bool
   (** Is it specifically Prop or Set *)
-		       
+
   val compare : t -> t -> int
   (** Comparison function *)
 
@@ -49,18 +48,19 @@ sig
 end
 
 type universe_level = Level.t
-(** Alias name. *)
+[@@ocaml.deprecated "Use Level.t"]
 
 (** Sets of universe levels *)
-module LSet : 
-sig 
-  include CSig.SetS with type elt = universe_level
-	      
+module LSet :
+sig
+  include CSig.SetS with type elt = Level.t
+
   val pr : (Level.t -> Pp.t) -> t -> Pp.t
   (** Pretty-printing *)
 end
 
 type universe_set = LSet.t
+[@@ocaml.deprecated "Use LSet.t"]
 
 module Universe :
 sig
@@ -106,17 +106,17 @@ sig
 
   val super : t -> t
   (** The universe strictly above *)
-    
+
   val sup   : t -> t -> t
   (** The l.u.b. of 2 universes *)
 
-  val type0m : t  
+  val type0m : t
   (** image of Prop in the universes hierarchy *)
-  
-  val type0 : t  
+
+  val type0 : t
   (** image of Set in the universes hierarchy *)
-  
-  val type1 : t 
+
+  val type1 : t
   (** the universe of the type of Prop/Set *)
 
   val exists : (Level.t * int -> bool) -> t -> bool
@@ -124,40 +124,41 @@ sig
 end
 
 type universe = Universe.t
+[@@ocaml.deprecated "Use Universe.t"]
 
 (** Alias name. *)
 
-val pr_uni : universe -> Pp.t
-	      
-(** The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ... 
+val pr_uni : Universe.t -> Pp.t
+
+(** The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ...
    Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *)
-val type0m_univ : universe
-val type0_univ : universe
-val type1_univ : universe
+val type0m_univ : Universe.t
+val type0_univ : Universe.t
+val type1_univ : Universe.t
 
-val is_type0_univ : universe -> bool
-val is_type0m_univ : universe -> bool
-val is_univ_variable : universe -> bool
-val is_small_univ : universe -> bool
+val is_type0_univ : Universe.t -> bool
+val is_type0m_univ : Universe.t -> bool
+val is_univ_variable : Universe.t -> bool
+val is_small_univ : Universe.t -> bool
 
-val sup : universe -> universe -> universe
-val super : universe -> universe
+val sup : Universe.t -> Universe.t -> Universe.t
+val super : Universe.t -> Universe.t
 
-val universe_level : universe -> universe_level option
+val universe_level : Universe.t -> Level.t option
 
 (** [univ_level_mem l u] Is l is mentionned in u ? *)
 
-val univ_level_mem : universe_level -> universe -> bool
+val univ_level_mem : Level.t -> Universe.t -> bool
 
 (** [univ_level_rem u v min] removes [u] from [v], resulting in [min]
     if [v] was exactly [u]. *)
 
-val univ_level_rem : universe_level -> universe -> universe -> universe
+val univ_level_rem : Level.t -> Universe.t -> Universe.t -> Universe.t
 
 (** {6 Constraints. } *)
 
 type constraint_type = Lt | Le | Eq
-type univ_constraint = universe_level * constraint_type * universe_level
+type univ_constraint = Level.t * constraint_type * Level.t
 
 module Constraint : sig
  include Set.S with type elt = univ_constraint
@@ -179,10 +180,10 @@ val constraints_of : 'a constrained -> constraints
 
 type 'a constraint_function = 'a -> 'a -> constraints -> constraints
 
-val enforce_eq : universe constraint_function
-val enforce_leq : universe constraint_function
-val enforce_eq_level : universe_level constraint_function
-val enforce_leq_level : universe_level constraint_function
+val enforce_eq : Universe.t constraint_function
+val enforce_leq : Universe.t constraint_function
+val enforce_eq_level : Level.t constraint_function
+val enforce_leq_level : Level.t constraint_function
 
 (** Type explanation is used to decorate error messages to provide
   useful explanation why a given constraint is rejected. It is composed
@@ -196,17 +197,17 @@ val enforce_leq_level : universe_level constraint_function
   system stores the graph and may result from combination of several
   constraints...
 *)
-type explanation = (constraint_type * universe) list
-type univ_inconsistency = constraint_type * universe * universe * explanation option
+type explanation = (constraint_type * Universe.t) list
+type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation option
 
 exception UniverseInconsistency of univ_inconsistency
 
 (** {6 Support for universe polymorphism } *)
 
 (** Polymorphic maps from universe levels to 'a *)
-module LMap : 
+module LMap :
 sig
-  include CMap.ExtS with type key = universe_level and module Set := LSet
+  include CMap.ExtS with type key = Level.t and module Set := LSet
 
   val union : 'a t -> 'a t -> 'a t
   (** [union x y] favors the bindings in the first map. *)
@@ -226,18 +227,18 @@ type 'a universe_map = 'a LMap.t
 
 (** {6 Substitution} *)
 
-type universe_subst_fn = universe_level -> universe
-type universe_level_subst_fn = universe_level -> universe_level
+type universe_subst_fn = Level.t -> Universe.t
+type universe_level_subst_fn = Level.t -> Level.t
 
 (** A full substitution, might involve algebraic universes *)
-type universe_subst = universe universe_map
-type universe_level_subst = universe_level universe_map
+type universe_subst = Universe.t universe_map
+type universe_level_subst = Level.t universe_map
 
 val level_subst_of : universe_subst_fn -> universe_level_subst_fn
 
 (** {6 Universe instances} *)
 
-module Instance : 
+module Instance :
 sig
   type t
   (** A universe instance represents a vector of argument universes
@@ -279,10 +280,11 @@ sig
 end
 
 type universe_instance = Instance.t
+[@@ocaml.deprecated "Use Instance.t"]
 
-val enforce_eq_instances : universe_instance constraint_function
+val enforce_eq_instances : Instance.t constraint_function
 
-type 'a puniverses = 'a * universe_instance
+type 'a puniverses = 'a * Instance.t
 val out_punivs : 'a puniverses -> 'a
 val in_punivs : 'a -> 'a puniverses
 
@@ -292,14 +294,14 @@ val eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool
     representiong local universe variables and associated constraints *)
 
 module UContext :
-sig 
+sig
   type t
 
   val make : Instance.t constrained -> t
 
   val empty : t
   val is_empty : t -> bool
-    
+
   val instance : t -> Instance.t
   val constraints : t -> constraints
 
@@ -314,9 +316,10 @@ sig
 end
 
 type universe_context = UContext.t
+[@@ocaml.deprecated "Use UContext.t"]
 
 module AUContext :
-sig 
+sig
   type t
 
   val repr : t -> UContext.t
@@ -340,6 +343,7 @@ sig
 end
 
 type abstract_universe_context = AUContext.t
+[@@ocaml.deprecated "Use AUContext.t"]
 
 (** Universe info for inductive types: A context of universe levels
     with universe constraints, representing local universe variables
@@ -354,49 +358,51 @@ module CumulativityInfo :
 sig
   type t
 
-  val make : universe_context * universe_context -> t
+  val make : UContext.t * UContext.t -> t
 
   val empty : t
   val is_empty : t -> bool
 
-  val univ_context : t -> universe_context
-  val subtyp_context : t -> universe_context
+  val univ_context : t -> UContext.t
+  val subtyp_context : t -> UContext.t
 
   (** This function takes a universe context representing constraints
       of an inductive and a Instance.t of fresh universe names for the
       subtyping (with the same length as the context in the given
       universe context) and produces a UInfoInd.t that with the
       trivial subtyping relation. *)
-  val from_universe_context : universe_context -> universe_instance -> t
+  val from_universe_context : UContext.t -> Instance.t -> t
 
   val subtyping_susbst : t -> universe_level_subst
 
 end
 
 type cumulativity_info = CumulativityInfo.t
+[@@ocaml.deprecated "Use CumulativityInfo.t"]
 
 module ACumulativityInfo :
 sig
   type t
 
-  val univ_context : t -> abstract_universe_context
-  val subtyp_context : t -> abstract_universe_context
+  val univ_context : t -> AUContext.t
+  val subtyp_context : t -> AUContext.t
 end
 
 type abstract_cumulativity_info = ACumulativityInfo.t
+[@@ocaml.deprecated "Use ACumulativityInfo.t"]
 
 (** Universe contexts (as sets) *)
 
 module ContextSet :
-sig 
-  type t = universe_set constrained
+sig
+  type t = LSet.t constrained
 
   val empty : t
   val is_empty : t -> bool
 
-  val singleton : universe_level -> t
+  val singleton : Level.t -> t
   val of_instance : Instance.t -> t
-  val of_set : universe_set -> t
+  val of_set : LSet.t -> t
 
   val equal : t -> t -> bool
   val union : t -> t -> t
@@ -406,39 +412,40 @@ sig
       much smaller than the right one. *)
 
   val diff : t -> t -> t
-  val add_universe : universe_level -> t -> t
+  val add_universe : Level.t -> t -> t
   val add_constraints : constraints -> t -> t
   val add_instance : Instance.t -> t -> t
 
   (** Arbitrary choice of linear order of the variables *)
   val sort_levels : Level.t array -> Level.t array
-  val to_context : t -> universe_context
-  val of_context : universe_context -> t
+  val to_context : t -> UContext.t
+  val of_context : UContext.t -> t
 
   val constraints : t -> constraints
-  val levels : t -> universe_set
+  val levels : t -> LSet.t
 end
 
 (** A set of universes with universe constraints.
-    We linearize the set to a list after typechecking. 
+    We linearize the set to a list after typechecking.
     Beware, representation could change.
 *)
 type universe_context_set = ContextSet.t
+[@@ocaml.deprecated "Use ContextSet.t"]
 
 (** A value in a universe context (resp. context set). *)
-type 'a in_universe_context = 'a * universe_context
-type 'a in_universe_context_set = 'a * universe_context_set
+type 'a in_universe_context = 'a * UContext.t
+type 'a in_universe_context_set = 'a * ContextSet.t
 
 val empty_level_subst : universe_level_subst
 val is_empty_level_subst : universe_level_subst -> bool
 
 (** Substitution of universes. *)
-val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level
-val subst_univs_level_universe : universe_level_subst -> universe -> universe
+val subst_univs_level_level : universe_level_subst -> Level.t -> Level.t
+val subst_univs_level_universe : universe_level_subst -> Universe.t -> Universe.t
 val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints
 val subst_univs_level_abstract_universe_context :
-  universe_level_subst -> abstract_universe_context -> abstract_universe_context
-val subst_univs_level_instance : universe_level_subst -> universe_instance -> universe_instance
+  universe_level_subst -> AUContext.t -> AUContext.t
+val subst_univs_level_instance : universe_level_subst -> Instance.t -> Instance.t
 
 (** Level to universe substitutions. *)
 
@@ -446,32 +453,32 @@ val empty_subst : universe_subst
 val is_empty_subst : universe_subst -> bool
 val make_subst : universe_subst -> universe_subst_fn
 
-val subst_univs_universe : universe_subst_fn -> universe -> universe
+val subst_univs_universe : universe_subst_fn -> Universe.t -> Universe.t
 val subst_univs_constraints : universe_subst_fn -> constraints -> constraints
 
 (** Substitution of instances *)
-val subst_instance_instance : universe_instance -> universe_instance -> universe_instance
-val subst_instance_universe : universe_instance -> universe -> universe
+val subst_instance_instance : Instance.t -> Instance.t -> Instance.t
+val subst_instance_universe : Instance.t -> Universe.t -> Universe.t
 
-val make_instance_subst : universe_instance -> universe_level_subst
-val make_inverse_instance_subst : universe_instance -> universe_level_subst
+val make_instance_subst : Instance.t -> universe_level_subst
+val make_inverse_instance_subst : Instance.t -> universe_level_subst
 
-val abstract_universes : universe_context -> universe_level_subst * abstract_universe_context
+val abstract_universes : UContext.t -> universe_level_subst * AUContext.t
 
-val abstract_cumulativity_info : cumulativity_info -> universe_level_subst * abstract_cumulativity_info
+val abstract_cumulativity_info : CumulativityInfo.t -> universe_level_subst * ACumulativityInfo.t
 
-val make_abstract_instance : abstract_universe_context -> universe_instance
+val make_abstract_instance : AUContext.t -> Instance.t
 
 (** {6 Pretty-printing of universes. } *)
 
 val pr_constraint_type : constraint_type -> Pp.t
 val pr_constraints : (Level.t -> Pp.t) -> constraints -> Pp.t
-val pr_universe_context : (Level.t -> Pp.t) -> universe_context -> Pp.t
-val pr_cumulativity_info : (Level.t -> Pp.t) -> cumulativity_info -> Pp.t
-val pr_abstract_universe_context : (Level.t -> Pp.t) -> abstract_universe_context -> Pp.t
-val pr_abstract_cumulativity_info : (Level.t -> Pp.t) -> abstract_cumulativity_info -> Pp.t
-val pr_universe_context_set : (Level.t -> Pp.t) -> universe_context_set -> Pp.t
-val explain_universe_inconsistency : (Level.t -> Pp.t) -> 
+val pr_universe_context : (Level.t -> Pp.t) -> UContext.t -> Pp.t
+val pr_cumulativity_info : (Level.t -> Pp.t) -> CumulativityInfo.t -> Pp.t
+val pr_abstract_universe_context : (Level.t -> Pp.t) -> AUContext.t -> Pp.t
+val pr_abstract_cumulativity_info : (Level.t -> Pp.t) -> ACumulativityInfo.t -> Pp.t
+val pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t
+val explain_universe_inconsistency : (Level.t -> Pp.t) ->
   univ_inconsistency -> Pp.t
 
 val pr_universe_level_subst : universe_level_subst -> Pp.t
@@ -479,23 +486,28 @@ val pr_universe_subst : universe_subst -> Pp.t
 
 (** {6 Hash-consing } *)
 
-val hcons_univ : universe -> universe
+val hcons_univ : Universe.t -> Universe.t
 val hcons_constraints : constraints -> constraints
-val hcons_universe_set : universe_set -> universe_set
-val hcons_universe_context : universe_context -> universe_context
-val hcons_abstract_universe_context : abstract_universe_context -> abstract_universe_context
-val hcons_universe_context_set : universe_context_set -> universe_context_set 
-val hcons_cumulativity_info : cumulativity_info -> cumulativity_info
-val hcons_abstract_cumulativity_info : abstract_cumulativity_info -> abstract_cumulativity_info
+val hcons_universe_set : LSet.t -> LSet.t
+val hcons_universe_context : UContext.t -> UContext.t
+val hcons_abstract_universe_context : AUContext.t -> AUContext.t
+val hcons_universe_context_set : ContextSet.t -> ContextSet.t
+val hcons_cumulativity_info : CumulativityInfo.t -> CumulativityInfo.t
+val hcons_abstract_cumulativity_info : ACumulativityInfo.t -> ACumulativityInfo.t
 
 (******)
 
 (* deprecated: use qualified names instead *)
-val compare_levels : universe_level -> universe_level -> int
-val eq_levels : universe_level -> universe_level -> bool
+val compare_levels : Level.t -> Level.t -> int
+[@@ocaml.deprecated "Use Level.compare"]
+
+val eq_levels : Level.t -> Level.t -> bool
+[@@ocaml.deprecated "Use Level.equal"]
 
 (** deprecated: Equality of formal universe expressions. *)
-val equal_universes : universe -> universe -> bool
+val equal_universes : Universe.t -> Universe.t -> bool
+[@@ocaml.deprecated "Use Universe.equal"]
 
 (** Universes of constraints *)
-val universes_of_constraints : constraints -> universe_set
+val universes_of_constraints : constraints -> LSet.t
+[@@ocaml.deprecated "Use Constraint.universes_of"]
diff --git a/kernel/vars.mli b/kernel/vars.mli
index ae846fd42..964de4e95 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -141,8 +141,8 @@ val subst_univs_level_constr : universe_level_subst -> constr -> constr
 val subst_univs_level_context : Univ.universe_level_subst -> Context.Rel.t -> Context.Rel.t
 
 (** Instance substitution for polymorphism. *)
-val subst_instance_constr : universe_instance -> constr -> constr
-val subst_instance_context : universe_instance -> Context.Rel.t -> Context.Rel.t
+val subst_instance_constr : Instance.t -> constr -> constr
+val subst_instance_context : Instance.t -> Context.Rel.t -> Context.Rel.t
 
 type id_key = Constant.t tableKey
 val eq_id_key : id_key -> id_key -> bool
diff --git a/kernel/vconv.mli b/kernel/vconv.mli
index f4e680c69..7f727df47 100644
--- a/kernel/vconv.mli
+++ b/kernel/vconv.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
+open Constr
 open Environ
 open Reduction
 
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 4e13881b8..51101f88e 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -7,7 +7,8 @@
 (************************************************************************)
 
 open Names
-open Term
+open Sorts
+open Constr
 open Cbytecodes
 
 external set_drawinstr : unit -> unit = "coq_set_drawinstr"
@@ -137,7 +138,7 @@ type vswitch = {
 type atom =
   | Aid of Vars.id_key
   | Aind of inductive
-  | Atype of Univ.universe
+  | Atype of Univ.Universe.t
 
 (* Zippers *)
 
@@ -152,7 +153,7 @@ type stack = zipper list
 type to_up = values
 
 type whd =
-  | Vsort of sorts
+  | Vsort of Sorts.t
   | Vprod of vprod
   | Vfun of vfun
   | Vfix of vfix * arguments option
@@ -160,7 +161,7 @@ type whd =
   | Vconstr_const of int
   | Vconstr_block of vblock
   | Vatom_stk of atom * stack
-  | Vuniv_level of Univ.universe_level
+  | Vuniv_level of Univ.Level.t
 
 (************************************************)
 (* Abstract machine *****************************)
@@ -216,7 +217,7 @@ let apply_varray vf varray =
 (* Destructors ***********************************)
 (*************************************************)
 
-let uni_lvl_val (v : values) : Univ.universe_level =
+let uni_lvl_val (v : values) : Univ.Level.t =
     let whd = Obj.magic v in
     match whd with
     | Vuniv_level lvl -> lvl
diff --git a/kernel/vm.mli b/kernel/vm.mli
index ea38ee43f..bc38452d4 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -1,5 +1,13 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 open Names
-open Term
+open Constr
 open Cbytecodes
 
 (** Debug printing *)
@@ -23,7 +31,7 @@ type arguments
 type atom =
   | Aid of Vars.id_key
   | Aind of inductive
-  | Atype of Univ.universe
+  | Atype of Univ.Universe.t
 
 (** Zippers *)
 
@@ -38,7 +46,7 @@ type stack = zipper list
 type to_up
 
 type whd =
-  | Vsort of sorts
+  | Vsort of Sorts.t
   | Vprod of vprod
   | Vfun of vfun
   | Vfix of vfix * arguments option
@@ -46,7 +54,7 @@ type whd =
   | Vconstr_const of int
   | Vconstr_block of vblock
   | Vatom_stk of atom * stack
-  | Vuniv_level of Univ.universe_level
+  | Vuniv_level of Univ.Level.t
 
 (** For debugging purposes only *)
 
@@ -66,7 +74,7 @@ external val_of_annot_switch : annot_switch -> values = "%identity"
 (** Destructors *)
 
 val whd_val : values -> whd
-val uni_lvl_val : values -> Univ.universe_level
+val uni_lvl_val : values -> Univ.Level.t
 
 (** Arguments *)