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

14 files changed, 27 insertions, 24 deletions

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 04a23919b5..549e5e4fd0 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -74,7 +74,8 @@ let visit_ref v r =
 exception Impossible
 
 let check_arity env cb = 
-  if Reduction.is_arity env cb.const_type then raise Impossible
+  let t = Typeops.type_of_constant_type env cb.const_type in
+  if Reduction.is_arity env t then raise Impossible
 
 let check_fix env cb i = 
   match cb.const_body with 
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 857d3400a4..f725c2259c 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -225,7 +225,7 @@ let rec extract_type env db j c args =
     | Const kn -> 
 	let r = ConstRef kn in 
 	let cb = lookup_constant kn env in 
-	let typ = cb.const_type in 
+	let typ = Typeops.type_of_constant_type env cb.const_type in 
 	(match flag_of_type env typ with 
 	   | (Info, TypeScheme) -> 
 	       let mlt = extract_type_app env db (r, type_sign env typ) args in 
@@ -321,7 +321,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
       Array.map 
 	(fun mip ->
 	   let b = snd (mind_arity mip) <> InProp in
-	   let ar = Inductive.type_of_inductive (mib,mip) in
+	   let ar = Inductive.type_of_inductive env (mib,mip) in
 	   let s,v = if b then type_sign_vl env ar else [],[] in
 	   let t = Array.make (Array.length mip.mind_nf_lc) [] in 
 	   { ip_typename = mip.mind_typename;
@@ -401,7 +401,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	(* Is this record officially declared with its projections ? *)
 	(* If so, we use this information. *)
 	begin try 
-	  let n = nb_default_params env (Inductive.type_of_inductive(mib,mip0))
+	  let n = nb_default_params env
+            (Inductive.type_of_inductive env (mib,mip0))
 	  in
 	  List.iter 
 	    (option_iter 
@@ -446,7 +447,7 @@ and mlt_env env r = match r with
 	   | _ -> None
        with Not_found -> 
 	 let cb = Environ.lookup_constant kn env in
-	 let typ = cb.const_type in
+	 let typ = Typeops.type_of_constant_type env cb.const_type in 
 	 match cb.const_body with
 	   | None -> None
 	   | Some l_body -> 
@@ -473,7 +474,7 @@ let record_constant_type env kn opt_typ =
     lookup_type kn 
   with Not_found ->
     let typ = match opt_typ with 
-      | None -> constant_type env kn 
+      | None -> Typeops.type_of_constant env kn
       | Some typ -> typ 
     in let mlt = extract_type env [] 1 typ [] 
     in let schema = (type_maxvar mlt, mlt)
@@ -814,7 +815,7 @@ let extract_fixpoint env vkn (fi,ti,ci) =
 		 
 let extract_constant env kn cb = 
   let r = ConstRef kn in 
-  let typ = cb.const_type in
+  let typ = Typeops.type_of_constant_type env cb.const_type in 
   match cb.const_body with
     | None -> (* A logical axiom is risky, an informative one is fatal. *) 
         (match flag_of_type env typ with
@@ -846,7 +847,7 @@ let extract_constant env kn cb =
 
 let extract_constant_spec env kn cb = 
   let r = ConstRef kn in 
-  let typ = cb.const_type in
+  let typ = Typeops.type_of_constant_type env cb.const_type in 
   match flag_of_type env typ with 
     | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype))
     | (Logic, Default) -> Sval (r, Tdummy Kother) 
@@ -884,7 +885,7 @@ let extract_declaration env r = match r with
 type kind = Logical | Term | Type 
     
 let constant_kind env cb = 
-  match flag_of_type env cb.const_type with 
+  match flag_of_type env (Typeops.type_of_constant_type env cb.const_type) with 
     | (Logic,_) -> Logical
     | (Info,TypeScheme) -> Type
     | (Info,Default) -> Term
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 596f3ccb0b..47a0977a5e 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -441,7 +441,7 @@ let extract_constant_inline inline r ids s =
   match g with 
     | ConstRef kn -> 
 	let env = Global.env () in 
-	let typ = Environ.constant_type env kn in 
+	let typ = Typeops.type_of_constant env kn in 
 	let typ = Reduction.whd_betadeltaiota env typ in
 	if Reduction.is_arity env typ 
 	  then begin 
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index ab411cf11d..14e2233fe8 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -890,7 +890,8 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
 (*   observe (str "f_body_with_params_and_other_fun " ++  pr_lconstr f_body_with_params_and_other_fun); *)
   let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
 (*   observe (str "eq_rhs " ++  pr_lconstr eq_rhs); *)
-  let type_ctxt,type_of_f = Sign.decompose_prod_n_assum (nb_params + nb_args) f_def.const_type in
+  let type_ctxt,type_of_f = Sign.decompose_prod_n_assum (nb_params + nb_args) 
+    (Typeops.type_of_constant_type (Global.env()) f_def.const_type) in
   let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
   let lemma_type = it_mkProd_or_LetIn ~init:eqn type_ctxt in
   let f_id = id_of_label (con_label (destConst f)) in
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index c7f100c365..82bb286953 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -306,8 +306,7 @@ let generate_principle
 	  list_map_i
 	    (fun i x ->
 	       let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in 
-	       let princ_type = 
-		 (Global.lookup_constant princ).Declarations.const_type
+	       let princ_type = Typeops.type_of_constant (Global.env()) princ
 	       in
 	       Functional_principles_types.generate_functional_principle
 		 interactive_proof 
@@ -682,7 +681,8 @@ let make_graph (f_ref:global_reference) =
 	  with_full_print 
 	    (fun () -> 
 	       (Constrextern.extern_constr false env body, 
-		Constrextern.extern_type false env  c_body.const_type
+		Constrextern.extern_type false env
+                  (Typeops.type_of_constant_type env c_body.const_type)
 	       )
 	    )
 	    ()
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 40c90f5a1b..04110ea989 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -101,7 +101,7 @@ let id_to_constr id =
 
 let generate_type g_to_f f graph i = 
   (*i we deduce the number of arguments of the function and its returned type from the graph i*)
-  let graph_arity = Inductive.type_of_inductive (Global.lookup_inductive (destInd graph))  in 
+  let graph_arity = Inductive.type_of_inductive (Global.env()) (Global.lookup_inductive (destInd graph))  in 
   let ctxt,_ = decompose_prod_assum graph_arity in 
   let fun_ctxt,res_type = 
     match ctxt with 
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 9e45006865..dc27cf9836 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -92,7 +92,7 @@ let rec def_const_in_term_rec vl x =
    | Case(_,x,t,a) 
         -> def_const_in_term_rec vl x
    | Cast(x,_,t)-> def_const_in_term_rec vl t
-   | Const(c)  -> def_const_in_term_rec vl (lookup_constant c vl).const_type
+   | Const(c)  -> def_const_in_term_rec vl (Typeops.type_of_constant vl c)
    | _ -> def_const_in_term_rec vl (type_of vl Evd.empty x)
 ;;
 let def_const_in_term_ x =
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 8fcdb5d90a..730e055b4e 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -396,7 +396,7 @@ let inspect n =
 			 let (_, _, v) = get_variable (basename sp) in
 			   add_search2 (Nametab.locate (qualid_of_sp sp)) v
 		     | (sp,kn), "CONSTANT" ->
-			 let {const_type=typ} = Global.lookup_constant (constant_of_kn kn) in
+			 let typ = Typeops.type_of_constant (Global.env()) (constant_of_kn kn) in
 			   add_search2 (Nametab.locate (qualid_of_sp sp)) typ
 		     | (sp,kn), "MUTUALINDUCTIVE" ->
 			 add_search2 (Nametab.locate (qualid_of_sp sp))
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 6195caa472..9a503cfb5a 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -149,7 +149,7 @@ let make_definition_ast name c typ implicits =
 let constant_to_ast_list kn =
   let cb = Global.lookup_constant kn in
   let c = cb.const_body in
-  let typ = cb.const_type in
+  let typ = Typeops.type_of_constant_type (Global.env()) cb.const_type in
   let l = implicits_of_global (ConstRef kn) in
   (match c with
       None -> 
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 997821c53a..4bec73501f 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -725,7 +725,7 @@ let rec nsortrec vl x =
    | Case(_,x,t,a) 
         -> nsortrec vl x
    | Cast(x,_, t)-> nsortrec vl t
-   | Const c  -> nsortrec vl (lookup_constant c vl).const_type
+   | Const c  -> nsortrec vl (Typeops.type_of_constant vl c)
    | _ -> nsortrec vl (type_of vl Evd.empty x)
 ;;
 let nsort x =
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 0d7146e68f..353fcdb3bb 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -119,8 +119,7 @@ let def_of_const t =
 
 let type_of_const t =
    match (kind_of_term t) with
-    Const sp -> 
-      (Global.lookup_constant sp).const_type
+    Const sp -> Typeops.type_of_constant (Global.env()) sp
     |_ -> assert false
 
 let arg_type t =
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index f217b03719..ff07c3c47c 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -241,7 +241,7 @@ let typeur sigma metamap =
           Util.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound"))
     | T.Const c ->
         let cb = Environ.lookup_constant c env in
-        T.body_of_type cb.Declarations.const_type
+        Typeops.type_of_constant_type env (cb.Declarations.const_type)
     | T.Evar ev -> Evd.existential_type sigma ev
     | T.Ind ind -> T.body_of_type (Inductiveops.type_of_inductive env ind)
     | T.Construct cstr ->
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index a3336817e0..c7d3b4ff0c 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -122,7 +122,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
         Typeops.judge_of_variable env id
 	  
      | T.Const c ->
-        E.make_judge cstr (E.constant_type env c)
+        E.make_judge cstr (Typeops.type_of_constant env c)
 	  
      | T.Ind ind ->
         E.make_judge cstr (Inductiveops.type_of_inductive env ind)
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 2e490b4c0f..f286d2c8a5 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -408,7 +408,7 @@ let mk_inductive_obj sp mib packs variables nparams hyps finite =
        let {D.mind_consnames=consnames ;
             D.mind_typename=typename } = p
        in
-        let arity = Inductive.type_of_inductive (mib,p) in
+        let arity = Inductive.type_of_inductive (Global.env()) (mib,p) in
         let lc = Inductiveops.arities_of_constructors (Global.env ()) (sp,!tyno) in
         let cons =
          (Array.fold_right (fun (name,lc) i -> (name,lc)::i)
@@ -522,6 +522,7 @@ let print internal glob_ref kind xml_library_root =
        let id = N.id_of_label (N.con_label kn) in
        let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
         G.lookup_constant kn in
+       let typ = Typeops.type_of_constant_type (Global.env()) typ in
         Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps
     | Ln.IndRef (kn,_) ->
        let mib = G.lookup_mind kn in