[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`.

7 files changed, 387 insertions, 186 deletions

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]"]