[api] Deprecate Term destructors, move to Constr

We mirror the structure of EConstr and move the destructors from `Term`
to `Constr`.

This is a step towards having a single module for `Constr`.

40 files changed, 571 insertions, 252 deletions

diff --git a/API/API.mli b/API/API.mli
index 991dca748..7eda207be 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -482,6 +482,7 @@ sig
 
   type family = InProp | InSet | InType
   val family : t -> family
+  val univ_of_sort : t -> Univ.Universe.t
 end
 
 module Evar :
@@ -502,6 +503,7 @@ end
 
 module Constr :
 sig
+
   open Names
 
   type t
@@ -579,13 +581,13 @@ sig
   val kind : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term
   val of_kind : (constr, types, Sorts.t, Univ.Instance.t) kind_of_term -> constr
 
-val map_with_binders :
-  ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
-val map : (constr -> constr) -> constr -> constr
+  val map_with_binders :
+    ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
+  val map : (constr -> constr) -> constr -> constr
 
-val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a
-val iter : (constr -> unit) -> constr -> unit
-val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool
+  val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a
+  val iter : (constr -> unit) -> constr -> unit
+  val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool
 
   val equal : t -> t -> bool
   val eq_constr_nounivs : t -> t -> bool
@@ -627,6 +629,109 @@ val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool
 
   val mkCase : case_info * t * t * t array -> t
 
+  (** {6 Simple case analysis} *)
+  val isRel  : constr -> bool
+  val isRelN : int -> constr -> bool
+  val isVar  : constr -> bool
+  val isVarId : Id.t -> constr -> bool
+  val isInd  : constr -> bool
+  val isEvar : constr -> bool
+  val isMeta : constr -> bool
+  val isEvar_or_Meta : constr -> bool
+  val isSort : constr -> bool
+  val isCast : constr -> bool
+  val isApp : constr -> bool
+  val isLambda : constr -> bool
+  val isLetIn : constr -> bool
+  val isProd : constr -> bool
+  val isConst : constr -> bool
+  val isConstruct : constr -> bool
+  val isFix : constr -> bool
+  val isCoFix : constr -> bool
+  val isCase : constr -> bool
+  val isProj : constr -> bool
+
+  val is_Prop : constr -> bool
+  val is_Set  : constr -> bool
+  val isprop : constr -> bool
+  val is_Type : constr -> bool
+  val iskind : constr -> bool
+  val is_small : Sorts.t -> bool
+
+  (** {6 Term destructors } *)
+  (** Destructor operations are partial functions and
+      @raise DestKO if the term has not the expected form. *)
+
+  exception DestKO
+
+  (** Destructs a de Bruijn index *)
+  val destRel : constr -> int
+
+  (** Destructs an existential variable *)
+  val destMeta : constr -> metavariable
+
+  (** Destructs a variable *)
+  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.t
+
+  (** Destructs a casted term *)
+  val destCast : constr -> constr * cast_kind * constr
+
+  (** Destructs the product {% $ %}(x:t_1)t_2{% $ %} *)
+  val destProd : types -> Name.t * types * types
+
+  (** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *)
+  val destLambda : constr -> Name.t * types * constr
+
+  (** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *)
+  val destLetIn : constr -> Name.t * constr * types * constr
+
+  (** Destructs an application *)
+  val destApp : constr -> constr * constr array
+
+  (** Decompose any term as an applicative term; the list of args can be empty *)
+  val decompose_app : constr -> constr * constr list
+
+  (** Same as [decompose_app], but returns an array. *)
+  val decompose_appvect : constr -> constr * constr array
+
+  (** Destructs a constant *)
+  val destConst : constr -> Constant.t puniverses
+
+  (** Destructs an existential variable *)
+  val destEvar : constr -> existential
+
+  (** Destructs a (co)inductive type *)
+  val destInd : constr -> inductive puniverses
+
+  (** Destructs a constructor *)
+  val destConstruct : constr -> constructor puniverses
+
+  (** Destructs a [match c as x in I args return P with ... |
+      Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args
+      return P in t1], or [if c then t1 else t2])
+      @return [(info,c,fun args x => P,[|...|fun yij => ti| ...|])]
+      where [info] is pretty-printing information *)
+  val destCase : constr -> case_info * constr * constr * constr array
+
+  (** Destructs a projection *)
+  val destProj : constr -> Projection.t * constr
+
+  (** Destructs the {% $ %}i{% $ %}th function of the block
+      [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1}
+      with    f{_ 2} ctx{_ 2} = b{_ 2}
+      ...
+      with    f{_ n} ctx{_ n} = b{_ n}],
+      where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}.
+  *)
+  val destFix : constr -> fixpoint
+
+  type cofixpoint = int * rec_declaration
+  val destCoFix : constr -> cofixpoint
+
 end
 
 module Context :
@@ -1016,6 +1121,8 @@ sig
   val mkNamedProd : Names.Id.t -> types -> types -> types
 
   val decompose_app : constr -> constr * constr list
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
+
   val decompose_prod : constr -> (Names.Name.t*constr) list * constr
   val decompose_prod_n : int -> constr -> (Names.Name.t * constr) list * constr
   val decompose_prod_assum : types -> Context.Rel.t * types
@@ -1027,26 +1134,46 @@ sig
   val compose_lam : (Names.Name.t * constr) list -> constr -> constr
 
   val destSort : constr -> Sorts.t
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val destVar : constr -> Names.Id.t
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val destApp : constr -> constr * constr array
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val destProd : types -> Names.Name.t * types * types
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val destLetIn : constr -> Names.Name.t * constr * types * constr
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val destEvar : constr -> existential
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val destRel : constr -> int
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val destConst : constr -> Names.Constant.t puniverses
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val destCast : constr -> constr * cast_kind * constr
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val destLambda : constr -> Names.Name.t * types * constr
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
 
   val isRel : constr -> bool
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val isVar  : constr -> bool
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val isEvar : constr -> bool
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val isLetIn : constr -> bool
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val isLambda : constr -> bool
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val isConst : constr -> bool
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val isEvar_or_Meta : constr -> bool
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val isCast : constr -> bool
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val isMeta : constr -> bool
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val isApp : constr -> bool
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
 
   val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a
   [@@ocaml.deprecated "Alias of Constr.fold"]
@@ -1060,7 +1187,7 @@ sig
   val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
   val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
   val prod_applist : constr -> constr list -> constr
-  exception DestKO
+
   val map_constr : (constr -> constr) -> constr -> constr
   [@@ocaml.deprecated "Alias of Constr.map"]
 
