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

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 860d19fe26..388b4f14bf 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -165,7 +165,7 @@ type one_inductive_body = {
 
     mind_nrealdecls : int; (** Length of realargs context (with let, no params) *)
 
-    mind_kelim : Sorts.family list; (** List of allowed elimination sorts *)
+    mind_kelim : Sorts.family; (** Highest allowed elimination sort *)
 
     mind_nf_lc : (rel_context * types) array; (** Head normalized constructor types so that their conclusion exposes the inductive type *)
 
-- 
cgit v1.2.3