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.ml  | 21 ---------------------
 kernel/term.mli | 11 -----------
 2 files changed, 32 deletions(-)

(limited to 'kernel')

diff --git a/kernel/term.ml b/kernel/term.ml
index 87678b911e..a2586e74f7 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -363,24 +363,3 @@ let rec isArity c =
   | Cast (c,_,_)      -> isArity c
   | Sort _          -> true
   | _               -> false
-
-(** Kind of type *)
-
-(* Experimental, used in Presburger contrib *)
-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
-
-let kind_of_type t = match kind 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"
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