From 2b833c49456c52ae941fc87b789e9d520d5b3c40 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 11 Jul 2014 19:18:39 +0200
Subject: Properly add a Set lower bound on any polymorphic inductive in Type
 with more than one constructor.

---
 kernel/indtypes.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index ee4a404a7c..f79d16c02f 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -156,8 +156,10 @@ let infer_constructor_packet env_ar_par ctx params lc =
   let lc'' = Array.map (fun j -> it_mkProd_or_LetIn j.utj_val params) jlc in
   (* compute the max of the sorts of the products of the constructors types *)
   let levels = List.map (infos_and_sort env_ar_par ctx) lc in
-  let level = List.fold_left (fun max l -> Universe.sup max l) Universe.type0m levels in
-  (lc'',(is_unit levels,level))
+  let isunit = is_unit levels in
+  let min = if Array.length jlc > 1 then Universe.type0 else Universe.type0m in
+  let level = List.fold_left (fun max l -> Universe.sup max l) min levels in
+  (lc'', (isunit, level))
 
 (* If indices matter *)
 let cumulate_arity_large_levels env sign =
-- 
cgit v1.2.3