Merge PR #6098: [api] Move structures deprecated in the API to the core.

38 files changed, 108 insertions, 100 deletions

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index ea33f1c0d6..d59102b6c7 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -10,6 +10,7 @@
 open Names
 open Globnames
 open Term
+open Constr
 open Environ
 open Util
 open Libobject
@@ -103,7 +104,7 @@ let rename_type_of_constructor env cstruct =
 let rename_typing env c =
   let j = Typeops.infer env c in
   let j' =
-    match kind_of_term c with
+    match kind c with
     | Const (c,u) -> { j with uj_type = rename_type j.uj_type (ConstRef c) }
     | Ind (i,u) -> { j with uj_type = rename_type j.uj_type (IndRef i) }
     | Construct (k,u) -> { j with uj_type = rename_type j.uj_type (ConstructRef k) }
diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli
index 804e38216c..b499da3ab7 100644
--- a/pretyping/arguments_renaming.mli
+++ b/pretyping/arguments_renaming.mli
@@ -9,7 +9,7 @@
 open Names
 open Globnames
 open Environ
-open Term
+open Constr
 
 val rename_arguments : bool -> global_reference -> Name.t list -> unit
 
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index aefa09dbe6..4f3669a2b9 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -13,7 +13,7 @@ open CErrors
 open Util
 open Names
 open Nameops
-open Term
+open Constr
 open Termops
 open Environ
 open EConstr
@@ -1014,7 +1014,7 @@ let adjust_impossible_cases pb pred tomatch submat =
         this means that the Evd.define below may redefine an already defined
         evar. See e.g. first definition of test for bug #3388. *)
     let pred = EConstr.Unsafe.to_constr pred in
-    begin match kind_of_term pred with
+    begin match Constr.kind pred with
     | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) == Evar_kinds.ImpossibleCase ->
         if not (Evd.is_defined !(pb.evdref) evk) then begin
 	  let evd, default = use_unit_judge !(pb.evdref) in
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 327ee00150..3a139b7b03 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Evd
 open Environ
 open EConstr
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 19d61a64db..3a2eac7e79 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -8,7 +8,7 @@
 
 open Util
 open Names
-open Term
+open Constr
 open Vars
 open CClosure
 open Esubst
@@ -211,7 +211,7 @@ and reify_value = function (* reduction under binders *)
     t
       (* map_constr_with_binders subs_lift (cbv_norm_term) env t *)
   | LAM (n,ctxt,b,env) ->
