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.mli | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'engine/eConstr.mli')

diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 90f50b764c..af44879e50 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} *)
 
-- 
cgit v1.2.3