@@ -1106,13 +1233,16 @@ sig
   [@@ocaml.deprecated "alias of Term.compare"]
 
   val destInd : constr -> Names.inductive puniverses
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val univ_of_sort : Sorts.t -> Univ.Universe.t
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
 
   val strip_lam : constr -> constr
   val strip_prod_assum : types -> types
 
   val decompose_lam_assum : constr -> Context.Rel.t * constr
   val destFix : constr -> fixpoint
+  [@@ocaml.deprecated "Alias for the function in [Constr]"]
 
   val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
   [@@ocaml.deprecated "Alias of Constr.compare_head."]
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index bcfbc8081..afdceae06 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -9,7 +9,6 @@
 open CErrors
 open Util
 open Names
-open Term
 open Constr
 open Context
 open Evd
@@ -55,7 +54,7 @@ struct
   type t = Sorts.t
   let make s = s
   let kind sigma = function
-  | Type u -> sort_of_univ (Evd.normalize_universe sigma u)
+  | Sorts.Type u -> Sorts.sort_of_univ (Evd.normalize_universe sigma u)
   | s -> s
   let unsafe_to_sorts s = s
 end
@@ -85,16 +84,16 @@ let rec whd_evar sigma c =
     | Some c -> whd_evar sigma c
     | None -> c
     end
-  | App (f, args) when Term.isEvar f ->
+  | App (f, args) when isEvar f ->
     (** Enforce smart constructor invariant on applications *)
-    let ev = Term.destEvar f in
+    let ev = destEvar f in
     begin match safe_evar_value sigma ev with
     | None -> c
     | Some f -> whd_evar sigma (mkApp (f, args))
     end
-  | Cast (c0, k, t) when Term.isEvar c0 ->
+  | Cast (c0, k, t) when isEvar c0 ->
     (** Enforce smart constructor invariant on casts. *)
-    let ev = Term.destEvar c0 in
+    let ev = destEvar c0 in
     begin match safe_evar_value sigma ev with
     | None -> c
     | Some c -> whd_evar sigma (mkCast (c, k, t))
@@ -115,7 +114,7 @@ let rec to_constr sigma c = match Constr.kind c with
   | Some c -> to_constr sigma c
   | None -> Constr.map (fun c -> to_constr sigma c) c
   end
