Extension du polymorphisme de sorte au cas des définitions dans Type.

(suppression au passage d'un cast dans constant_entry_of_com - ce
n'est pas normal qu'on force le type s'il n'est pas déjà présent mais
en même temps il semble que ce cast serve pour rafraîchir les univers
algébriques...)


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

5 files changed, 39 insertions, 19 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 452639170..041187d84 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -23,7 +23,7 @@ open Reductionops
 
 let type_of_inductive env ind =
  let specif = Inductive.lookup_mind_specif env ind in
-  Inductive.type_of_inductive specif
+  Inductive.type_of_inductive env specif
 
 (* Return type as quoted by the user *)
 let type_of_constructor env cstr =
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 1756c8377..656f370ae 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -53,9 +53,7 @@ let typeur sigma metamap =
           body_of_type ty
         with Not_found ->
           anomaly ("type_of: variable "^(string_of_id id)^" unbound"))
-    | Const c ->
-        let cb = lookup_constant c env in
-        body_of_type cb.const_type
+    | 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)
@@ -76,6 +74,9 @@ let typeur sigma metamap =
     | 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
+        strip_outer_cast (subst_type env sigma t (Array.to_list args))
     | App(f,args) ->
         strip_outer_cast
           (subst_type env sigma (type_of env f) (Array.to_list args))
@@ -100,6 +101,9 @@ let typeur sigma metamap =
     | 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
+        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 _ ->
         anomaly "sort_of: Not a type (1)"
@@ -122,16 +126,24 @@ let typeur sigma metamap =
     let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in
     Inductive.type_of_inductive_knowing_parameters env mip argtyps
 
-  in type_of, sort_of, sort_family_of, type_of_inductive_knowing_parameters
+  and type_of_constant_knowing_parameters env cst args =
+    let t = constant_type env cst in
+    let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in
+    Typeops.type_of_constant_knowing_parameters env t argtyps
+
+  in type_of, sort_of, sort_family_of,
+     type_of_inductive_knowing_parameters, type_of_constant_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 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 _,_,_,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_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 900a96829..32b90cd86 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -36,3 +36,6 @@ 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 -> 
+  constr array -> types
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 57c83fa7e..d248ba70e 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -53,7 +53,7 @@ let rec execute env evd cstr =
         j_nf_evar (evars_of evd) (judge_of_variable env id)
 	  
     | Const c ->
-        make_judge cstr (nf_evar (evars_of evd) (constant_type env c))
+        make_judge cstr (nf_evar (evars_of evd) (type_of_constant env c))
 	  
     | Ind ind ->
 	make_judge cstr (nf_evar (evars_of evd) (type_of_inductive env ind))
@@ -90,12 +90,17 @@ let rec execute env evd cstr =
     | App (f,args) ->
         let jl = execute_array env evd args in
 	let j =
-	if isInd f then
-	  (* Sort-polymorphism of inductive types *)
-	  judge_of_inductive_knowing_parameters env (destInd f)
-	    (jv_nf_evar (evars_of evd) jl)
-	else
-	  execute env evd f
+	  match kind_of_term f with
+	    | Ind ind ->
+		(* Sort-polymorphism of inductive types *)
+		judge_of_inductive_knowing_parameters env ind
+		  (jv_nf_evar (evars_of evd) jl)
+	    | Const cst -> 
+		(* Sort-polymorphism of inductive types *)
+		judge_of_constant_knowing_parameters env cst
+		  (jv_nf_evar (evars_of evd) jl)
+	    | _ -> 
+		execute env evd f
 	in
 	fst (judge_of_apply env j jl)
 	    
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index fb05661d7..55f798de9 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -70,7 +70,7 @@ let construct_of_constr_block env tag typ =
 let constr_type_of_idkey env idkey =
   match idkey with
   | ConstKey cst ->
-      mkConst cst, (lookup_constant cst env).const_type
+      mkConst cst, Typeops.type_of_constant env cst
   | VarKey id -> 
       let (_,_,ty) = lookup_named id env in 
       mkVar id, ty
@@ -80,7 +80,7 @@ let constr_type_of_idkey env idkey =
       mkRel n, lift n ty
 
 let type_of_ind env ind = 
-  type_of_inductive (Inductive.lookup_mind_specif env ind)
+  type_of_inductive env (Inductive.lookup_mind_specif env ind)
 
 let build_branches_type env (mind,_ as _ind) mib mip params dep p =
   let rtbl = mip.mind_reloc_tbl in