[api] Remove deprecated object from `Term`

We remove most of what was deprecated in `Term`. Now, `intf` and
`kernel` are almost deprecation-free, tho I am not very convinced
about the whole `Term -> Constr` renaming but I'm afraid there is no
way back.

Inconsistencies with the constructor policy (see #6440) remain along
the code-base and I'm afraid I don't see a plan to reconcile them.

The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a
good idea as someone added a `List` module inside it.

3 files changed, 32 insertions, 622 deletions

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index cea09c510..f4e6d45c2 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -13,7 +13,7 @@
 (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *)
 
 open Names
-open Term
+open Constr
 open Cbytecodes
 open Copcodes
 open Mod_subst
diff --git a/kernel/term.ml b/kernel/term.ml
index e1affb1c0..b44e038e9 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -15,219 +15,17 @@ open Names
 open Vars
 open Constr
 
-(**********************************************************************)
-(**         Redeclaration of types from module Constr                 *)
-(**********************************************************************)
-
+(* Deprecated *)
 type contents = Sorts.contents = Pos | Null
-
-type sorts = Sorts.t =
-  | Prop of contents       (** Prop and Set *)
-  | Type of Univ.Universe.t  (** Type *)
+[@@ocaml.deprecated "Alias for Sorts.contents"]
 
 type sorts_family = Sorts.family = InProp | InSet | InType
+[@@ocaml.deprecated "Alias for Sorts.family"]
 
-type constr = Constr.t
-(** Alias types, for compatibility. *)
-
-type types = Constr.t
-(** Same as [constr], for documentation purposes. *)
-
-type existential_key = Evar.t
-type existential = Constr.existential
-
-type metavariable = Constr.metavariable
-
-type case_style = Constr.case_style =
-  LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
-
-type case_printing = Constr.case_printing =
-  { ind_tags : bool list; cstr_tags : bool list array; style : case_style }
-
-type case_info = Constr.case_info =
-  { ci_ind        : inductive;
-    ci_npar       : int;
-    ci_cstr_ndecls : int array;
-    ci_cstr_nargs : int array;
-    ci_pp_info    : case_printing
-  }
-
-type cast_kind = Constr.cast_kind =
-  VMcast | NATIVEcast | DEFAULTcast | REVERTcast
-
-(********************************************************************)
-(*       Constructions as implemented                               *)
-(********************************************************************)
-
-type rec_declaration = Constr.rec_declaration
-type fixpoint = Constr.fixpoint
-type cofixpoint = Constr.cofixpoint
-type 'constr pexistential = 'constr Constr.pexistential
-type ('constr, 'types) prec_declaration =
-  ('constr, 'types) Constr.prec_declaration
-type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint
-type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint
-type 'a puniverses = 'a Univ.puniverses
-
-(** Simply type aliases *)
-type pconstant = Constant.t puniverses
-type pinductive = inductive puniverses
-type pconstructor = constructor puniverses
-
-type ('constr, 'types, 'sort, 'univs) kind_of_term =
-  ('constr, 'types, 'sort, 'univs) Constr.kind_of_term =
-  | Rel       of int
-  | Var       of Id.t
-  | Meta      of metavariable
-  | Evar      of 'constr pexistential
-  | Sort      of 'sort
-  | Cast      of 'constr * cast_kind * 'types
-  | Prod      of Name.t * 'types * 'types
-  | Lambda    of Name.t * 'types * 'constr
-  | LetIn     of Name.t * 'constr * 'types * 'constr
-  | App       of 'constr * 'constr array
-  | Const     of (Constant.t * 'univs)
-  | Ind       of (inductive * 'univs)
-  | Construct of (constructor * 'univs)
-  | Case      of case_info * 'constr * 'constr * 'constr array
-  | Fix       of ('constr, 'types) pfixpoint
-  | CoFix     of ('constr, 'types) pcofixpoint
-  | Proj      of Projection.t * 'constr
-
-type values = Vmvalues.values
-
-(**********************************************************************)
-(**         Redeclaration of functions from module Constr             *)
-(**********************************************************************)
-
-let set_sort  = Sorts.set
-let prop_sort = Sorts.prop
-let type1_sort  = Sorts.type1
-let sorts_ord = Sorts.compare
-let is_prop_sort = Sorts.is_prop
-let family_of_sort = Sorts.family
-let univ_of_sort = Sorts.univ_of_sort
-let sort_of_univ = Sorts.sort_of_univ
-
-(** {6 Term constructors. } *)
-
-let mkRel = Constr.mkRel
-let mkVar = Constr.mkVar
-let mkMeta = Constr.mkMeta
-let mkEvar = Constr.mkEvar
-let mkSort = Constr.mkSort
-let mkProp = Constr.mkProp
-let mkSet  = Constr.mkSet 
-let mkType = Constr.mkType
-let mkCast = Constr.mkCast
-let mkProd = Constr.mkProd
-let mkLambda = Constr.mkLambda
-let mkLetIn = Constr.mkLetIn
-let mkApp = Constr.mkApp
-let mkConst = Constr.mkConst
-let mkProj = Constr.mkProj
-let mkInd = Constr.mkInd
-let mkConstruct = Constr.mkConstruct
-let mkConstU = Constr.mkConstU
-let mkIndU = Constr.mkIndU
-let mkConstructU = Constr.mkConstructU
-let mkConstructUi = Constr.mkConstructUi
-let mkCase = Constr.mkCase
-let mkFix = Constr.mkFix
-let mkCoFix = Constr.mkCoFix
-
-(**********************************************************************)
-(**         Aliases of functions from module Constr                   *)
-(**********************************************************************)
-
-let eq_constr = Constr.equal
-let eq_constr_univs = Constr.eq_constr_univs
-let leq_constr_univs = Constr.leq_constr_univs
-let eq_constr_nounivs = Constr.eq_constr_nounivs
-
-let kind_of_term = Constr.kind
-let compare = Constr.compare
-let constr_ord = compare
-let fold_constr = Constr.fold
-let map_puniverses = Constr.map_puniverses
-let map_constr = Constr.map
-let map_constr_with_binders = Constr.map_with_binders
-let iter_constr = Constr.iter
-let iter_constr_with_binders = Constr.iter_with_binders
-let compare_constr = Constr.compare_head
-let hash_constr = Constr.hash
-let hcons_sorts = Sorts.hcons
-let hcons_constr = Constr.hcons
-let hcons_types = Constr.hcons
-
-(**********************************************************************)
-(**         HERE BEGINS THE INTERESTING STUFF                         *)
-(**********************************************************************)
-
-(**********************************************************************)
-(*          Non primitive term destructors                            *)
-(**********************************************************************)
-
-exception DestKO = DestKO
-(* Destructs a de Bruijn index *)
-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 = 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 *)
-(******************************************************************)
-
-let decompose_app c =
-  match kind_of_term c with
-    | App (f,cl) -> (f, Array.to_list cl)
-    | _ -> (c,[])
-
-let decompose_appvect c =
-  match kind_of_term c with
-    | App (f,cl) -> (f, cl)
-    | _ -> (c,[||])
+type sorts = Sorts.t =
+  | Prop of Sorts.contents   (** Prop and Set *)
+  | Type of Univ.Universe.t  (** Type *)
+[@@ocaml.deprecated "Alias for Sorts.t"]
 
 (****************************************************************************)
 (*              Functions for dealing with constr terms                     *)
@@ -321,7 +119,7 @@ let rec to_lambda n prod =
   if Int.equal n 0 then
     prod
   else
-    match kind_of_term prod with
+    match kind prod with
       | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd)
       | Cast (c,_,_) -> to_lambda n c
       | _   -> user_err ~hdr:"to_lambda" (mt ())
@@ -330,7 +128,7 @@ let rec to_prod n lam =
   if Int.equal n 0 then
     lam
   else
-    match kind_of_term lam with
+    match kind lam with
       | Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd)
       | Cast (c,_,_) -> to_prod n c
       | _   -> user_err ~hdr:"to_prod" (mt ())
@@ -342,7 +140,7 @@ let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c)
 
 let lambda_applist c l =
   let rec app subst c l =
