Réutilisation de l'infrastructure pour le polymorphisme d'univers des

constantes qui avait été mise en place pour la 8.1gamma puis abandonné
pour cause entre autres d'inefficacité. Cette fois, on restreind le
polymorphisme au seul cas d'alias vers un inductif.



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

4 files changed, 8 insertions, 8 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index cc5beb974e..a5cda5d133 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -129,6 +129,8 @@ let cook_constant env r =
     | PolymorphicArity (ctx,s) ->
 	let t = mkArity (ctx,Type s.poly_level) in
 	let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
-	Typeops.make_polymorphic_if_arity env typ in
+	let j = make_judge (force (Option.get body)) typ in
+	Typeops.make_polymorphic_if_constant_for_ind env j
+  in
   let boxed = Cemitcodes.is_boxed cb.const_body_code in
   (body, typ, cb.const_constraints, cb.const_opaque, boxed,false)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index aedc44ac8f..2b28a7147d 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -24,10 +24,7 @@ open Typeops
 
 let constrain_type env j cst1 = function
   | None ->
-(* To have definitions in Type polymorphic
-      make_polymorphic_if_arity env j.uj_type, cst1
-*) 
-      NonPolymorphicType j.uj_type, cst1
+      make_polymorphic_if_constant_for_ind env j, cst1
   | Some t -> 
       let (tj,cst2) = infer_type env t in
       let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 616349ba0a..53f230baae 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -135,10 +135,10 @@ let extract_context_levels env =
   List.fold_left
     (fun l (_,b,p) -> if b=None then extract_level env p::l else l) []
 
-let make_polymorphic_if_arity env t =
+let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} =
   let params, ccl = dest_prod_assum env t in
   match kind_of_term ccl with
-  | Sort (Type u) -> 
+  | Sort (Type u) when isInd (fst (decompose_app (whd_betadeltaiota env c))) ->
       let param_ccls = extract_context_levels env params in
       let s = { poly_param_levels = param_ccls; poly_level = u} in
       PolymorphicArity (params,s)
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index fe428230a7..5bb0dee1d2 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -105,5 +105,6 @@ val type_of_constant_knowing_parameters :
   env -> constant_type -> constr array -> types
 
 (* Make a type polymorphic if an arity *)
-val make_polymorphic_if_arity : env -> types -> constant_type
+val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment ->
+  constant_type