Compatibilité du polymorphisme de constantes avec les sections.

Amélioration affichage des univers. Réparation de petits oublis du premier
commit. Essai d'une nouvelle stratégie : si le type d'une constante
est mentionné explicitement, la constante est monomorphe dans Type.


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

7 files changed, 28 insertions, 32 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 68d301eb46..e6d7613b00 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -16,6 +16,7 @@ open Sign
 open Declarations
 open Environ
 open Reduction
+open Term_typing
 
 (*s Cooking the constants. *)
 
@@ -129,7 +130,6 @@ 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
-	let ctx,_ = dest_prod env typ in
-	PolymorphicArity (ctx,s) in
+	Typeops.make_polymorphic_if_arity env typ in
   let boxed = Cemitcodes.is_boxed cb.const_body_code in
   (body, typ, cb.const_constraints, cb.const_opaque, boxed)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 7dd9aa7864..fcb45befa0 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -122,14 +122,6 @@ where
 Remark: Set (predicative) is encoded as Type(0)
 *)
 
-let set_inductive_level env s t = 
-  let sign,s' = dest_prod_assum env t in
-  if family_of_sort s <> family_of_sort (destSort s') then
-    (* This induces reductions if user_arity <> nf_arity *)
-    mkArity (sign,s)
-  else
-    t
-
 let sort_as_univ = function
 | Type u -> u
 | Prop Null -> neutral_univ
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 9c75829d5b..012ddae775 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -80,8 +80,6 @@ val check_cofix : env -> cofixpoint -> unit
 val type_of_inductive_knowing_parameters :
   env -> one_inductive_body -> types array -> types
 
-val set_inductive_level : env -> sorts -> types -> types
-
 val max_inductive_sort : sorts array -> universe
 
 val instantiate_universes : env -> Sign.rel_context ->
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 94cd397607..d834504ab6 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -22,23 +22,6 @@ open Type_errors
 open Indtypes
 open Typeops
 
-let extract_level env p =
-  let _,c = dest_prod_assum env p in
-  match kind_of_term c with Sort (Type u) -> Some u | _ -> None
-
-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 params, ccl = dest_prod env t in
-  match kind_of_term ccl with
-  | Sort (Type u) -> 
-      let param_ccls = extract_context_levels env params in
-      let s = { poly_param_levels = param_ccls; poly_level = u} in
-      PolymorphicArity (params,s)
-  | _ -> NonPolymorphicType t
-
 let constrain_type env j cst1 = function
   | None ->
       make_polymorphic_if_arity env j.uj_type, cst1
@@ -46,7 +29,7 @@ let constrain_type env j cst1 = function
       let (tj,cst2) = infer_type env t in
       let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
       assert (t = tj.utj_val);
-      make_polymorphic_if_arity env t, Constraint.union (Constraint.union cst1 cst2) cst3
+      NonPolymorphicType t, Constraint.union (Constraint.union cst1 cst2) cst3
 
 let local_constrain_type env j cst1 = function
   | None ->
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 3c335d115b..9b8735fa72 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -125,6 +125,26 @@ let check_hyps id env hyps =
 *)
 (* Instantiation of terms on real arguments. *)
 
+(* Make a type polymorphic if an arity *)
+
+let extract_level env p =
+  let _,c = dest_prod_assum env p in
+  match kind_of_term c with Sort (Type u) -> Some u | _ -> None
+
+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 params, ccl = dest_prod_assum env t in
+  match kind_of_term ccl with
+  | Sort (Type u) -> 
+      let param_ccls = extract_context_levels env params in
+      let s = { poly_param_levels = param_ccls; poly_level = u} in
+      PolymorphicArity (params,s)
+  | _ ->
+      NonPolymorphicType t
+
 (* Type of constants *)
 
 let type_of_constant_knowing_parameters env t paramtyps =
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 43d7b33db7..9066e46d94 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -103,3 +103,6 @@ val type_of_constant_type : env -> constant_type -> types
 
 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
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 906354b04c..a58424d3d7 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -63,8 +63,8 @@ let pr_uni_level u = str (string_of_univ_level u)
 let pr_uni = function
   | Atom u -> 
       pr_uni_level u
-  | Max ([],[Base]) ->
-      int 1
+  | Max ([],[u]) ->
+      str "(" ++ pr_uni_level u ++ str ")+1"
   | Max (gel,gtl) ->
       str "max(" ++ hov 0
        (prlist_with_sep pr_coma pr_uni_level gel ++