From 238b0cb82a1e66332131f10de79f4abe55d4b0b2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 17 Jan 2020 13:40:10 +0100
Subject: 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"?
---
 engine/eConstr.ml | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'engine/eConstr.ml')

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
-- 
cgit v1.2.3