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

9 files changed, 26 insertions, 14 deletions

diff --git a/CHANGES b/CHANGES
index 2fd30d416b..5a39cc7a21 100644
--- a/CHANGES
+++ b/CHANGES
@@ -18,6 +18,7 @@ Language
   (e.g. "Record stream := { hd : nat; tl : stream }.")
 - New syntax "Theorem id1:t1 ... with idn:tn" for proving mutually dependent
   statements.
+- Support for sort-polymorphism on constants denoting inductive types.
 
 Vernacular commands
 
@@ -100,8 +101,8 @@ Notations, coercions and implicit arguments
   (DOC TODO?)
 - New options Global and Local to "Implicit Arguments" for section
   surviving or non export outside module.
-- Level "constr" moved from 9 to 8 and notation "[ _ ]" now at level 0
-  (easy to fix in case of incompatibilites). (DOC TODO?)
+- Level "constr" moved from 9 to 8 and notation "[ _ ]" now reserved at level 0
+  (may need to move post-fixed uses of [ ] at level 8). (DOC TODO?)
 - Structure/Record now printed as Record (unless option Printing All is set).
 - Support for parametric notations defining constants.
 - Insertion of coercions below product types refrains to unfold
@@ -317,7 +318,7 @@ Syntax
 
 Language and commands
 
-- Added sort-polymorphism for definitions in Type.
+- Added sort-polymorphism for definitions in Type (but finally abandonned).
 - Support for implicit arguments in the types of parameters in
   (co-)fixpoints and (co-)inductive declarations.
 - Improved type inference: use as much of possible general information.
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
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 19df941b28..0c03d1b6a3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -411,7 +411,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  | App (f,args) ->
               let f = whd_evar (Evd.evars_of !evdref) f in
               begin match kind_of_term f with
-              | Ind _ (* | Const _ *) ->
+              | Ind _ | Const _
+		  when isInd f or has_polymorphic_type (destConst f)
+		    ->
 	          let sigma = evars_of !evdref in
 		  let c = mkApp (f,Array.map (whd_evar sigma) args) in
 	          let t = Retyping.get_type_of env sigma c in
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 124637e131..6d8946f440 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -877,6 +877,11 @@ let isGlobalRef c =
   | Const _ | Ind _ | Construct _ | Var _ -> true
   | _ -> false
 
+let has_polymorphic_type c =
+  match (Global.lookup_constant c).Declarations.const_type with
+  | Declarations.PolymorphicArity _ -> true
+  | _ -> false
+
 (* nouvelle version de renommage des variables (DEC 98) *)
 (* This is the algorithm to display distinct bound variables 
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index ded85464e9..608a7d9dbd 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -237,6 +237,8 @@ val is_section_variable : identifier -> bool
 
 val isGlobalRef : constr -> bool
 
+val has_polymorphic_type : constant -> bool
+
 (* Combinators on judgments *)
 
 val on_judgment       : (types -> types) -> unsafe_judgment -> unsafe_judgment
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 67bb3a3c21..654bc504a9 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -278,8 +278,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
     | App (f,l) ->
 	let (acc',hdty) =
 	  match kind_of_term f with
-	    | (Ind _ (* needed if defs in Type are polymorphic: | Const _*))
-		when not (array_exists occur_meta l) (* we could be finer *) ->
+	    | Ind _ | Const _
+		when not (array_exists occur_meta l) (* we could be finer *)
+		  & (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