-      List.fold_left (fun c (n,t)  -> Term.mkLambda (n, t, c)) b ctxt
+      List.fold_left (fun c (n,t)  -> mkLambda (n, t, c)) b ctxt
   | FIXP ((lij,(names,lty,bds)),env,args) ->
       mkApp
         (mkFix (lij,
@@ -240,7 +240,7 @@ and reify_value = function (* reduction under binders *)
 
 let rec norm_head info env t stack =
   (* no reduction under binders *)
-  match kind_of_term t with
+  match kind t with
   (* stack grows (remove casts) *)
   | App (head,args) -> (* Applied terms are normalized immediately;
                         they could be computed when getting out of the stack *)
@@ -294,7 +294,7 @@ let rec norm_head info env t stack =
 
   (* non-neutral cases *)
   | Lambda _ ->
-      let ctxt,b = decompose_lam t in
+      let ctxt,b = Term.decompose_lam t in
       (LAM(List.length ctxt, List.rev ctxt,b,env), stack)
   | Fix fix -> (FIXP(fix,env,[||]), stack)
   | CoFix cofix -> (COFIXP(cofix,env,[||]), stack)
@@ -411,12 +411,12 @@ and cbv_norm_value info = function (* reduction under binders *)
   | STACK (n,v,stk) ->
       lift n (apply_stack info (cbv_norm_value info v) stk)
   | CBN(t,env) ->
-      map_constr_with_binders subs_lift (cbv_norm_term info) env t
+      Constr.map_with_binders subs_lift (cbv_norm_term info) env t
   | LAM (n,ctxt,b,env) ->
       let nctxt =
         List.map_i (fun i (x,ty) ->
           (x,cbv_norm_term info (subs_liftn i env) ty)) 0 ctxt in
-      compose_lam (List.rev nctxt) (cbv_norm_term info (subs_liftn n env) b)
+      Term.compose_lam (List.rev nctxt) (cbv_norm_term info (subs_liftn n env) b)
   | FIXP ((lij,(names,lty,bds)),env,args) ->
       mkApp
         (mkFix (lij,
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 3ee7bebf08..5f9609a5c5 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -24,7 +24,7 @@ val cbv_norm         : cbv_infos -> constr -> constr
 (***********************************************************************
   i This is for cbv debug *)
 
-open Term
+open Constr
 
 type cbv_value =
   | VAL of int * constr
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index fe969f9e59..c36630f5d3 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -10,12 +10,12 @@ open CErrors
 open Util
 open Pp
 open Names
+open Constr
 open Libnames
 open Globnames
 open Nametab
 open Environ
 open Libobject
-open Term
 open Mod_subst
 
 (* usage qque peu general: utilise aussi dans record *)
@@ -43,7 +43,7 @@ type coe_info_typ = {
   coe_value : constr;
   coe_type : types;
   coe_local : bool;
-  coe_context : Univ.universe_context_set;
+  coe_context : Univ.ContextSet.t;
   coe_is_identity : bool;
   coe_is_projection : bool;
   coe_param : int }
diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli
index 34c62043ef..780ccc23d1 100644
--- a/pretyping/constr_matching.mli
+++ b/pretyping/constr_matching.mli
@@ -9,7 +9,7 @@
 (** This module implements pattern-matching on terms *)
 
 open Names
-open Term
+open Constr
 open EConstr
 open Environ
 open Pattern
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index c02fc5aafd..0d1e401d98 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -554,7 +554,7 @@ and detype_r d flags avoid env sigma t =
           let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel sigma c && Int.Set.mem (destRel sigma c) rels || isVar sigma c && (Id.Set.mem (destVar sigma c) fvs)))) (Evd.find sigma evk) cl in
           id,l
         with Not_found ->
-          Id.of_string ("X" ^ string_of_int (Evar.repr evk)), 
+          Id.of_string ("X" ^ string_of_int (Evar.repr evk)),
           (Array.map_to_list (fun c -> (Id.of_string "__",c)) cl)
       in
         GEvar (id,
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index f03bde68ec..cb1c0d8d4b 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open Environ
 open EConstr
 open Glob_term
@@ -40,7 +39,7 @@ val detype_names : bool -> Id.Set.t -> names_context -> env -> evar_map -> const
 
 val detype : 'a delay -> ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> constr -> 'a glob_constr_g
 
-val detype_sort : evar_map -> sorts -> glob_sort
+val detype_sort : evar_map -> Sorts.t -> glob_sort
 
 val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> (names_context * env) -> 
   evar_map -> rel_context -> 'a glob_decl_g list
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 45fe2b2d8a..681eb17d3c 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -10,6 +10,7 @@ open CErrors
 open Util
 open Names
 open Term
+open Constr
 open Termops
 open Environ
 open EConstr
@@ -49,7 +50,7 @@ let _ = Goptions.declare_bool_option {
 let impossible_default_case () =
   let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in
   let (_, u) = Term.destConst c in
-  Some (c, Term.mkConstU (Coqlib.type_of_id, u), ctx)
+  Some (c, Constr.mkConstU (Coqlib.type_of_id, u), ctx)
 
 let coq_unit_judge =
   let open Environ in
@@ -175,7 +176,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
       | Sort s ->
         let s = ESorts.kind sigma s in
 	lookup_canonical_conversion
-	  (proji, Sort_cs (family_of_sort s)),[]
+	  (proji, Sort_cs (Sorts.family s)),[]
       | Proj (p, c) ->
         let c2 = Globnames.ConstRef (Projection.constant p) in
         let c = Retyping.expand_projection env sigma p c [] in
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index c30d1d26bf..d793b06d3d 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -47,7 +47,7 @@ val check_problems_are_solved : env -> evar_map -> unit
 
 val check_conv_record : env -> evar_map -> 
   state -> state ->
-  Univ.universe_context_set * (constr * constr) 
+  Univ.ContextSet.t * (constr * constr) 
   * constr * constr list * (constr Stack.t * constr Stack.t) *
     (constr Stack.t * constr Stack.t) *
     (constr Stack.t * constr Stack.t) * constr *
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 5f12f360b3..18dbbea1bd 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -10,6 +10,7 @@ open Util
 open Pp
 open Names
 open Term
+open Constr
 open Termops
 open EConstr
 open Vars
@@ -82,7 +83,7 @@ let define_pure_evar_as_product evd evk =
     let newenv = push_named (LocalAssum (id, dom)) evenv in
     let src = evar_source evk evd1 in
     let filter = Filter.extend 1 (evar_filter evi) in
-      if is_prop_sort (ESorts.kind evd1 s) then
+      if Sorts.is_prop (ESorts.kind evd1 s) then
        (* Impredicative product, conclusion must fall in [Prop]. *)
         new_evar newenv evd1 concl ~src ~filter
       else
diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli
index 5477c5c99d..869e3adbf9 100644
--- a/pretyping/evardefine.mli
+++ b/pretyping/evardefine.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Evd
 open Environ
@@ -39,7 +38,7 @@ val lift_tycon : int -> type_constraint -> type_constraint
 
 val define_evar_as_product : evar_map -> existential -> evar_map * types
 val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types
-val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts
+val define_evar_as_sort : env -> evar_map -> existential -> evar_map * Sorts.t
 
 (** {6 debug pretty-printer:} *)
 
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b906c3b597..fba1542912 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -10,6 +10,7 @@ open Util
 open CErrors
 open Names
 open Term
+open Constr
 open Environ
 open Termops
 open Evd
@@ -1391,7 +1392,7 @@ let occur_evar_upto_types sigma n c =
   let c = EConstr.Unsafe.to_constr c in
   let seen = ref Evar.Set.empty in
   (** FIXME: Is that supposed to be evar-insensitive? *)
-  let rec occur_rec c = match kind_of_term c with
+  let rec occur_rec c = match Constr.kind c with
     | Evar (sp,_) when Evar.equal sp n -> raise Occur
     | Evar (sp,args as e) ->
        if Evar.Set.mem sp !seen then
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 811b4dc18f..e5d288b5c3 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
+open Constr
 open EConstr
 open Evd
 open Environ
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 0cb5974e80..48b33e708c 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -18,6 +18,7 @@ open Libnames
 open Globnames
 open Nameops
 open Term
+open Constr
 open Vars
 open Namegen
 open Declarations
@@ -33,7 +34,7 @@ type dep_flag = bool
 
 (* Errors related to recursors building *)
 type recursion_scheme_error =
-  | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive
+  | NotAllowedCaseAnalysis of (*isrec:*) bool * Sorts.t * pinductive
   | NotMutualInScheme of inductive * inductive
   | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive
 
@@ -168,7 +169,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
       let p',largs = whd_allnolet_stack env sigma (EConstr.of_constr p) in
       let p' = EConstr.Unsafe.to_constr p' in
       let largs = List.map EConstr.Unsafe.to_constr largs in
-      match kind_of_term p' with
+      match kind p' with
 	| Prod (n,t,c) ->
 	    let d = LocalAssum (n,t) in
 	    make_prod env (n,t,prec (push_rel d env) (i+1) (d::sign) c)
@@ -186,13 +187,13 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
       	| _ ->
 	   let t' = whd_all env sigma (EConstr.of_constr p) in
 	   let t' = EConstr.Unsafe.to_constr t' in
-	   if Term.eq_constr p' t' then assert false
+	   if Constr.equal p' t' then assert false
 	   else prec env i sign t'
     in
     prec env 0 []
   in
   let rec process_constr env i c recargs nhyps li =
-    if nhyps > 0 then match kind_of_term c with
+    if nhyps > 0 then match kind c with
       | Prod (n,t,c_0) ->
           let (optionpos,rest) =
 	    match recargs with
@@ -247,7 +248,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
       let p',largs = whd_allnolet_stack env sigma (EConstr.of_constr p) in
       let p' = EConstr.Unsafe.to_constr p' in
       let largs = List.map EConstr.Unsafe.to_constr largs in
-      match kind_of_term p' with
+      match kind p' with
 	| Prod (n,t,c) ->
 	    let d = LocalAssum (n,t) in
 	    mkLambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c)
@@ -261,7 +262,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
      	| _ ->
 	   let t' = whd_all env sigma (EConstr.of_constr p) in
 	   let t' = EConstr.Unsafe.to_constr t' in
-	     if Term.eq_constr t' p' then assert false
+	     if Constr.equal t' p' then assert false
 	     else prec env i hyps t'
     in
     prec env 0 []
@@ -505,7 +506,7 @@ let build_case_analysis_scheme_default env sigma pity kind =
    [rec] by [s] *)
 
 let change_sort_arity sort =
-  let rec drec a = match kind_of_term a with
+  let rec drec a = match kind a with
     | Cast (c,_,_) -> drec c
     | Prod (n,t,c) -> let s, c' = drec c in s, mkProd (n, t, c')
     | LetIn (n,b,t,c) -> let s, c' = drec c in s, mkLetIn (n,b,t,c')
