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

15 files changed, 96 insertions, 89 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 68d301eb4..e6d7613b0 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 7dd9aa786..fcb45befa 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 9c75829d5..012ddae77 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 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 ->
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 3c335d115..9b8735fa7 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 43d7b33db..9066e46d9 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 906354b04..a58424d3d 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 ++
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 749534984..64953592b 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -330,10 +330,14 @@ let print_body = function
 let print_typed_body (val_0,typ) =
   (print_body val_0 ++ fnl () ++ str "     : " ++ pr_ltype typ ++ fnl ())
 
+let ungeneralized_type_of_constant_type = function
+  | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
+  | NonPolymorphicType t -> t
+
 let print_constant with_values sep sp =
   let cb = Global.lookup_constant sp in
   let val_0 = cb.const_body in
-  let typ = Typeops.type_of_constant_type (Global.env()) cb.const_type in
+  let typ = ungeneralized_type_of_constant_type cb.const_type in
   hov 0 (
     match val_0 with 
     | None -> 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a94dc0451..08e7fc150 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -392,14 +392,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	let resj =
 	  match evar_kind_of_term !isevars resj.uj_val with
 	  | App (f,args) ->
-              begin match evar_kind_of_term !isevars f with
-              | Ind ind ->
+              let f = whd_evar (Evd.evars_of !isevars) f in
+              begin match kind_of_term f with
+              | Ind _ | Const _ ->
 	          let sigma = evars_of !isevars in
-                  let args = Array.map (nf_evar sigma) args in
-	          let t = Retyping.type_of_inductive_knowing_parameters env sigma ind args in
-	          let s = snd (splay_arity env sigma t) in
-	          on_judgment_type (set_inductive_level env s) resj
-		(* Rem: no need to send sigma: no head evar, it's an arity *)
+		  let c = mkApp (f,Array.map (whd_evar sigma) args) in
+	          let t = Retyping.get_type_of env sigma c in
+		  make_judge c t
               | _ -> resj end
 	  | _ -> resj in
 	inh_conv_coerce_to_tycon loc env isevars resj tycon
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 656f370ae..5cc146036 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -17,6 +17,7 @@ open Reductionops
 open Environ
 open Typeops
 open Declarations
+open Termops
 
 let rec subst_type env sigma typ = function
   | [] -> typ
@@ -38,6 +39,11 @@ let sort_of_atomic_type env sigma ft args =
     | _ -> decomp_sort env sigma (subst_type env sigma ft (Array.to_list args))
   in concl_of_arity env ft
 
+let type_of_var env id =
+  try let (_,_,ty) = lookup_named id env in ty
+  with Not_found ->
+    anomaly ("type_of: variable "^(string_of_id id)^" unbound")
+
 let typeur sigma metamap =
   let rec type_of env cstr=
     match kind_of_term cstr with
@@ -47,16 +53,11 @@ let typeur sigma metamap =
     | Rel n ->
         let (_,_,ty) = lookup_rel n env in
         lift n ty
-    | Var id ->
-        (try
-          let (_,_,ty) = lookup_named id env in
-          body_of_type ty
-        with Not_found ->
-          anomaly ("type_of: variable "^(string_of_id id)^" unbound"))
+    | Var id -> type_of_var env id
     | Const cst -> Typeops.type_of_constant env cst
     | Evar ev -> Evd.existential_type sigma ev
-    | Ind ind -> body_of_type (type_of_inductive env ind)
-    | Construct cstr -> body_of_type (type_of_constructor env cstr)
+    | Ind ind -> type_of_inductive env ind
+    | Construct cstr -> type_of_constructor env cstr
     | Case (_,p,c,lf) ->
         let Inductiveops.IndType(_,realargs) =
           try Inductiveops.find_rectype env sigma (type_of env c)
@@ -71,11 +72,8 @@ let typeur sigma metamap =
          subst1 b (type_of (push_rel (name,Some b,c1) env) c2)
     | Fix ((_,i),(_,tys,_)) -> tys.(i)
     | CoFix (i,(_,tys,_)) -> tys.(i)
-    | App(f,args) when isInd f ->
-	let t = type_of_inductive_knowing_parameters env (destInd f) args in
-        strip_outer_cast (subst_type env sigma t (Array.to_list args))
-    | App(f,args) when isConst f ->
-	let t = type_of_constant_knowing_parameters env (destConst f) args in
+    | App(f,args) when isGlobalRef f ->
+	let t = type_of_global_reference_knowing_parameters env f args in
         strip_outer_cast (subst_type env sigma t (Array.to_list args))
     | App(f,args) ->
         strip_outer_cast
@@ -98,11 +96,8 @@ let typeur sigma metamap =
 	  | Prop Pos, (Type u2) -> Type (Univ.sup Univ.base_univ u2)
 	  | Prop Null, (Type _ as s) -> s
 	  | Type u1, Type u2 -> Type (Univ.sup u1 u2))
-    | App(f,args) when isInd f ->
-	let t = type_of_inductive_knowing_parameters env (destInd f) args in
-        sort_of_atomic_type env sigma t args
-    | App(f,args) when isConst f ->
-	let t = type_of_constant_knowing_parameters env (destConst f) args in
+    | App(f,args) when isGlobalRef f ->
+	let t = type_of_global_reference_knowing_parameters env f args in
         sort_of_atomic_type env sigma t args
     | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
     | Lambda _ | Fix _ | Construct _ ->
@@ -121,29 +116,30 @@ let typeur sigma metamap =
         anomaly "sort_of: Not a type (1)"
     | _ -> family_of_sort (decomp_sort env sigma (type_of env t))
 
-  and type_of_inductive_knowing_parameters env ind args =
-    let (_,mip) = lookup_mind_specif env ind in
-    let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in
-    Inductive.type_of_inductive_knowing_parameters env mip argtyps
-
-  and type_of_constant_knowing_parameters env cst args =
-    let t = constant_type env cst in
+  and type_of_global_reference_knowing_parameters env c args =
     let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in
-    Typeops.type_of_constant_knowing_parameters env t argtyps
+    match kind_of_term c with
+    | Ind ind ->
+      let (_,mip) = lookup_mind_specif env ind in
+      Inductive.type_of_inductive_knowing_parameters env mip argtyps
+    | Const cst ->
+      let t = constant_type env cst in
+      Typeops.type_of_constant_knowing_parameters env t argtyps
+    | Var id -> type_of_var env id
+    | Construct cstr -> type_of_constructor env cstr
+    | _ -> assert false
 
   in type_of, sort_of, sort_family_of,
-     type_of_inductive_knowing_parameters, type_of_constant_knowing_parameters
+     type_of_global_reference_knowing_parameters
 
-let get_type_of env sigma c = let f,_,_,_,_ = typeur sigma [] in f env c
-let get_sort_of env sigma t = let _,f,_,_,_ = typeur sigma [] in f env t
-let get_sort_family_of env sigma c = let _,_,f,_,_ = typeur sigma [] in f env c
-let type_of_inductive_knowing_parameters env sigma ind args =
-  let _,_,_,f,_ = typeur sigma [] in f env ind args
-let type_of_constant_knowing_parameters env sigma cst args =
-  let _,_,_,_,f = typeur sigma [] in f env cst args
+let get_type_of env sigma c = let f,_,_,_ = typeur sigma [] in f env c
+let get_sort_of env sigma t = let _,f,_,_ = typeur sigma [] in f env t
+let get_sort_family_of env sigma c = let _,_,f,_ = typeur sigma [] in f env c
+let type_of_global_reference_knowing_parameters env sigma c args =
+  let _,_,_,f = typeur sigma [] in f env c args
 
 let get_type_of_with_meta env sigma metamap = 
-  let f,_,_,_,_ = typeur sigma metamap in f env
+  let f,_,_,_ = typeur sigma metamap in f env
 
 (* Makes an assumption from a constr *)
 let get_assumption_of env evc c = c
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 32b90cd86..6dbd426b2 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -34,8 +34,6 @@ val get_assumption_of : env -> evar_map -> constr -> types
 (* Makes an unsafe judgment from a constr *)
 val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment
 
-val type_of_inductive_knowing_parameters : env -> evar_map -> inductive -> 
-  constr array -> types
-
-val type_of_constant_knowing_parameters : env -> evar_map -> constant -> 
+val type_of_global_reference_knowing_parameters : env -> evar_map -> constr -> 
   constr array -> types
+ 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 252961834..08c38f1b1 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -855,7 +855,12 @@ let next_global_ident_away allow_secvar id avoid =
   else  
     next_global_ident_from allow_secvar (lift_ident id) avoid
 
-(* Nouvelle version de renommage des variables (DEC 98) *)
+let isGlobalRef c = 
+  match kind_of_term c with
+  | Const _ | Ind _ | Construct _ | Var _ -> true
+  | _ -> false
+
+(* nouvelle version de renommage des variables (DEC 98) *)
 (* This is the algorithm to display distinct bound variables 
 
     - Règle 1 : un nom non anonyme, même non affiché, contribue à la liste
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index c635dc887..d461498d9 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -204,6 +204,8 @@ val global_vars_set_of_decl : env -> named_declaration -> Idset.t
 (* Test if an identifier is the basename of a global reference *)
 val is_section_variable : identifier -> bool
 
+val isGlobalRef : constr -> bool
+
 (* Combinators on judgments *)
 
 val on_judgment       : (types -> types) -> unsafe_judgment -> unsafe_judgment
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 5f765c962..33b22c3b7 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -292,14 +292,11 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
     | App (f,l) ->
 	let (acc',hdty) =
 	  match kind_of_term f with
-	    | Ind ind
+	    | (Ind _ | Const _)
 		when not (array_exists occur_meta l) (* we could be finer *) ->
-		(* Sort-polymorphism of inductive types *)
-		goalacc, type_of_inductive_knowing_parameters env sigma ind l
-	    | Const cst
-		when not (array_exists occur_meta l) (* we could be finer *) ->
-		(* Sort-polymorphism of inductive types *)
-		goalacc, type_of_constant_knowing_parameters env sigma cst l
+		(* Sort-polymorphism of definition and inductive types *)
+		goalacc, 
+		type_of_global_reference_knowing_parameters env sigma f l
 	    | _ -> 
 		mk_hdgoals sigma goal goalacc f
 	in
@@ -342,8 +339,10 @@ and mk_hdgoals sigma goal goalacc trm =
 
     | App (f,l) ->
 	let (acc',hdty) = 
-	  if isInd f & not (array_exists occur_meta l) (* we could be finer *)
-	  then (goalacc,type_of_inductive_knowing_parameters env sigma (destInd f) l)
+	  if isInd f or isConst f 
+	     & not (array_exists occur_meta l) (* we could be finer *)
+	  then
+	    (goalacc,type_of_global_reference_knowing_parameters env sigma f l)
 	  else mk_hdgoals sigma goal goalacc f
 	in
 	mk_arggoals sigma goal acc' hdty (Array.to_list l)
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
new file mode 100644
index 000000000..a49b927da
--- /dev/null
+++ b/test-suite/success/polymorphism.v
@@ -0,0 +1,8 @@
+(* Some tests of sort-polymorphisme *)
+Section S.
+Variable A:Type.
+Definition f (B:Type) := (A * B)%type.
+Inductive I (B:Type) : Type := prod : A->B->I B.
+End S.
+Check f nat nat : Set.
+Check I nat nat : Set.