Merge PR #11417: Move kind_of_type from the kernel to EConstr.

Reviewed-by: SkySkimmer
Reviewed-by: gares

4 files changed, 28 insertions, 3 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index e37a58be61..08e283f524 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -739,6 +739,26 @@ let fresh_global ?loc ?rigid ?names env sigma reference =
 
 let is_global = isRefX
 
+(** Kind of type *)
+
+type kind_of_type =
+  | SortType   of ESorts.t
+  | CastType   of types * t
+  | ProdType   of Name.t Context.binder_annot * t * t
+  | LetInType  of Name.t Context.binder_annot * t * t * t
+  | AtomicType of t * t array
+
+let kind_of_type sigma t = match kind sigma t with
+  | Sort s -> SortType s
+  | Cast (c,_,t) -> CastType (c, t)
+  | Prod (na,t,c) -> ProdType (na, t, c)
+  | LetIn (na,b,t,c) -> LetInType (na, b, t, c)
+  | App (c,l) -> AtomicType (c, l)
+  | (Rel _ | Meta _ | Var _ | Evar _ | Const _
+  | Proj _ | Case _ | Fix _ | CoFix _ | Ind _)
+    -> AtomicType (t,[||])
+  | (Lambda _ | Construct _ | Int _ | Float _) -> failwith "Not a type"
+
 module Unsafe =
 struct
 let to_sorts = ESorts.unsafe_to_sorts
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 181714460d..ead7d88176 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -80,7 +80,14 @@ val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t
 val to_constr_opt : Evd.evar_map -> t -> Constr.t option
 (** Same as [to_constr], but returns [None] if some unresolved evars remain *)
 
-val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
+type kind_of_type =
+  | SortType   of ESorts.t
+  | CastType   of types * t
+  | ProdType   of Name.t Context.binder_annot * t * t
+  | LetInType  of Name.t Context.binder_annot * t * t * t
+  | AtomicType of t * t array
+
+val kind_of_type : Evd.evar_map -> t -> kind_of_type
 
 (** {5 Constructors} *)
 
diff --git a/engine/evd.ml b/engine/evd.ml
index 70f58163fd..4bfa7c45e3 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1364,7 +1364,6 @@ module MiniEConstr = struct
 
   let kind sigma c = Constr.kind (whd_evar sigma c)
   let kind_upto = kind
-  let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c)
   let of_kind = Constr.of_kind
   let of_constr c = c
   let of_constr_array v = v
diff --git a/engine/evd.mli b/engine/evd.mli
index 82e1003a65..2c1194a5de 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -711,7 +711,6 @@ module MiniEConstr : sig
 
   val kind : evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
   val kind_upto : evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term
-  val kind_of_type : evar_map -> t -> (t, t) Term.kind_of_type
 
   val whd_evar : evar_map -> t -> t