-| Sort (Type u) ->
+| Sort (Sorts.Type u) ->
   let u' = Evd.normalize_universe sigma u in
   if u' == u then c else mkSort (Sorts.sort_of_univ u')
 | Const (c', u) when not (Univ.Instance.is_empty u) ->
diff --git a/engine/evd.ml b/engine/evd.ml
index 8d465384b..60bd6de2a 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -243,7 +243,7 @@ let evar_instance_array test_id info args =
     instrec filter (evar_context info) 0
 
 let make_evar_instance_array info args =
-  evar_instance_array (NamedDecl.get_id %> Term.isVarId) info args
+  evar_instance_array (NamedDecl.get_id %> isVarId) info args
 
 let instantiate_evar_array info c args =
   let inst = make_evar_instance_array info args in
@@ -707,10 +707,10 @@ let extract_all_conv_pbs evd =
   extract_conv_pbs evd (fun _ -> true)
 
 let loc_of_conv_pb evd (pbty,env,t1,t2) =
-  match kind (fst (Term.decompose_app t1)) with
+  match kind (fst (decompose_app t1)) with
   | Evar (evk1,_) -> fst (evar_source evk1 evd)
   | _ ->
-  match kind (fst (Term.decompose_app t2)) with
+  match kind (fst (decompose_app t2)) with
   | Evar (evk2,_) -> fst (evar_source evk2 evd)
   | _             -> None
 
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 598358c47..3b945c87f 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1200,7 +1200,7 @@ module V82 = struct
    { Evd.it = comb ; sigma = solution }
 
   let top_goals initial { solution=solution; } =
-    let goals = CList.map (fun (t,_) -> fst (Term.destEvar (EConstr.Unsafe.to_constr t))) initial in
+    let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in
     { Evd.it = goals ; sigma=solution; }
 
   let top_evars initial =
diff --git a/engine/univops.ml b/engine/univops.ml
index 9dc138eb8..d498b2e0d 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -6,8 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Constr
 open Univ
+open Constr
 
 let universes_of_constr c =
   let rec aux s c = 
@@ -15,7 +15,7 @@ let universes_of_constr c =
     | Const (_, u) | Ind (_, u) | Construct (_, u) ->
       LSet.fold LSet.add (Instance.levels u) s
     | Sort u when not (Sorts.is_small u) -> 
-      let u = Term.univ_of_sort u in
+      let u = Sorts.univ_of_sort u in
       LSet.fold LSet.add (Universe.levels u) s
     | _ -> Constr.fold aux s c
   in aux LSet.empty c
diff --git a/interp/impargs.ml b/interp/impargs.ml
index f70154e61..3105214d5 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -10,7 +10,6 @@ open CErrors
 open Util
 open Names
 open Globnames
-open Term
 open Constr
 open Reduction
 open Declarations
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 6fd1d0b58..22c5a2f5e 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -102,7 +102,7 @@ let declare_reserved_type idl t =
 let find_reserved_type id = Id.Map.find (root_of_id id) !reserve_table
 
 let constr_key c =
-  try RefKey (canonical_gr (global_of_constr (fst (Term.decompose_app c))))
+  try RefKey (canonical_gr (global_of_constr (fst (Constr.decompose_app c))))
   with Not_found -> Oth
 
 let revert_reserved_type t =
diff --git a/kernel/constr.ml b/kernel/constr.ml
index cec00c04b..be59f9341 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -233,7 +233,6 @@ let mkMeta  n =  Meta n
 (* Constructs a Variable named id *)
 let mkVar id = Var id
 
-
 (************************************************************************)
 (*    kind_of_term = constructions as seen by the user                 *)
 (************************************************************************)
@@ -250,6 +249,168 @@ let of_kind = function
 | Cast (c, knd, t) -> mkCast (c, knd, t)
 | k -> k
 
+(**********************************************************************)
+(*          Non primitive term destructors                            *)
+(**********************************************************************)
+
+(* Destructor operations : partial functions
+   Raise [DestKO] if the const has not the expected form *)
+
+exception DestKO
+
+let isMeta c = match kind c with Meta _ -> true | _ -> false
+
+(* Destructs a type *)
+let isSort c = match kind c with
+  | Sort _ -> true
+  | _ -> false
+
+let rec isprop c = match kind c with
+  | Sort (Sorts.Prop _) -> true
+  | Cast (c,_,_) -> isprop c
+  | _ -> false
+
+let rec is_Prop c = match kind c with
+  | Sort (Sorts.Prop Sorts.Null) -> true
+  | Cast (c,_,_) -> is_Prop c
+  | _ -> false
+
+let rec is_Set c = match kind c with
+  | Sort (Sorts.Prop Sorts.Pos) -> true
+  | Cast (c,_,_) -> is_Set c
+  | _ -> false
+
+let rec is_Type c = match kind c with
+  | Sort (Sorts.Type _) -> true
+  | Cast (c,_,_) -> is_Type c
+  | _ -> false
+
+let is_small = Sorts.is_small
+let iskind c = isprop c || is_Type c
+
+(* Tests if an evar *)
+let isEvar c = match kind c with Evar _ -> true | _ -> false
+let isEvar_or_Meta c = match kind c with
+  | Evar _ | Meta _ -> true
+  | _ -> false
+
+let isCast c = match kind c with Cast _ -> true | _ -> false
+(* Tests if a de Bruijn index *)
+let isRel c = match kind c with Rel _ -> true | _ -> false
+let isRelN n c =
+  match kind c with Rel n' -> Int.equal n n' | _ -> false
+(* Tests if a variable *)
+let isVar c = match kind c with Var _ -> true | _ -> false
+let isVarId id c = match kind c with Var id' -> Id.equal id id' | _ -> false
+(* Tests if an inductive *)
+let isInd c = match kind c with Ind _ -> true | _ -> false
+let isProd c = match kind c with | Prod _ -> true | _ -> false
+let isLambda c = match kind c with | Lambda _ -> true | _ -> false
+let isLetIn c =  match kind c with LetIn _ -> true | _ -> false
+let isApp c = match kind c with App _ -> true | _ -> false
+let isConst c = match kind c with Const _ -> true | _ -> false
+let isConstruct c = match kind c with Construct _ -> true | _ -> false
+let isCase c =  match kind c with Case _ -> true | _ -> false
+let isProj c =  match kind c with Proj _ -> true | _ -> false
+let isFix c =  match kind c with Fix _ -> true | _ -> false
+let isCoFix c =  match kind c with CoFix _ -> true | _ -> false
+
+(* Destructs a de Bruijn index *)
+let destRel c = match kind c with
+  | Rel n -> n
+  | _ -> raise DestKO
+
+(* Destructs an existential variable *)
+let destMeta c = match kind c with
+  | Meta n -> n
+  | _ -> raise DestKO
+
+(* Destructs a variable *)
+let destVar c = match kind c with
+  | Var id -> id
+  | _ -> raise DestKO
+
+let destSort c = match kind c with
+  | Sort s -> s
+  | _ -> raise DestKO
+
+(* Destructs a casted term *)
+let destCast c = match kind c with
+  | Cast (t1,k,t2) -> (t1,k,t2)
+  | _ -> raise DestKO
+
+(* Destructs the product (x:t1)t2 *)
+let destProd c = match kind c with
+  | Prod (x,t1,t2) -> (x,t1,t2)
+  | _ -> raise DestKO
+
+(* Destructs the abstraction [x:t1]t2 *)
+let destLambda c = match kind c with
+  | Lambda (x,t1,t2) -> (x,t1,t2)
+  | _ -> raise DestKO
+
+(* Destructs the let [x:=b:t1]t2 *)
+let destLetIn c = match kind c with
+  | LetIn (x,b,t1,t2) -> (x,b,t1,t2)
+  | _ -> raise DestKO
+
+(* Destructs an application *)
+let destApp c = match kind c with
+  | App (f,a) -> (f, a)
+  | _ -> raise DestKO
+
+(* Destructs a constant *)
+let destConst c = match kind c with
+  | Const kn -> kn
+  | _ -> raise DestKO
+
+(* Destructs an existential variable *)
+let destEvar c = match kind c with
+  | Evar (kn, a as r) -> r
+  | _ -> raise DestKO
+
+(* Destructs a (co)inductive type named kn *)
+let destInd c = match kind c with
+  | Ind (kn, a as r) -> r
+  | _ -> raise DestKO
+
+(* Destructs a constructor *)
+let destConstruct c = match kind c with
+  | Construct (kn, a as r) -> r
+  | _ -> raise DestKO
+
+(* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
+let destCase c = match kind c with
+  | Case (ci,p,c,v) -> (ci,p,c,v)
+  | _ -> raise DestKO
+
+let destProj c = match kind c with
+  | Proj (p, c) -> (p, c)
+  | _ -> raise DestKO
+
+let destFix c = match kind c with
+  | Fix fix -> fix
+  | _ -> raise DestKO
+
+let destCoFix c = match kind c with
+  | CoFix cofix -> cofix
+  | _ -> raise DestKO
+
+
+(******************************************************************)
+(* Flattening and unflattening of embedded applications and casts *)
+(******************************************************************)
+
+let decompose_app c =
+  match kind c with
+    | App (f,cl) -> (f, Array.to_list cl)
+    | _ -> (c,[])
+
+let decompose_appvect c =
+  match kind c with
+    | App (f,cl) -> (f, cl)
+    | _ -> (c,[||])
+
 (****************************************************************************)
 (*              Functions to recur through subterms                         *)
 (****************************************************************************)
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 474ab3884..4c5ea9e95 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -225,6 +225,110 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
 val kind : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term
 val of_kind : (constr, types, Sorts.t, Univ.Instance.t) kind_of_term -> constr
 
+(** {6 Simple case analysis} *)
+val isRel  : constr -> bool
+val isRelN : int -> constr -> bool
+val isVar  : constr -> bool
+val isVarId : Id.t -> constr -> bool
+val isInd  : constr -> bool
+val isEvar : constr -> bool
+val isMeta : constr -> bool
+val isEvar_or_Meta : constr -> bool
+val isSort : constr -> bool
+val isCast : constr -> bool
+val isApp : constr -> bool
+val isLambda : constr -> bool
+val isLetIn : constr -> bool
+val isProd : constr -> bool
+val isConst : constr -> bool
+val isConstruct : constr -> bool
+val isFix : constr -> bool
+val isCoFix : constr -> bool
+val isCase : constr -> bool
+val isProj : constr -> bool
+
+val is_Prop : constr -> bool
+val is_Set  : constr -> bool
+val isprop : constr -> bool
+val is_Type : constr -> bool
+val iskind : constr -> bool
+val is_small : Sorts.t -> bool
+
+(** {6 Term destructors } *)
+(** Destructor operations are partial functions and
+    @raise DestKO if the term has not the expected form. *)
+
+exception DestKO
+
+(** Destructs a de Bruijn index *)
+val destRel : constr -> int
+
+(** Destructs an existential variable *)
+val destMeta : constr -> metavariable
+
+(** Destructs a variable *)
+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.t
+
+(** Destructs a casted term *)
+val destCast : constr -> constr * cast_kind * constr
+
+(** Destructs the product {% $ %}(x:t_1)t_2{% $ %} *)
+val destProd : types -> Name.t * types * types
+
+(** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *)
+val destLambda : constr -> Name.t * types * constr
+
+(** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *)
+val destLetIn : constr -> Name.t * constr * types * constr
+
+(** Destructs an application *)
+val destApp : constr -> constr * constr array
+
+(** Decompose any term as an applicative term; the list of args can be empty *)
+val decompose_app : constr -> constr * constr list
+
+(** Same as [decompose_app], but returns an array. *)
+val decompose_appvect : constr -> constr * constr array
+
+(** Destructs a constant *)
+val destConst : constr -> Constant.t puniverses
+
+(** Destructs an existential variable *)
+val destEvar : constr -> existential
+
+(** Destructs a (co)inductive type *)
+val destInd : constr -> inductive puniverses
+
+(** Destructs a constructor *)
+val destConstruct : constr -> constructor puniverses
+
+(** Destructs a [match c as x in I args return P with ... |
+Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args
+return P in t1], or [if c then t1 else t2])
+@return [(info,c,fun args x => P,[|...|fun yij => ti| ...|])]
+where [info] is pretty-printing information *)
+val destCase : constr -> case_info * constr * constr * constr array
+
+(** Destructs a projection *)
+val destProj : constr -> projection * constr
+
+(** Destructs the {% $ %}i{% $ %}th function of the block
+   [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1}
+    with    f{_ 2} ctx{_ 2} = b{_ 2}
+    ...
+    with    f{_ n} ctx{_ n} = b{_ n}],
+   where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}.
+*)
+val destFix : constr -> fixpoint
+
+val destCoFix : constr -> cofixpoint
+
+(** {6 Equality} *)
+
 (** [equal a b] is true if [a] equals [b] modulo alpha, casts,
    and application grouping *)
 val equal : constr -> constr -> bool