@@ -519,7 +520,7 @@ let change_sort_arity sort =
 let weaken_sort_scheme env evd set sort npars term ty =
   let evdref = ref evd in
   let rec drec np elim =
-    match kind_of_term elim with
+    match kind elim with
       | Prod (n,t,c) ->
 	  if Int.equal np 0 then
             let osort, t' = change_sort_arity sort t in
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index 2825c4d83a..a9838cffe5 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -7,14 +7,14 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Environ
 open Evd
 
 (** Errors related to recursors building *)
 
 type recursion_scheme_error =
-  | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive
+  | NotAllowedCaseAnalysis of (*isrec:*) bool * Sorts.t * pinductive
   | NotMutualInScheme of inductive * inductive
   | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive
 
@@ -27,25 +27,25 @@ type dep_flag = bool
 (** Build a case analysis elimination scheme in some sort family *)
 
 val build_case_analysis_scheme : env -> Evd.evar_map -> pinductive ->
-      dep_flag -> sorts_family -> evar_map * Constr.t
+      dep_flag -> Sorts.family -> evar_map * Constr.t
 
 (** Build a dependent case elimination predicate unless type is in Prop
    or is a recursive record with primitive projections. *)
 
 val build_case_analysis_scheme_default : env -> evar_map -> pinductive ->
