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, 31 insertions, 35 deletions

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