@@ -344,7 +448,7 @@ val compare_head_gen_leq : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool)
   (constr -> constr -> bool) ->
   (constr -> constr -> bool) ->
   constr -> constr -> bool
-  
+
 (** {6 Hashconsing} *)
 
 val hash : constr -> int
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index f4e611c19..083b0ae40 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -56,7 +56,7 @@ let weaker_noccur_between env x nvars t =
    else None
 
 let is_constructor_head t =
-  Term.isRel(fst(Term.decompose_app t))
+  isRel(fst(decompose_app t))
 
 (************************************************************************)
 (* Various well-formedness check for inductive declarations            *)
@@ -135,7 +135,7 @@ let infos_and_sort env t =
       | 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 (Term.univ_of_sort varj.utj_type) in
+        let max = Universe.sup max (Sorts.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
@@ -184,7 +184,7 @@ let cumulate_arity_large_levels env sign =
      match d with
      | LocalAssum (_,t) ->
 	let tj = infer_type env t in
-	let u = Term.univ_of_sort tj.utj_type in
+        let u = Sorts.univ_of_sort tj.utj_type in
 	  (Universe.sup u lev, push_rel d env)
      | LocalDef _ ->
 	lev, push_rel d env)
@@ -351,7 +351,7 @@ let typecheck_inductive env mie =
 	| None -> clev
       in
       let full_polymorphic () = 
-	let defu = Term.univ_of_sort def_level in
+        let defu = Sorts.univ_of_sort def_level in
 	let is_natural =
 	  type_in_type env || (UGraph.check_leq (universes env') infu defu)
 	in
@@ -555,7 +555,7 @@ 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 = Term.decompose_app (whd_all env c) in
+    let x,largs = decompose_app (whd_all env c) in
       match kind x with
 	| Prod (na,b,d) ->
 	    let () = assert (List.is_empty largs) in
@@ -663,7 +663,7 @@ 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 = Term.decompose_app (whd_all env c) in
+      let x,largs = decompose_app (whd_all env c) in
 	match kind x with
 
           | Prod (na,b,d) ->
@@ -916,11 +916,11 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
 	let ar = {template_param_levels = paramlevs; template_level = lev} in
 	  TemplateArity ar, all_sorts
       | RegularArity (info,ar,defs) ->
-	let s = sort_of_univ defs in
+        let s = Sorts.sort_of_univ defs in
 	let kelim = allowed_sorts info s in
 	let ar = RegularArity 
 	  { mind_user_arity = Vars.subst_univs_level_constr substunivs ar; 
-	    mind_sort = sort_of_univ (Univ.subst_univs_level_universe substunivs defs); } in
+            mind_sort = Sorts.sort_of_univ (Univ.subst_univs_level_universe substunivs defs); } in
 	  ar, kelim in
     (* Assigning VM tags to constructors *)
     let nconst, nblock = ref 0, ref 0 in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index cb03a4d6b..0782ea820 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -29,20 +29,20 @@ let lookup_mind_specif env (kn,tyi) =
   (mib, mib.mind_packets.(tyi))
 
 let find_rectype env c =
-  let (t, l) = Term.decompose_app (whd_all env c) in
+  let (t, l) = 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) = Term.decompose_app (whd_all env c) in
+  let (t, l) = 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) = Term.decompose_app (whd_all env c) in
+  let (t, l) = 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)
@@ -354,7 +354,7 @@ let build_branches_type (ind,u) (_,mip as specif) params p =
     let typi = full_constructor_instantiate (ind,u,specif,params) cty in
     let (cstrsign,ccl) = Term.decompose_prod_assum typi in
     let nargs = Context.Rel.length cstrsign in
-    let (_,allargs) = Term.decompose_app ccl in
+    let (_,allargs) = 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
@@ -566,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' = Term.decompose_app (whd_all env s) in
-  Term.isInd i
+  let i,l' = decompose_app (whd_all env s) in
+  isInd i
 
 (* The following functions are almost duplicated from indtypes.ml, except
 that they carry here a poorer environment (containing less information). *)