-      sorts_family -> evar_map * Constr.t
+      Sorts.family -> evar_map * Constr.t
 
 (** Builds a recursive induction scheme (Peano-induction style) in the same
    sort family as the inductive family; it is dependent if not in Prop
    or a recursive record with primitive projections.  *)
 
 val build_induction_scheme : env -> evar_map -> pinductive ->
-      dep_flag -> sorts_family -> evar_map * constr
+      dep_flag -> Sorts.family -> evar_map * constr
 
 (** Builds mutual (recursive) induction schemes *)
 
 val build_mutual_induction_scheme :
-  env -> evar_map -> (pinductive * dep_flag * sorts_family) list -> evar_map * constr list
+  env -> evar_map -> (pinductive * dep_flag * Sorts.family) list -> evar_map * constr list
 
 (** Scheme combinators *)
 
@@ -54,13 +54,13 @@ val build_mutual_induction_scheme :
    scheme quantified on sort [s]. [set] asks for [s] be declared equal to [i],
   otherwise just less or equal to [i]. *)
 
-val weaken_sort_scheme : env -> evar_map -> bool -> sorts -> int -> constr -> types -> 
+val weaken_sort_scheme : env -> evar_map -> bool -> Sorts.t -> int -> constr -> types ->
   evar_map * types * constr
 
 (** Recursor names utilities *)
 
-val lookup_eliminator : inductive -> sorts_family -> Globnames.global_reference
-val elimination_suffix : sorts_family -> string
-val make_elimination_ident : Id.t -> sorts_family -> Id.t
+val lookup_eliminator : inductive -> Sorts.family -> Globnames.global_reference
+val elimination_suffix : Sorts.family -> string
+val make_elimination_ident : Id.t -> Sorts.family -> Id.t
 
 val case_suffix : string
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index b31ee03d8c..34df7d3d72 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -11,6 +11,7 @@ open Util
 open Names
 open Univ
 open Term
+open Constr
 open Vars
 open Termops
 open Declarations
@@ -643,7 +644,7 @@ let type_of_projection_knowing_arg env sigma p c ty =
    syntactic conditions *)
 
 let control_only_guard env c =
-  let check_fix_cofix e c = match kind_of_term c with
+  let check_fix_cofix e c = match kind c with
     | CoFix (_,(_,_,_) as cofix) ->
       Inductive.check_cofix e cofix
     | Fix (_,(_,_,_) as fix) ->
@@ -659,7 +660,7 @@ let control_only_guard env c =
 (* inference of subtyping condition for inductive types *)
 
 let infer_inductive_subtyping_arity_constructor
