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"?
---
 kernel/term.mli | 11 -----------
 1 file changed, 11 deletions(-)

(limited to 'kernel/term.mli')

diff --git a/kernel/term.mli b/kernel/term.mli
index d2de4177ce..1fef54257a 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -181,17 +181,6 @@ val destArity : types -> arity
 (** Tell if a term has the form of an arity *)
 val isArity : types -> bool
 
-(** {5 Kind of type} *)
-
-type ('constr, 'types) kind_of_type =
-  | SortType   of Sorts.t
-  | CastType   of 'types * 'types
-  | ProdType   of Name.t Context.binder_annot * 'types * 'types
-  | LetInType  of Name.t Context.binder_annot * 'constr * 'types * 'types
-  | AtomicType of 'constr * 'constr array
-
-val kind_of_type : types -> (constr, types) kind_of_type
-
 (* Deprecated *)
 type sorts_family = Sorts.family = InSProp | InProp | InSet | InType
 [@@ocaml.deprecated "Alias for Sorts.family"]
-- 
cgit v1.2.3