@@ -621,7 +621,7 @@ 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 = Term.decompose_app (whd_all env c) in
+    let x,largs = decompose_app (whd_all env c) in
     match kind x with
     | Prod (na,b,d) ->
        assert (List.is_empty largs);
@@ -680,7 +680,7 @@ 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 = Term.decompose_app (whd_all env c) in
+      let x,largs = decompose_app (whd_all env c) in
 	match kind x with
 
           | Prod (na,b,d) ->
@@ -709,7 +709,7 @@ 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 = Term.decompose_app (whd_all env s) in
+  let i,args = decompose_app (whd_all env s) in
   match kind i with
   | Ind i ->
      begin match spec with
@@ -730,7 +730,7 @@ let restrict_spec env spec p =
 
 let rec subterm_specif renv stack t =
   (* maybe reduction is not always necessary! *)
-  let f,l = Term.decompose_app (whd_all renv.env t) in
+  let f,l = decompose_app (whd_all renv.env t) in
     match kind f with
     | Rel k -> subterm_var k renv
     | Case (ci,p,c,lbr) ->
@@ -863,7 +863,7 @@ let filter_stack_domain env ci p stack =
       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 = Term.decompose_app (whd_all env a) in
+      let ty, args = decompose_app (whd_all env a) in
       let elt = match kind ty with
       | Ind ind -> 
         let spec' = stack_element_specif elt in
@@ -894,7 +894,7 @@ 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) = Term.decompose_app (whd_betaiotazeta renv.env t) in
+      let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in
       match kind f with
         | Rel p ->
             (* Test if [p] is a fixpoint (recursive call) *)
@@ -1120,7 +1120,7 @@ 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 = Term.decompose_app (whd_all env t) in
+      let c,args = 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
diff --git a/kernel/modops.ml b/kernel/modops.ml
index b1df1a187..11e6be659 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -266,9 +266,9 @@ 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 (Term.isConst e || Term.isInd e) ->
+    | Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) ->
       Environ.register env f e
-    |_ ->
+    | _ ->
       CErrors.anomaly ~label:"Modops.add_retroknowledge"
         (Pp.str "had to import an unsupported kind of term.")
   in
diff --git a/kernel/term.ml b/kernel/term.ml
index 1c970867a..4217cfac7 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -11,6 +11,7 @@ open Pp
 open CErrors
 open Names
 open Vars
+open Constr
 
 (**********************************************************************)
 (**         Redeclaration of types from module Constr                 *)
@@ -165,167 +166,52 @@ let hcons_types = Constr.hcons
 (*          Non primitive term destructors                            *)
 (**********************************************************************)
 
-(* Destructor operations : partial functions
-   Raise [DestKO] if the const has not the expected form *)
-
-exception DestKO
-
+exception DestKO = DestKO
 (* Destructs a de Bruijn index *)
-let destRel c = match kind_of_term c with
-  | Rel n -> n
-  | _ -> raise DestKO
-
-(* Destructs an existential variable *)
-let destMeta c = match kind_of_term c with
-  | Meta n -> n
-  | _ -> raise DestKO
-
-let isMeta c = match kind_of_term c with Meta _ -> true | _ -> false
-
-(* Destructs a variable *)
-let destVar c = match kind_of_term c with
-  | Var id -> id
-  | _ -> raise DestKO
-
-(* Destructs a type *)
-let isSort c = match kind_of_term c with
-  | Sort _ -> true
-  | _ -> false
-
-let destSort c = match kind_of_term c with
-  | Sort s -> s
-  | _ -> raise DestKO
-
-let rec isprop c = match kind_of_term c with
-  | Sort (Prop _) -> true
-  | Cast (c,_,_) -> isprop c
-  | _ -> false
-
-let rec is_Prop c = match kind_of_term c with
-  | Sort (Prop Null) -> true
-  | Cast (c,_,_) -> is_Prop c
-  | _ -> false
-
-let rec is_Set c = match kind_of_term c with
-  | Sort (Prop Pos) -> true
-  | Cast (c,_,_) -> is_Set c
-  | _ -> false
-
-let rec is_Type c = match kind_of_term c with
-  | Sort (Type _) -> true
-  | Cast (c,_,_) -> is_Type c
-  | _ -> false
-
-let is_small = Sorts.is_small
-
-let iskind c = isprop c || is_Type c
-
-(* Tests if an evar *)
-let isEvar c = match kind_of_term c with Evar _ -> true | _ -> false
-
-let isEvar_or_Meta c = match kind_of_term c with
-  | Evar _ | Meta _ -> true
-  | _ -> false
-
-(* Destructs a casted term *)
-let destCast c = match kind_of_term c with
-  | Cast (t1,k,t2) -> (t1,k,t2)
-  | _ -> raise DestKO
-
-let isCast c = match kind_of_term c with Cast _ -> true | _ -> false
-
-
-(* Tests if a de Bruijn index *)
-let isRel c = match kind_of_term c with Rel _ -> true | _ -> false
-let isRelN n c =
-  match kind_of_term c with Rel n' -> Int.equal n n' | _ -> false
-
-(* Tests if a variable *)
-let isVar c = match kind_of_term c with Var _ -> true | _ -> false
-let isVarId id c =
-  match kind_of_term c with Var id' -> Id.equal id id' | _ -> false
-
-(* Tests if an inductive *)
-let isInd c = match kind_of_term c with Ind _ -> true | _ -> false
-
-(* Destructs the product (x:t1)t2 *)
-let destProd c = match kind_of_term c with
-  | Prod (x,t1,t2) -> (x,t1,t2)
-  | _ -> raise DestKO
-
-let isProd c = match kind_of_term c with | Prod _ -> true | _ -> false
-
-(* Destructs the abstraction [x:t1]t2 *)
-let destLambda c = match kind_of_term c with
-  | Lambda (x,t1,t2) -> (x,t1,t2)
-  | _ -> raise DestKO
-
-let isLambda c = match kind_of_term c with | Lambda _ -> true | _ -> false
-
-(* Destructs the let [x:=b:t1]t2 *)
-let destLetIn c = match kind_of_term c with
-  | LetIn (x,b,t1,t2) -> (x,b,t1,t2)
-  | _ -> raise DestKO
-
-let isLetIn c =  match kind_of_term c with LetIn _ -> true | _ -> false
-
-(* Destructs an application *)
-let destApp c = match kind_of_term c with
-  | App (f,a) -> (f, a)
-  | _ -> raise DestKO
-
+let destRel = destRel
+let destMeta = destRel
+let isMeta = isMeta
+let destVar = destVar
+let isSort = isSort
+let destSort = destSort
+let isprop = isprop
+let is_Prop = is_Prop
+let is_Set = is_Set
+let is_Type = is_Type
+let is_small = is_small
+let iskind = iskind
+let isEvar = isEvar
+let isEvar_or_Meta = isEvar_or_Meta
+let destCast = destCast
+let isCast = isCast
+let isRel = isRel
+let isRelN = isRelN
+let isVar = isVar
+let isVarId = isVarId
+let isInd = isInd
+let destProd = destProd
+let isProd = isProd
+let destLambda = destLambda
+let isLambda = isLambda
+let destLetIn = destLetIn
+let isLetIn = isLetIn
+let destApp = destApp
 let destApplication = destApp