-    match kind_of_term c, l with
+    match kind c, l with
     | Lambda(_,_,c), arg::l -> app (arg::subst) c l
     | _, [] -> substl subst c
     | _ -> anomaly (Pp.str "Not enough lambda's.") in
@@ -355,7 +153,7 @@ let lambda_applist_assum n c l =
     if Int.equal n 0 then
       if l == [] then substl subst t
       else anomaly (Pp.str "Too many arguments.")
-    else match kind_of_term t, l with
+    else match kind t, l with
     | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l
     | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
     | _, [] -> anomaly (Pp.str "Not enough arguments.")
@@ -367,7 +165,7 @@ let lambda_appvect_assum n c v = lambda_applist_assum n c (Array.to_list v)
 (* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *)
 let prod_applist c l =
   let rec app subst c l =
-    match kind_of_term c, l with
+    match kind c, l with
     | Prod(_,_,c), arg::l -> app (arg::subst) c l
     | _, [] -> substl subst c
     | _ -> anomaly (Pp.str "Not enough prod's.") in
@@ -381,7 +179,7 @@ let prod_applist_assum n c l =
     if Int.equal n 0 then
       if l == [] then substl subst t
       else anomaly (Pp.str "Too many arguments.")
-    else match kind_of_term t, l with
+    else match kind t, l with
     | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l
     | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
     | _, [] -> anomaly (Pp.str "Not enough arguments.")