-    (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity (params : Context.Rel.t) =
+    (env, evd, csts) (subst : constr -> constr) (arcn : types) is_arity (params : Context.Rel.t) =
   let numchecked = ref 0 in
   let numparams = Context.Rel.nhyps params in
   let update_contexts (env, evd, csts) csts' =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 65d5161df0..febe99b0bc 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Declarations
 open Environ
 open Evd
@@ -120,7 +120,7 @@ val constructor_nrealdecls_env : env -> constructor -> int
 val constructor_has_local_defs : constructor -> bool
 val inductive_has_local_defs : inductive -> bool
 
-val allowed_sorts : env -> inductive -> sorts_family list
+val allowed_sorts : env -> inductive -> Sorts.family list
 
 (** (Co)Inductive records with primitive projections do not have eta-conversion,
     hence no dependent elimination. *)
@@ -152,12 +152,12 @@ val get_projections  : env -> inductive_family -> Constant.t array option
 (** [get_arity] returns the arity of the inductive family instantiated
     with the parameters; if recursively non-uniform parameters are not
     part of the inductive family, they appears in the arity *)
-val get_arity        : env -> inductive_family -> Context.Rel.t * sorts_family
+val get_arity        : env -> inductive_family -> Context.Rel.t * Sorts.family
 
 val build_dependent_constructor : constructor_summary -> constr
 val build_dependent_inductive   : env -> inductive_family -> constr
 val make_arity_signature : env -> evar_map -> bool -> inductive_family -> EConstr.rel_context
-val make_arity : env -> evar_map -> bool -> inductive_family -> sorts -> EConstr.types
+val make_arity : env -> evar_map -> bool -> inductive_family -> Sorts.t -> EConstr.types
 val build_branch_type : env -> evar_map -> bool -> constr -> constructor_summary -> types
 
 (** Raise [Not_found] if not given a valid inductive type *)
@@ -172,7 +172,7 @@ val find_coinductive : env -> evar_map -> EConstr.types -> (inductive * EConstr.
 
 (** Builds the case predicate arity (dependent or not) *)
 val arity_of_case_predicate :
-  env -> inductive_family -> bool -> sorts -> types
+  env -> inductive_family -> bool -> Sorts.t -> types
 
 val type_case_branches_with_names :
   env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> types array * types
@@ -203,8 +203,8 @@ val control_only_guard : env -> types -> unit
 (* inference of subtyping condition for inductive types *)
 (* for debugging purposes only to be removed *)
 val infer_inductive_subtyping_arity_constructor : Environ.env * Evd.evar_map * Univ.Constraint.t ->
-(Term.constr -> Term.constr) ->
-Term.types -> bool -> Context.Rel.t -> Environ.env * Evd.evar_map * Univ.Constraint.t
+(constr -> constr) ->
+types -> bool -> Context.Rel.t -> Environ.env * Evd.evar_map * Univ.Constraint.t
 
 val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry ->
   Entries.mutual_inductive_entry
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index fe134f5126..dafe8cb269 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 open CErrors
 open Term
+open Constr
 open Vars
 open Environ
 open Reduction
@@ -98,7 +99,7 @@ let app_type env c =
  
 let find_rectype_a env c =
   let (t, l) = app_type env c in
-  match kind_of_term t with
+  match kind t with
   | Ind ind -> (ind, l)
   | _ -> raise Not_found
 
@@ -131,7 +132,7 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
 
 let construct_of_constr const env tag typ =
   let t, l = app_type env typ in
-  match kind_of_term t with
+  match kind t with
   | Ind (ind,u) -> 
       construct_of_constr_notnative const env tag ind u l
   | _ -> assert false
@@ -360,7 +361,7 @@ and nf_atom_type env sigma atom =
 
 
 and  nf_predicate env sigma ind mip params v pT =
-  match kind_of_value v, kind_of_term pT with
+  match kind_of_value v, kind pT with
   | Vfun f, Prod _ ->
       let k = nb_rel env in
       let vb = f (mk_rel_accu k) in
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index fd76a9473f..ee79b54744 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -12,6 +12,7 @@ open Names
 open Globnames
 open Nameops
 open Term
+open Constr
 open Vars
 open Glob_term
 open Pp
@@ -75,8 +76,8 @@ and cofixpoint_eq (i1, r1) (i2, r2) =
 
 and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) =
   Array.equal Name.equal n1 n2 &&
-  Array.equal Term.eq_constr c1 c2 &&
-  Array.equal Term.eq_constr r1 r2
+  Array.equal Constr.equal c1 c2 &&
+  Array.equal Constr.equal r1 r2
 
 let rec occur_meta_pattern = function
   | PApp (f,args) ->
@@ -149,7 +150,7 @@ let head_of_constr_reference sigma c = match EConstr.kind sigma c with
 let pattern_of_constr env sigma t =
   let rec pattern_of_constr env t =
   let open Context.Rel.Declaration in
-  match kind_of_term t with
+  match kind t with
     | Rel n  -> PRel n
     | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n)))
     | Var id -> PVar id