-
-let isApp c = match kind_of_term c with App _ -> true | _ -> false
-
-(* Destructs a constant *)
-let destConst c = match kind_of_term c with
-  | Const kn -> kn
-  | _ -> raise DestKO
-
-let isConst c = match kind_of_term c with Const _ -> true | _ -> false
-
-(* Destructs an existential variable *)
-let destEvar c = match kind_of_term c with
-  | Evar (kn, a as r) -> r
-  | _ -> raise DestKO
-
-(* Destructs a (co)inductive type named kn *)
-let destInd c = match kind_of_term c with
-  | Ind (kn, a as r) -> r
-  | _ -> raise DestKO
-
-(* Destructs a constructor *)
-let destConstruct c = match kind_of_term c with
-  | Construct (kn, a as r) -> r
-  | _ -> raise DestKO
-
-let isConstruct c = match kind_of_term c with Construct _ -> true | _ -> false
-
-(* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
-let destCase c = match kind_of_term c with
-  | Case (ci,p,c,v) -> (ci,p,c,v)
-  | _ -> raise DestKO
-
-let isCase c =  match kind_of_term c with Case _ -> true | _ -> false
-
-let isProj c =  match kind_of_term c with Proj _ -> true | _ -> false
-
-let destProj c = match kind_of_term c with
-  | Proj (p, c) -> (p, c)
-  | _ -> raise DestKO
-
-let destFix c = match kind_of_term c with
-  | Fix fix -> fix
-  | _ -> raise DestKO
-
-let isFix c =  match kind_of_term c with Fix _ -> true | _ -> false
-
-let destCoFix c = match kind_of_term c with
-  | CoFix cofix -> cofix
-  | _ -> raise DestKO
-
-let isCoFix c =  match kind_of_term c with CoFix _ -> true | _ -> false
+let isApp = isApp
+let destConst = destConst
+let isConst = isConst
+let destEvar = destEvar
+let destInd = destInd
+let destConstruct = destConstruct
+let isConstruct = isConstruct
+let destCase = destCase
+let isCase = isCase
+let isProj = isProj
+let destProj = destProj
+let destFix = destFix
+let isFix = isFix
+let destCoFix = destCoFix
+let isCoFix = isCoFix
 
 (******************************************************************)
 (* Flattening and unflattening of embedded applications and casts *)
diff --git a/kernel/term.mli b/kernel/term.mli
index 33c6b0b08..4efb582d0 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -16,90 +16,133 @@ open Constr
 
 *)
 
+exception DestKO
+[@@ocaml.deprecated "Alias for [Constr.DestKO]"]
+
 (** {5 Simple term case analysis. } *)
 val isRel  : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isRel]"]
 val isRelN : int -> constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isRelN]"]
 val isVar  : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isVar]"]
 val isVarId : Id.t -> constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isVarId]"]
 val isInd  : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isInd]"]
 val isEvar : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isEvar]"]
 val isMeta : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isMeta]"]
 val isEvar_or_Meta : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isEvar_or_Meta]"]
 val isSort : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isSort]"]
 val isCast : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isCast]"]
 val isApp : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isApp]"]
 val isLambda : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isLambda]"]
 val isLetIn : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isletIn]"]
 val isProd : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isProp]"]
 val isConst : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isConst]"]
 val isConstruct : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isConstruct]"]
 val isFix : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isFix]"]
 val isCoFix : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isCoFix]"]
 val isCase : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isCase]"]
 val isProj : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isProj]"]
 
 val is_Prop : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.is_Prop]"]
 val is_Set  : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.is_Set]"]
 val isprop : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.isprop]"]
 val is_Type : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.is_Type]"]
 val iskind : constr -> bool
+[@@ocaml.deprecated "Alias for [Constr.is_kind]"]
 val is_small : Sorts.t -> bool
+[@@ocaml.deprecated "Alias for [Constr.is_small]"]
 
 
 (** {5 Term destructors } *)
 (** Destructor operations are partial functions and
     @raise DestKO if the term has not the expected form. *)
 
-exception DestKO
-
 (** Destructs a de Bruijn index *)
 val destRel : constr -> int
+[@@ocaml.deprecated "Alias for [Constr.destRel]"]
 
 (** Destructs an existential variable *)
 val destMeta : constr -> metavariable
+[@@ocaml.deprecated "Alias for [Constr.destMeta]"]
 
 (** Destructs a variable *)
 val destVar : constr -> Id.t
+[@@ocaml.deprecated "Alias for [Constr.destVar]"]
 
 (** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether
    [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *)
 val destSort : constr -> Sorts.t
+[@@ocaml.deprecated "Alias for [Constr.destSort]"]
 
 (** Destructs a casted term *)
 val destCast : constr -> constr * cast_kind * constr
+[@@ocaml.deprecated "Alias for [Constr.destCast]"]
 
 (** Destructs the product {% $ %}(x:t_1)t_2{% $ %} *)
 val destProd : types -> Name.t * types * types
+[@@ocaml.deprecated "Alias for [Constr.destProd]"]
 
 (** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *)
 val destLambda : constr -> Name.t * types * constr
+[@@ocaml.deprecated "Alias for [Constr.destLambda]"]
 
 (** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *)
 val destLetIn : constr -> Name.t * constr * types * constr
+[@@ocaml.deprecated "Alias for [Constr.destLetIn]"]
 
 (** Destructs an application *)
 val destApp : constr -> constr * constr array
+[@@ocaml.deprecated "Alias for [Constr.destApp]"]
 
 (** Obsolete synonym of destApp *)
 val destApplication : constr -> constr * constr array
+[@@ocaml.deprecated "Alias for [Constr.destApplication]"]
 
 (** Decompose any term as an applicative term; the list of args can be empty *)
 val decompose_app : constr -> constr * constr list
+[@@ocaml.deprecated "Alias for [Constr.decompose_app]"]
 
 (** Same as [decompose_app], but returns an array. *)
 val decompose_appvect : constr -> constr * constr array
+[@@ocaml.deprecated "Alias for [Constr.decompose_appvect]"]
 
 (** Destructs a constant *)
 val destConst : constr -> Constant.t puniverses
+[@@ocaml.deprecated "Alias for [Constr.destConst]"]
 
 (** Destructs an existential variable *)
 val destEvar : constr -> existential
+[@@ocaml.deprecated "Alias for [Constr.destEvar]"]
 
 (** Destructs a (co)inductive type *)
 val destInd : constr -> inductive puniverses
+[@@ocaml.deprecated "Alias for [Constr.destInd]"]
 
 (** Destructs a constructor *)
 val destConstruct : constr -> constructor puniverses
+[@@ocaml.deprecated "Alias for [Constr.destConstruct]"]
 
 (** Destructs a [match c as x in I args return P with ... |
 Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args
@@ -107,9 +150,11 @@ return P in t1], or [if c then t1 else t2])
 @return [(info,c,fun args x => P,[|...|fun yij => ti| ...|])]
 where [info] is pretty-printing information *)
 val destCase : constr -> case_info * constr * constr * constr array
