From be8db31abc6839921e91540ab4b3300da9b64933 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 10 May 2019 11:49:50 +0200
Subject: mind_kelim is the highest allowed sort instead of a list

---
 kernel/sorts.mli | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'kernel/sorts.mli')

diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index c49728b146..3769e31465 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -37,11 +37,7 @@ val hcons : t -> t
 
 val family_compare : family -> family -> int
 val family_equal : family -> family -> bool
-
-module List : sig
-  val mem : family -> family list -> bool
-  val intersect : family list -> family list -> family list
-end
+val family_leq : family -> family -> bool
 
 val univ_of_sort : t -> Univ.Universe.t
 val sort_of_univ : Univ.Universe.t -> t
-- 
cgit v1.2.3