@@ -165,7 +166,7 @@ let pattern_of_constr env sigma t =
 				  pattern_of_constr (push_rel (LocalAssum (na, c)) env) b)
     | App (f,a) ->
         (match
-          match kind_of_term f with
+          match kind f with
           | Evar (evk,args) ->
             (match snd (Evd.evar_source evk sigma) with
               Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar id) -> Some id
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 54b477bed9..ce478ac202 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Environ
 open EConstr
 open Type_errors
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 124fa6e06c..dab376ef07 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Environ
 open EConstr
 open Type_errors
@@ -99,8 +99,8 @@ val error_ill_typed_rec_body :
 
 val error_elim_arity :
   ?loc:Loc.t -> env -> Evd.evar_map ->
-      pinductive -> sorts_family list -> constr ->
-      unsafe_judgment -> (sorts_family * sorts_family * arity_error) option -> 'b
+      pinductive -> Sorts.family list -> constr ->
+      unsafe_judgment -> (Sorts.family * Sorts.family * arity_error) option -> 'b
 
 val error_not_a_type :
   ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 6537d1ecf7..eb2b435bf6 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -12,7 +12,7 @@
    into elementary ones, insertion of coercions and resolution of
    implicit arguments. *)
 
-open Term
+open Constr
 open Environ
 open Evd
 open EConstr
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 4f4e49d821..cb24ca804d 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -19,7 +19,7 @@ open Pp
 open Names
 open Globnames
 open Nametab
-open Term
+open Constr
 open Libobject
 open Mod_subst
 open Reductionops
@@ -144,7 +144,7 @@ type obj_typ = {
 type cs_pattern =
     Const_cs of global_reference
   | Prod_cs
-  | Sort_cs of sorts_family
+  | Sort_cs of Sorts.family
   | Default_cs
 
 let eq_cs_pattern p1 p2 = match p1, p2 with
@@ -172,7 +172,7 @@ let keep_true_projections projs kinds =
   List.map_filter filter (List.combine projs kinds)
 
 let cs_pattern_of_constr env t =
-  match kind_of_term t with
+  match kind t with
       App (f,vargs) ->
 	begin
 	  try Const_cs (global_of_constr f) , None, Array.to_list vargs
@@ -184,7 +184,7 @@ let cs_pattern_of_constr env t =
       let { Environ.uj_type = ty } = Typeops.infer env c in
       let _, params = Inductive.find_rectype env ty in
       Const_cs (ConstRef (Projection.constant p)), None, params @ [c]
-    | Sort s -> Sort_cs (family_of_sort s), None, []
+    | Sort s -> Sort_cs (Sorts.family s), None, []
     | _ ->
 	begin
 	  try Const_cs (global_of_constr t) , None, []
@@ -213,7 +213,7 @@ let compute_canonical_projections warn (con,ind) =
   let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
   let t = EConstr.Unsafe.to_constr t in
   let lt = List.rev_map snd sign in
-  let args = snd (decompose_app t) in
+  let args = snd (Term.decompose_app t) in
   let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } =
     lookup_structure ind in
   let params, projs = List.chop p args in
@@ -311,10 +311,10 @@ let check_and_decompose_canonical_structure ref =
     | None -> error_not_structure ref in
   let body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in
   let body = EConstr.Unsafe.to_constr body in
-  let f,args = match kind_of_term body with
+  let f,args = match kind body with
     | App (f,args) -> f,args
     | _ -> error_not_structure ref in
-  let indsp = match kind_of_term f with
+  let indsp = match kind f with
     | Construct ((indsp,1),u) -> indsp
     | _ -> error_not_structure ref in
   let s = try lookup_structure indsp with Not_found -> error_not_structure ref in
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 0666231643..f15418577d 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Globnames
 
 (** Operations concerning records and canonical structures *)