+[@@ocaml.deprecated "Alias for [Constr.destCase]"]
 
 (** Destructs a projection *)
 val destProj : constr -> projection * constr
+[@@ocaml.deprecated "Alias for [Constr.destProj]"]
 
 (** Destructs the {% $ %}i{% $ %}th function of the block
    [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1}
@@ -119,8 +164,10 @@ val destProj : constr -> projection * constr
    where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}.
 *)
 val destFix : constr -> fixpoint
+[@@ocaml.deprecated "Alias for [Constr.destFix]"]
 
 val destCoFix : constr -> cofixpoint
+[@@ocaml.deprecated "Alias for [Constr.destCoFix]"]
 
 (** {5 Derived constructors} *)
 
@@ -415,8 +462,11 @@ val map_constr_with_binders :
 [@@ocaml.deprecated "Alias for [Constr.map_with_binders]"]
 
 val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses
+[@@ocaml.deprecated "Alias for [Constr.map_puniverses]"]
 val univ_of_sort : Sorts.t -> Univ.Universe.t
+[@@ocaml.deprecated "Alias for [Sorts.univ_of_sort]"]
 val sort_of_univ : Univ.Universe.t -> Sorts.t
+[@@ocaml.deprecated "Alias for [Sorts.sort_of_univ]"]
 
 val iter_constr : (constr -> unit) -> constr -> unit
 [@@ocaml.deprecated "Alias for [Constr.iter]"]
diff --git a/library/heads.ml b/library/heads.ml
index 8b8e407f7..ee3bfe1bd 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -8,7 +8,6 @@
 
 open Util
 open Names
-open Term
 open Constr
 open Vars
 open Mod_subst
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index faabd7c14..ccef9ab96 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -12,13 +12,13 @@
 
 open CErrors
 open Pp
-open Goptions
 open Names
-open Term
+open Sorts
 open Constr
 open Vars
-open Tacmach
 open Evd
+open Goptions
+open Tacmach
 open Util
 
 let init_size=5
@@ -437,7 +437,7 @@ and make_app l=function
 and applist_proj c l =
   match c with
   | Symb s -> applist_projection s l
-  | _ -> applistc (constr_of_term c) l
+  | _ -> Term.applistc (constr_of_term c) l
 and applist_projection c l =
   match Constr.kind c with
   | Const c when Environ.is_projection (fst c) (Global.env()) ->
@@ -447,10 +447,10 @@ and applist_projection c l =
       let ty = Typeops.type_of_constant_in (Global.env ()) c in (* FIXME constraints *)
       let pb = Environ.lookup_projection p (Global.env()) in
       let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in
-	it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx
+      Term.it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx
     | hd :: tl ->
-      applistc (mkProj (p, hd)) tl)
-  | _ -> applistc c l
+      Term.applistc (mkProj (p, hd)) tl)
+  | _ -> Term.applistc c l
 
 let rec canonize_name sigma c =
   let c = EConstr.Unsafe.to_constr c in
@@ -838,7 +838,7 @@ let complete_one_class state i=
 	let _args =
 	  List.map (fun i -> constr_of_term (term state.uf  i))
 	    pac.args in
-	let typ = prod_applist _c (List.rev _args) in
+        let typ = Term.prod_applist _c (List.rev _args) in
 	let ct = app (term state.uf i) typ pac.arity in
 	  state.uf.epsilons <- pac :: state.uf.epsilons;
 	  ignore (add_term state ct)
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7dec34d4d..8642df684 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -12,7 +12,6 @@ open Evd
 open Names
 open Inductiveops
 open Declarations
-open Term
 open Constr
 open EConstr
 open Vars
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index f660ba734..d46201335 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -11,7 +11,7 @@ open Formula
 open Sequent
 open Rules
 open Instances
-open Term
+open Constr
 open Tacmach.New
 open Tacticals.New
 
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index d6309b057..1a6eba8c6 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -235,8 +235,8 @@ let constant str = Universes.constr_of_global
   @@ Coqlib.coq_reference "User" ["Init";"Logic"] str
 
 let defined_connectives=lazy
-  [AllOccurrences,EvalConstRef (fst (Term.destConst (constant "not")));
-   AllOccurrences,EvalConstRef (fst (Term.destConst (constant "iff")))]
+  [AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "not")));
+   AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "iff")))]
 
 let normalize_evaluables=
   Proofview.Goal.enter begin fun gl ->
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 29e824f44..62ca70626 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1,7 +1,7 @@
 open Printer
 open CErrors
 open Util
-open Term
+open Constr
 open EConstr
 open Vars
 open Namegen
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 3899bc709..996e2b6af 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -1,7 +1,8 @@
 open Printer
 open CErrors
-open Util
 open Term
+open Sorts
+open Util
 open Constr
 open Vars
 open Namegen
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index d04b7a33d..fa4353630 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1,7 +1,6 @@
 open Printer
 open Pp
 open Names
-open Term
 open Constr
 open Vars
 open Glob_term
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index f01b6669d..9e22ad306 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,7 +1,8 @@
 open CErrors
+open Sorts
 open Util
 open Names
-open Term
+open Constr
 open EConstr
 open Pp
 open Indfun_common
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 04d729b10..3089ec470 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -9,7 +9,6 @@
 
 module CVars = Vars
 