@@ -397,7 +195,7 @@ let prod_appvect_assum n c v = prod_applist_assum n c (Array.to_list v)
 (* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
    ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
 let decompose_prod =
-  let rec prodec_rec l c = match kind_of_term c with
+  let rec prodec_rec l c = match kind c with
     | Prod (x,t,c) -> prodec_rec ((x,t)::l) c
     | Cast (c,_,_)   -> prodec_rec l c
     | _              -> l,c
@@ -407,7 +205,7 @@ let decompose_prod =
 (* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair
    ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)
 let decompose_lam =
-  let rec lamdec_rec l c = match kind_of_term c with
+  let rec lamdec_rec l c = match kind c with
     | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c
     | Cast (c,_,_)     -> lamdec_rec l c
     | _                -> l,c
@@ -420,7 +218,7 @@ let decompose_prod_n n =
   if n < 0 then user_err (str "decompose_prod_n: integer parameter must be positive");
   let rec prodec_rec l n c =
     if Int.equal n 0 then l,c
-    else match kind_of_term c with
+    else match kind c with
       | Prod (x,t,c) -> prodec_rec ((x,t)::l) (n-1) c
       | Cast (c,_,_)   -> prodec_rec l n c
       | _ -> user_err (str "decompose_prod_n: not enough products")
@@ -433,7 +231,7 @@ let decompose_lam_n n =
   if n < 0 then user_err (str "decompose_lam_n: integer parameter must be positive");
   let rec lamdec_rec l n c =
     if Int.equal n 0 then l,c
-    else match kind_of_term c with
+    else match kind c with
       | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c
       | Cast (c,_,_)     -> lamdec_rec l n c
       | _ -> user_err (str "decompose_lam_n: not enough abstractions")
@@ -445,7 +243,7 @@ let decompose_lam_n n =
 let decompose_prod_assum =
   let open Context.Rel.Declaration in
   let rec prodec_rec l c =
-    match kind_of_term c with
+    match kind c with
     | Prod (x,t,c)    -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) c
     | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c
     | Cast (c,_,_)      -> prodec_rec l c
@@ -458,7 +256,7 @@ let decompose_prod_assum =
 let decompose_lam_assum =
   let rec lamdec_rec l c =
     let open Context.Rel.Declaration in
-    match kind_of_term c with
+    match kind c with
     | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) c
     | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c
     | Cast (c,_,_)      -> lamdec_rec l c
@@ -477,7 +275,7 @@ let decompose_prod_n_assum n =
     if Int.equal n 0 then l,c
     else
       let open Context.Rel.Declaration in
-      match kind_of_term c with
+      match kind c with
       | Prod (x,t,c)    -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
       | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c
       | Cast (c,_,_)      -> prodec_rec l n c
@@ -498,7 +296,7 @@ let decompose_lam_n_assum n =
     if Int.equal n 0 then l,c
     else
       let open Context.Rel.Declaration in
-      match kind_of_term c with
+      match kind c with
       | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
       | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c
       | Cast (c,_,_)      -> lamdec_rec l n c
@@ -514,7 +312,7 @@ let decompose_lam_n_decls n =
     if Int.equal n 0 then l,c
     else
       let open Context.Rel.Declaration in
-      match kind_of_term c with
+      match kind c with
       | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
       | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c
       | Cast (c,_,_)      -> lamdec_rec l n c
@@ -541,12 +339,12 @@ let strip_lam_n n t = snd (decompose_lam_n n t)
    Such a term can canonically be seen as the pair of a context of types
    and of a sort *)
 
-type arity = Context.Rel.t * sorts
+type arity = Context.Rel.t * Sorts.t
 
 let destArity =
   let open Context.Rel.Declaration in
   let rec prodec_rec l c =
