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

5 files changed, 47 insertions, 47 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a94dc0451a..08e7fc1505 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 656f370aea..5cc1460369 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 32b90cd864..6dbd426b24 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 252961834f..08c38f1b14 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 c635dc887a..d461498d9e 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