-open Term
 open Constr
 open EConstr
 open Vars
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 96bf31b11..0ea8904f2 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -104,7 +104,7 @@
 open CErrors
 open Util
 open Names
-open Term
+open Constr
 open EConstr
 open Pattern
 open Patternops
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 5397b0065..32a1c07b2 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -7,7 +7,6 @@
  *************************************************************************)
 
 open Names
-open Term
 open Constr
 
 let module_refl_name = "ReflOmegaCore"
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 274c7110c..bd9633afb 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -342,7 +342,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
     let sort = elimination_sort_of_goal gl in
     let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in
     if dir = R2L then elim, gl else (* taken from Coq's rewrite *)
-    let elim, _ = Term.destConst elim in          
+    let elim, _ = destConst elim in
     let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical elim)) in
     let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r")  in 
     let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make3 mp dp l')) in
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index a707226cd..5c1b399a8 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -8,11 +8,12 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
+open Pp
 open Names
+open Constr
 open Tacmach
 
 open Ssrmatching_plugin.Ssrmatching
-
 open Ssrprinters
 open Ssrcommon
 open Ssrtacticals
@@ -30,10 +31,6 @@ let ssrposetac ist (id, (_, t)) gl =
   let sigma, t, ucst, _ = pf_abs_ssrterm ist gl t in
   posetac id t (pf_merge_uc ucst gl)
 
-open Pp
-open Term
-open Constr
-
 let ssrsettac ist id ((_, (pat, pty)), (_, occ)) gl =
   let pat = interp_cpattern ist gl pat (Option.map snd pty) in
   let cl, sigma, env = pf_concl gl, project gl, pf_env gl in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 681eb17d3..18e0c31dd 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -9,7 +9,6 @@
 open CErrors
 open Util
 open Names
-open Term
 open Constr
 open Termops
 open Environ
@@ -49,7 +48,7 @@ let _ = Goptions.declare_bool_option {
    "data.id.type" etc... *)
 let impossible_default_case () =
   let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in
-  let (_, u) = Term.destConst c in
+  let (_, u) = Constr.destConst c in
   Some (c, Constr.mkConstU (Coqlib.type_of_id, u), ctx)
 
 let coq_unit_judge =
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 18dbbea1b..b646a37f8 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -6,10 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Sorts
 open Util
 open Pp
 open Names
-open Term
 open Constr
 open Termops
 open EConstr
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index fba154291..e6d1e59b3 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -6,10 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Sorts
 open Util
 open CErrors
 open Names
-open Term
 open Constr
 open Environ
 open Termops
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index e6d8a0af2..9ff9a75b3 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -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 (Term.decompose_app t) in
+  let args = snd (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
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 060cf6fc7..8fc00ed96 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -15,7 +15,6 @@ open CErrors
 open Util
 open Names
 open Nameops
-open Term
 open Termops
 open Declarations
 open Environ
@@ -139,7 +138,7 @@ let print_renames_list prefix l =
 
 let need_expansion impl ref =
   let typ, _ = Global.type_of_global_in_context (Global.env ()) ref in
-  let ctx = prod_assum typ in
+  let ctx = Term.prod_assum typ in
   let nprods = List.count is_local_assum ctx in
   not (List.is_empty impl) && List.length impl >= nprods &&
     let _,lastimpl = List.chop nprods impl in
@@ -490,7 +489,7 @@ let gallina_print_typed_value_in_env env sigma (trm,typ) =
 let print_named_def env sigma name body typ =
   let pbody = pr_lconstr_env env sigma body in
   let ptyp = pr_ltype_env env sigma typ in
-  let pbody = if isCast body then surround pbody else pbody in
+  let pbody = if Constr.isCast body then surround pbody else pbody in
   (str "*** [" ++ str name ++ str " " ++
      hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++
 	      str ":" ++ brk (1,2) ++ ptyp) ++
diff --git a/printing/printer.ml b/printing/printer.ml
index 377a6b4e1..d7bb0460d 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -10,7 +10,6 @@ open Pp
 open CErrors
 open Util
 open Names
-open Term
 open Constr
 open Environ
 open Globnames
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 13a4e4ce3..a9ad606a0 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -11,7 +11,6 @@ open CErrors
 open Util
 open Names
 open Nameops
-open Term
 open Constr
 open Vars
 open Termops
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 6a9cd7e20..de98f6382 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -9,7 +9,6 @@
 open Equality
 open Names
 open Pp
-open Term
 open Constr
 open Termops
 open CErrors
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 75fae6647..8e851375a 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -160,7 +160,7 @@ let test_strict_disjunction n lc =
   let open Term in
   Array.for_all_i (fun i c ->
     match (prod_assum (snd (decompose_prod_n_assum n c))) with
-    | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i)
+    | [LocalAssum (_,c)] -> Constr.isRel c && Int.equal (Constr.destRel c) (n - i)
     | _ -> false) 0 lc
 
 let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
diff --git a/vernac/command.ml b/vernac/command.ml
index fd0027c40..257c003b5 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -8,8 +8,8 @@
 
 open Pp
 open CErrors
+open Sorts
 open Util
-open Term
 open Constr
 open Vars
 open Termops
@@ -376,8 +376,8 @@ let rec check_anonymous_type ind =
     | _ -> false
 
 let make_conclusion_flexible evdref ty poly =
-  if poly && isArity ty then
-    let _, concl = destArity ty in
+  if poly && Term.isArity ty then
+    let _, concl = Term.destArity ty in
       match concl with
       | Type u -> 
         (match Univ.universe_level u with
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 839064aa0..e8c5aeedd 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -11,7 +11,7 @@ open Util
 open Names
 open Nameops
 open Namegen
-open Term
+open Constr
 open Termops
 open Indtypes
 open Environ
@@ -405,7 +405,7 @@ let explain_not_product env sigma c =
   let pr = pr_lconstr_env env sigma c in
   str "The type of this term is a product" ++ spc () ++
   str "while it is expected to be" ++
-  (if Term.is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "."
+  (if Constr.is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "."
 
 (* TODO: use the names *)
 (* (co)fixpoints *)
diff --git a/vernac/record.ml b/vernac/record.ml
index 1bd47a556..f09b57048 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -8,11 +8,12 @@
 
 open Pp
 open CErrors
+open Term
+open Sorts
 open Util
 open Names
 open Globnames
 open Nameops
-open Term
 open Constr
 open Vars
 open Environ