-    match kind_of_term c with
+    match kind c with
     | Prod (x,t,c)    -> prodec_rec (LocalAssum (x,t) :: l) c
     | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c
     | Cast (c,_,_)      -> prodec_rec l c
@@ -558,7 +356,7 @@ let destArity =
 let mkArity (sign,s) = it_mkProd_or_LetIn (mkSort s) sign
 
 let rec isArity c =
-  match kind_of_term c with
+  match kind c with
   | Prod (_,_,c)    -> isArity c
   | LetIn (_,b,_,c) -> isArity (subst1 b c)
   | Cast (c,_,_)      -> isArity c
@@ -569,13 +367,13 @@ let rec isArity c =
 
 (* Experimental, used in Presburger contrib *)
 type ('constr, 'types) kind_of_type =
-  | SortType   of sorts
+  | SortType   of Sorts.t
   | CastType   of 'types * 'types
   | ProdType   of Name.t * 'types * 'types
   | LetInType  of Name.t * 'constr * 'types * 'types
   | AtomicType of 'constr * 'constr array
 
-let kind_of_type t = match kind_of_term t with
+let kind_of_type t = match kind t with
   | Sort s -> SortType s
   | Cast (c,_,t) -> CastType (c, t)
   | Prod (na,t,c) -> ProdType (na, t, c)
diff --git a/kernel/term.mli b/kernel/term.mli
index ee84dcb2b..f651d1a58 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -11,166 +11,6 @@
 open Names
 open Constr
 
