From c5e8c731ede28ba4f734bbd143c7d7e5a05c365a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 27 Oct 2006 17:32:45 +0000
Subject: Correction de 2 bugs critiques du polymorphisme d'univers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9301 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/indtypes.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 41ca4e6614..a41cc53beb 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -163,9 +163,13 @@ let small_unit constrsinfos =
    w1,w2,w3 <= u3
 *)   
 
+let extract_level (_,_,_,lc,lev) =
+  (* Enforce that the level is not in Prop if more than two constructors *)
+  if Array.length lc >= 2 then sup base_univ lev else lev
+
 let inductive_levels arities inds =
   let levels = Array.map pi3 arities in
-  let cstrs_levels = Array.map (fun (_,_,_,_,lev) -> lev) inds in
+  let cstrs_levels = Array.map extract_level inds in
   (* Take the transitive closure of the system of constructors *)
   (* level constraints and remove the recursive dependencies *)
   solve_constraints_system levels cstrs_levels
-- 
cgit v1.2.3