Move kind_of_type from the kernel to ssr.

It was virtually unused except in ssr, and there is no reason to clutter
the kernel with irrelevant code.

Fixes #9390: What is the purpose of the function "kind_of_type"?

1 files changed, 20 insertions, 0 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 150dad16c2..51d2962851 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -726,6 +726,26 @@ let fresh_global ?loc ?rigid ?names env sigma reference =
 let is_global sigma gr c =
   Globnames.is_global gr (to_constr sigma c)
 
+(** 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