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/inductive.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/inductive.mli')

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 997a620742..f705cdf646 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -52,7 +52,7 @@ val type_of_inductive : env -> mind_specif puniverses -> types
 val type_of_inductive_knowing_parameters :
   env -> ?polyprop:bool -> mind_specif puniverses -> types Lazy.t array -> types
 
-val elim_sorts : mind_specif -> Sorts.family list
+val elim_sort : mind_specif -> Sorts.family
 
 val is_private : mind_specif -> bool
 val is_primitive_record : mind_specif -> bool
-- 
cgit v1.2.3