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/evd.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'engine/evd.mli')

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