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

1 files changed, 1 insertions, 18 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 94cd39760..d834504ab 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 ->