bug #1951: polymorphic indtypes: universe subst was not performed in the type of the arguments; refiner: relaxed universe cstrs for poly indtypes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11433 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 12 insertions, 6 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 918a32c95..10e6569ca 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -147,7 +147,7 @@ let rec make_subst env = function
       let args = match args with _::args -> args | [] -> [] in
       let ctx,subst = make_subst env (sign, exp, args) in
       d::ctx, subst
-  | d::sign, Some u::exp, a::args ->
+  | (na,None,t as d)::sign, Some u::exp, a::args ->
       (* We recover the level of the argument, but we don't change the *)
       (* level in the corresponding type in the arity; this level in the *)
       (* arity is a global level which, at typing time, will be enforce *)
@@ -155,7 +155,8 @@ let rec make_subst env = function
       (* a useless extra constraint *)
       let s = sort_as_univ (snd (dest_arity env a)) in
       let ctx,subst = make_subst env (sign, exp, args) in
-      d::ctx, cons_subst u s subst
+      let t = actualize_decl_level env (Type s) t in
+      (na,None,t)::ctx, cons_subst u s subst
   | (na,None,t as d)::sign, Some u::exp, [] ->
       (* No more argument here: we instantiate the type with a fresh level *)
       (* which is first propagated to the corresponding premise in the arity *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 81b4a5e19..15f8b8a73 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -237,6 +237,12 @@ let check_conv_leq_goal env sigma arg ty conclty =
 let goal_type_of env sigma c =
   (if !check then type_of else Retyping.get_type_of) env sigma c
 
+let refresh_poly_universes c =
+  let (ctx,t) = decompose_prod_assum c in
+  let ctx' = List.map (fun (na,b,ty) -> (na,b,refresh_universes ty)) ctx in
+  let t' = refresh_universes t in
+  it_mkProd_or_LetIn t' ctx'
+
 let rec mk_refgoals sigma goal goalacc conclty trm =
   let env = evar_env goal in
   let hyps = goal.evar_hyps in
@@ -263,12 +269,11 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	let (acc',hdty) =
 	  match kind_of_term f with
 	    | Ind _ | Const _
-		when not (array_exists occur_meta l) (* we could be finer *)
-		  & (isInd f or has_polymorphic_type (destConst f))
-		  ->
+		when (isInd f or has_polymorphic_type (destConst f)) ->
 		(* Sort-polymorphism of definition and inductive types *)
 		goalacc, 
-		type_of_global_reference_knowing_parameters env sigma f l
+		refresh_poly_universes
+                  (type_of_global_reference_knowing_parameters env sigma f [||])
 	    | _ -> 
 		mk_hdgoals sigma goal goalacc f
 	in