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

1 files changed, 5 insertions, 1 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 41ca4e661..a41cc53be 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