-(** {5 Redeclaration of types from module Constr and Sorts}
-
-    This reexports constructors of inductive types defined in module [Constr],
-    for compatibility purposes. Refer to this module for further info.
-
-*)
-
-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. *)
-
-(** 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 Univ.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 Univ.puniverses
-[@@ocaml.deprecated "Alias for [Constr.destInd]"]
-
-(** Destructs a constructor *)
-val destConstruct : constr -> constructor Univ.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
-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.t * constr
-[@@ocaml.deprecated "Alias for [Constr.destProj]"]
-
-(** 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
-[@@ocaml.deprecated "Alias for [Constr.destFix]"]
-
-val destCoFix : constr -> cofixpoint
-[@@ocaml.deprecated "Alias for [Constr.destCoFix]"]
-
 (** {5 Derived constructors} *)
 
 (** non-dependent product [t1 -> t2], an alias for
@@ -349,242 +189,14 @@ type ('constr, 'types) kind_of_type =
 
 val kind_of_type : types -> (constr, types) kind_of_type
 
-(** {5 Redeclaration of stuff from module [Sorts]} *)
-
-val set_sort  : Sorts.t
-[@@ocaml.deprecated "Alias for Sorts.set"]
-
-val prop_sort : Sorts.t
-[@@ocaml.deprecated "Alias for Sorts.prop"]
-
-val type1_sort  : Sorts.t
-[@@ocaml.deprecated "Alias for Sorts.type1"]
-
-val sorts_ord : Sorts.t -> Sorts.t -> int
-[@@ocaml.deprecated "Alias for Sorts.compare"]
-
-val is_prop_sort : Sorts.t -> bool
-[@@ocaml.deprecated "Alias for Sorts.is_prop"]
-
-val family_of_sort : Sorts.t -> Sorts.family
-[@@ocaml.deprecated "Alias for Sorts.family"]
-
-(** {5 Redeclaration of stuff from module [Constr]}
-
-    See module [Constr] for further info. *)
-
-(** {6 Term constructors. } *)
-
-val mkRel : int -> constr
-[@@ocaml.deprecated "Alias for Constr.mkRel"]
-val mkVar : Id.t -> constr
-[@@ocaml.deprecated "Alias for Constr.mkVar"]
-val mkMeta : metavariable -> constr
-[@@ocaml.deprecated "Alias for Constr.mkMeta"]
-val mkEvar : existential -> constr
-[@@ocaml.deprecated "Alias for Constr.mkEvar"]
-val mkSort : Sorts.t -> types
-[@@ocaml.deprecated "Alias for Constr.mkSort"]
-val mkProp : types
-[@@ocaml.deprecated "Alias for Constr.mkProp"]
-val mkSet  : types
-[@@ocaml.deprecated "Alias for Constr.mkSet"]
-val mkType : Univ.Universe.t -> types
-[@@ocaml.deprecated "Alias for Constr.mkType"]
-val mkCast : constr * cast_kind * constr -> constr
-[@@ocaml.deprecated "Alias for Constr"]
-val mkProd : Name.t * types * types -> types
-[@@ocaml.deprecated "Alias for Constr"]
-val mkLambda : Name.t * types * constr -> constr
-[@@ocaml.deprecated "Alias for Constr"]
-val mkLetIn : Name.t * constr * types * constr -> constr
-[@@ocaml.deprecated "Alias for Constr"]
-val mkApp : constr * constr array -> constr
-[@@ocaml.deprecated "Alias for Constr"]
-val mkConst : Constant.t -> constr
-[@@ocaml.deprecated "Alias for Constr"]
-val mkProj : Projection.t * constr -> constr
-[@@ocaml.deprecated "Alias for Constr"]
-val mkInd : inductive -> constr
-[@@ocaml.deprecated "Alias for Constr"]
-val mkConstruct : constructor -> constr
-[@@ocaml.deprecated "Alias for Constr"]
-val mkConstU : Constant.t Univ.puniverses -> constr
-[@@ocaml.deprecated "Alias for Constr"]
-val mkIndU : inductive Univ.puniverses -> constr
-[@@ocaml.deprecated "Alias for Constr"]
-val mkConstructU : constructor Univ.puniverses -> constr
-[@@ocaml.deprecated "Alias for Constr"]
-val mkConstructUi : (pinductive * int) -> constr
-[@@ocaml.deprecated "Alias for Constr"]
-val mkCase : case_info * constr * constr * constr array -> constr
-[@@ocaml.deprecated "Alias for Constr.mkCase"]
-val mkFix : fixpoint -> constr
-[@@ocaml.deprecated "Alias for Constr.mkFix"]
-val mkCoFix : cofixpoint -> constr
-[@@ocaml.deprecated "Alias for Constr.mkCoFix"]
-
-(** {6 Aliases} *)
-
-val eq_constr : constr -> constr -> bool
-[@@ocaml.deprecated "Alias for Constr.equal"]
-
-(** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
-   application grouping and the universe constraints in [u]. *)
-val eq_constr_univs : constr UGraph.check_function
-[@@ocaml.deprecated "Alias for Constr.eq_constr_univs"]
-
-(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo 
-    alpha, casts, application grouping and the universe constraints in [u]. *)
-val leq_constr_univs : constr UGraph.check_function
-[@@ocaml.deprecated "Alias for Constr.leq_constr_univs"]
-
-(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts,
-   application grouping and ignoring universe instances. *)
-val eq_constr_nounivs : constr -> constr -> bool
-[@@ocaml.deprecated "Alias for Constr.qe_constr_nounivs"]
-
-val kind_of_term : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term
-[@@ocaml.deprecated "Alias for Constr.kind"]
-
-val compare : constr -> constr -> int
-[@@ocaml.deprecated "Alias for [Constr.compare]"]
-
-val constr_ord : constr -> constr -> int
-[@@ocaml.deprecated "Alias for [Term.compare]"]
-
-val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a
-[@@ocaml.deprecated "Alias for [Constr.fold]"]
-
-val map_constr : (constr -> constr) -> constr -> constr
-[@@ocaml.deprecated "Alias for [Constr.map]"]
-
-val map_constr_with_binders :
-  ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
-[@@ocaml.deprecated "Alias for [Constr.map_with_binders]"]
-
-val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.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]"]
-
-val iter_constr_with_binders :
-  ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
-[@@ocaml.deprecated "Alias for [Constr.iter_with_binders]"]
-
-val compare_constr : (int -> constr -> constr -> bool) -> int -> constr -> constr -> bool
-[@@ocaml.deprecated "Alias for [Constr.compare_head]"]
-
-type constr = Constr.constr
-[@@ocaml.deprecated "Alias for Constr.t"]
-
-(** Alias types, for compatibility. *)
-
-type types = Constr.types
-[@@ocaml.deprecated "Alias for Constr.types"]
-
+(* Deprecated *)
 type contents = Sorts.contents = Pos | Null
 [@@ocaml.deprecated "Alias for Sorts.contents"]
 
+type sorts_family = Sorts.family = InProp | InSet | InType
+[@@ocaml.deprecated "Alias for Sorts.family"]
+
 type sorts = Sorts.t =
   | Prop of Sorts.contents   (** Prop and Set *)
   | Type of Univ.Universe.t  (** Type *)
 [@@ocaml.deprecated "Alias for Sorts.t"]
-
-type sorts_family = Sorts.family = InProp | InSet | InType
-[@@ocaml.deprecated "Alias for Sorts.family"]
-
-type 'a puniverses = 'a Univ.puniverses
-[@@ocaml.deprecated "Alias for Constr.puniverses"]
-
-(** Simply type aliases *)
-type pconstant = Constr.pconstant
-[@@ocaml.deprecated "Alias for Constr.pconstant"]
-type pinductive = Constr.pinductive
-[@@ocaml.deprecated "Alias for Constr.pinductive"]
-type pconstructor = Constr.pconstructor
-[@@ocaml.deprecated "Alias for Constr.pconstructor"]
-type existential_key = Evar.t
-[@@ocaml.deprecated "Alias for Evar.t"]
-type existential = Constr.existential
-[@@ocaml.deprecated "Alias for Constr.existential"]
-type metavariable = Constr.metavariable
-[@@ocaml.deprecated "Alias for Constr.metavariable"]
-
-type case_style = Constr.case_style =
-  LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
-[@@ocaml.deprecated "Alias for Constr.case_style"]
-
-type case_printing = Constr.case_printing =
-  { ind_tags : bool list; cstr_tags : bool list array; style : Constr.case_style }
-[@@ocaml.deprecated "Alias for Constr.case_printing"]
-
-type case_info = Constr.case_info =
-  { ci_ind         : inductive;
-    ci_npar        : int;
-    ci_cstr_ndecls : int array;
-    ci_cstr_nargs  : int array;
-    ci_pp_info     : Constr.case_printing
-  }
-[@@ocaml.deprecated "Alias for Constr.case_info"]
-
-type cast_kind = Constr.cast_kind =
-  VMcast | NATIVEcast | DEFAULTcast | REVERTcast
-[@@ocaml.deprecated "Alias for Constr.cast_kind"]
-
-type rec_declaration = Constr.rec_declaration
-[@@ocaml.deprecated "Alias for Constr.rec_declaration"]
-type fixpoint = Constr.fixpoint
-[@@ocaml.deprecated "Alias for Constr.fixpoint"]
-type cofixpoint = Constr.cofixpoint
-[@@ocaml.deprecated "Alias for Constr.cofixpoint"]
-type 'constr pexistential = 'constr Constr.pexistential
-[@@ocaml.deprecated "Alias for Constr.pexistential"]
-type ('constr, 'types) prec_declaration =
-  ('constr, 'types) Constr.prec_declaration
-[@@ocaml.deprecated "Alias for Constr.prec_declaration"]
-type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint
-[@@ocaml.deprecated "Alias for Constr.pfixpoint"]
-type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint
-[@@ocaml.deprecated "Alias for Constr.pcofixpoint"]
-
-type ('constr, 'types, 'sort, 'univs) kind_of_term =
-  ('constr, 'types, 'sort, 'univs) Constr.kind_of_term =
-  | Rel       of int
-  | Var       of Id.t
-  | Meta      of Constr.metavariable
-  | Evar      of 'constr Constr.pexistential
-  | Sort      of 'sort
-  | Cast      of 'constr * Constr.cast_kind * 'types
-  | Prod      of Name.t * 'types * 'types
-  | Lambda    of Name.t * 'types * 'constr
-  | LetIn     of Name.t * 'constr * 'types * 'constr
-  | App       of 'constr * 'constr array
-  | Const     of (Constant.t * 'univs)
-  | Ind       of (inductive * 'univs)
-  | Construct of (constructor * 'univs)
-  | Case      of Constr.case_info * 'constr * 'constr * 'constr array
-  | Fix       of ('constr, 'types) Constr.pfixpoint
-  | CoFix     of ('constr, 'types) Constr.pcofixpoint
-  | Proj      of Projection.t * 'constr
-[@@ocaml.deprecated "Alias for Constr.kind_of_term"]
-
-type values = Vmvalues.values
-[@@ocaml.deprecated "Alias for Vmvalues.values"]
-
-val hash_constr : Constr.constr -> int
-[@@ocaml.deprecated "Alias for Constr.hash"]
-
-val hcons_sorts : Sorts.t -> Sorts.t
-[@@ocaml.deprecated "Alias for [Sorts.hcons]"]
-
-val hcons_constr : Constr.constr -> Constr.constr
-[@@ocaml.deprecated "Alias for [Constr.hcons]"]
-
-val hcons_types : Constr.types -> Constr.types
-[@@ocaml.deprecated "Alias for [Constr.hcons]"]