@@ -52,7 +52,7 @@ val find_projection : global_reference -> struc_typ
 type cs_pattern =
     Const_cs of global_reference
   | Prod_cs
-  | Sort_cs of sorts_family
+  | Sort_cs of Sorts.family
   | Default_cs
 
 type obj_typ = {
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 32c993224e..04374c88b4 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -9,7 +9,7 @@
 open CErrors
 open Util
 open Names
-open Term
+open Constr
 open Termops
 open Univ
 open Evd
@@ -339,7 +339,7 @@ struct
 
   type 'a member =
   | App of 'a app_node
-  | Case of Term.case_info * 'a * 'a array * Cst_stack.t
+  | Case of case_info * 'a * 'a array * Cst_stack.t
   | Proj of int * int * projection * Cst_stack.t
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
   | Cst of cst_member * int * int list * 'a t * Cst_stack.t
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 950fcdee44..db0c29aeff 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open EConstr
 open Univ
 open Evd
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 56f8b33e01..5dd6879d39 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -10,6 +10,7 @@ open Pp
 open CErrors
 open Util
 open Term
+open Constr
 open Inductive
 open Inductiveops
 open Names
@@ -146,7 +147,7 @@ let retype ?(polyprop=true) sigma =
     | Cast (c,_, s) when isSort sigma s -> destSort sigma s
     | Sort s ->
       begin match ESorts.kind sigma s with
-      | Prop _ -> type1_sort
+      | Prop _ -> Sorts.type1
       | Type u -> Type (Univ.super u)
       end
     | Prod (name,t,c2) ->
@@ -167,7 +168,7 @@ let retype ?(polyprop=true) sigma =
 
   and sort_family_of env t =
     match EConstr.kind sigma t with
-    | Cast (c,_, s) when isSort sigma s -> family_of_sort (destSort sigma s)
+    | Cast (c,_, s) when isSort sigma s -> Sorts.family (destSort sigma s)
     | Sort _ -> InType
     | Prod (name,t,c2) ->
 	let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in
@@ -175,12 +176,12 @@ let retype ?(polyprop=true) sigma =
 	   s2 == InSet && sort_family_of env t == InType then InType else s2
     | App(f,args) when is_template_polymorphic env sigma f ->
 	let t = type_of_global_reference_knowing_parameters env f args in
-        family_of_sort (sort_of_atomic_type env sigma t args)
+        Sorts.family (sort_of_atomic_type env sigma t args)
     | App(f,args) ->
-	family_of_sort (sort_of_atomic_type env sigma (type_of env f) args)
+	Sorts.family (sort_of_atomic_type env sigma (type_of env f) args)
     | Lambda _ | Fix _ | Construct _ -> retype_error NotAType
     | _ -> 
-      family_of_sort (decomp_sort env sigma (type_of env t))
+      Sorts.family (decomp_sort env sigma (type_of env t))
 
   and type_of_global_reference_knowing_parameters env c args =
     let argtyps =
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index ed3a9d0f96..af86df499c 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open Evd
 open Environ
 open EConstr
@@ -30,10 +29,10 @@ val get_type_of :
   ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> types
 
 val get_sort_of :
-  ?polyprop:bool -> env -> evar_map -> types -> sorts
+  ?polyprop:bool -> env -> evar_map -> types -> Sorts.t
 
 val get_sort_family_of :
-  ?polyprop:bool -> env -> evar_map -> types -> sorts_family
+  ?polyprop:bool -> env -> evar_map -> types -> Sorts.family
 
 (** Makes an unsafe judgment from a constr *)
 val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment
@@ -44,7 +43,7 @@ val type_of_global_reference_knowing_parameters : env -> evar_map -> constr ->
 val type_of_global_reference_knowing_conclusion :
   env -> evar_map -> constr -> types -> evar_map * types
 
-val sorts_of_context : env -> evar_map -> rel_context -> sorts list
+val sorts_of_context : env -> evar_map -> rel_context -> Sorts.t list
 
 val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 1e06e9f8c5..d55b286fb4 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -11,6 +11,7 @@ open Names
 open Globnames
 open Decl_kinds
 open Term
+open Constr
 open Vars
 open Evd
 open Util
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 20fbbb5a07..062d5cf356 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -8,7 +8,7 @@
 
 open Names
 open Globnames
-open Term
+open Constr
 open Evd
 open Environ
 
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 1f35fa19aa..43066c8099 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -160,7 +160,7 @@ let check_type_fixpoint ?loc env evdref lna lar vdefj =
 (* FIXME: might depend on the level of actual parameters!*)
 let check_allowed_sort env sigma ind c p =
   let pj = Retyping.get_judgment_of env sigma p in
-  let ksort = family_of_sort (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in
+  let ksort = Sorts.family (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in
   let specif = Global.lookup_inductive (fst ind) in
   let sorts = elim_sorts specif in
   if not (List.exists ((==) ksort) sorts) then
@@ -195,11 +195,11 @@ let check_cofix env sigma pcofix =
 
 let judge_of_prop =
   { uj_val = EConstr.mkProp;
-    uj_type = EConstr.mkSort type1_sort }
+    uj_type = EConstr.mkSort Sorts.type1 }
 
 let judge_of_set =
   { uj_val = EConstr.mkSet;
-    uj_type = EConstr.mkSort type1_sort }
+    uj_type = EConstr.mkSort Sorts.type1 }
 
 let judge_of_prop_contents = function
   | Null -> judge_of_prop
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 1e20788268..9f084ae8df 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Environ
 open EConstr
 open Evd
@@ -26,7 +26,7 @@ val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
 val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types
 
 (** Typecheck a type and return its sort *)
-val e_sort_of : env -> evar_map ref -> types -> sorts
+val e_sort_of : env -> evar_map ref -> types -> Sorts.t
 
 (** Typecheck a term has a given type (assuming the type is OK) *)
 val e_check   : env -> evar_map ref -> constr -> types -> unit
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index c149aaaaa9..5eb6b780ad 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -12,7 +12,7 @@ open CErrors
 open Pp
 open Util
 open Names
-open Term
+open Constr
 open Termops
 open Environ
 open EConstr
@@ -68,10 +68,10 @@ let _ = Goptions.declare_bool_option {
 
 let unsafe_occur_meta_or_existential c =
   let c = EConstr.Unsafe.to_constr c in
-  let rec occrec c = match kind_of_term c with
+  let rec occrec c = match Constr.kind c with
     | Evar _ -> raise Occur
     | Meta _ -> raise Occur
-    | _ -> iter_constr occrec c
+    | _ -> Constr.iter occrec c
   in try occrec c; false with Occur -> true
 
 
@@ -79,7 +79,7 @@ let occur_meta_or_undefined_evar evd c =
   (** This is performance-critical. Using the evar-insensitive API changes the
       resulting heuristic. *)
   let c = EConstr.Unsafe.to_constr c in
-  let rec occrec c = match kind_of_term c with
+  let rec occrec c = match Constr.kind c with
     | Meta _ -> raise Occur
     | Evar (ev,args) ->
         (match evar_body (Evd.find evd ev) with
@@ -613,7 +613,7 @@ let subst_defined_metas_evars sigma (bl,el) c =
   (** This seems to be performance-critical, and using the evar-insensitive
       primitives blow up the time passed in this function. *)
   let c = EConstr.Unsafe.to_constr c in
-  let rec substrec c = match kind_of_term c with
+  let rec substrec c = match Constr.kind c with
     | Meta i ->
       let select (j,_,_) = Int.equal i j in
       substrec (EConstr.Unsafe.to_constr (pi2 (List.find select bl)))
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index fce17d5641..085e8c5b8b 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
+open Constr
 open EConstr
 open Environ
 open Evd
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 66cc42cb61..b5b8987e33 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -10,6 +10,7 @@ open Util
 open Names
 open Declarations
 open Term
+open Constr
 open Vars
 open Environ
 open Inductive
@@ -51,7 +52,7 @@ let invert_tag cst tag reloc_tbl =
 
 let find_rectype_a env c =
   let (t, l) = decompose_appvect (whd_all env c) in
-  match kind_of_term t with
+  match kind t with
   | Ind ind -> (ind, l)
   | _ -> assert false
 
@@ -262,7 +263,7 @@ and nf_stk ?from:(from=0) env sigma c t stk  =
      nf_stk env sigma (mkProj(p',c)) ty stk
 
 and nf_predicate env sigma ind mip params v pT =
-  match whd_val v, kind_of_term pT with
+  match whd_val v, kind pT with
   | Vfun f, Prod _ ->
       let k = nb_rel env in
       let vb = body_of_vfun k f in