Mise en place d'une méthode directe pour indiquer le type des déclarations à toplevel plutôt que de passer par mkCast

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

7 files changed, 31 insertions, 29 deletions

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 79348a7040..7b6303130b 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -861,8 +861,10 @@ let print_object lobj id sp dn fv env =
           let (_,(_,varentry,_)) = Declare.out_variable lobj in
            begin
             match varentry with
-               Declare.SectionLocalDef body ->
-                let typ = Retyping.get_type_of env Evd.empty body in
+               Declare.SectionLocalDef (body,optt) ->
+                 let typ = match optt with
+		   | None -> Retyping.get_type_of env Evd.empty body 
+		   | Some t -> t in
                  add_to_pvars (Definition (N.string_of_id id, body, typ)) ;
                  print_variable id (Some body) typ env inner_types
              | Declare.SectionLocalAssum typ ->
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c770e0237a..fdb7c0d0c1 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -38,10 +38,15 @@ let empty_environment = empty_env
 (* Insertion of variables (named and de Bruijn'ed). They are now typed before
    being added to the environment. *)
 
-let push_rel_or_named_def push (id,b) env =
+let push_rel_or_named_def push (id,b,topt) env =
   let (j,cst) = safe_infer env b in
+  let (t,cst) = match topt with
+    | None -> j.uj_type, cst
+    | Some t -> 
+	let (jt,cstt) = safe_infer_type env t in
+	jt.utj_val, Constraint.union cst cstt in
   let env' = add_constraints cst env in
-  let env'' = push (id,Some j.uj_val,j.uj_type) env' in
+  let env'' = push (id,Some j.uj_val,t) env' in
   (cst,env'')
 
 let push_named_def = push_rel_or_named_def push_named_decl
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 5f6697b4eb..36c2bbb23a 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -30,7 +30,7 @@ val push_named_assum :
   identifier * types -> safe_environment ->
     Univ.constraints * safe_environment
 val push_named_def :
-  identifier * constr -> safe_environment ->
+  identifier * constr * types option -> safe_environment ->
     Univ.constraints * safe_environment
 val pop_named_decls : identifier list -> safe_environment -> safe_environment
 
diff --git a/library/declare.ml b/library/declare.ml
index 816a456154..542bd6b946 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -66,8 +66,8 @@ let make_strength_2 () =
 (* Section variables. *)
 
 type section_variable_entry =
-  | SectionLocalDef of constr
-  | SectionLocalAssum of constr
+  | SectionLocalDef of constr * types option
+  | SectionLocalAssum of types
 
 type variable_declaration = dir_path * section_variable_entry * strength
 
@@ -90,7 +90,7 @@ let cache_variable (sp,(id,(p,d,str))) =
     errorlabstrm "cache_variable" [< pr_id id; 'sTR " already exists" >];
   let cst = match d with (* Fails if not well-typed *)
     | SectionLocalAssum ty -> Global.push_named_assum (id,ty)
-    | SectionLocalDef c -> Global.push_named_def (id,c) in
+    | SectionLocalDef (c,t) -> Global.push_named_def (id,c,t) in
   let (_,bd,ty) = Global.lookup_named id in
   let vd = (bd,ty,cst) in
   Nametab.push 0 (restrict_path 0 sp) (VarRef id);
diff --git a/library/declare.mli b/library/declare.mli
index c57dd2079c..bb903a9c46 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -32,8 +32,8 @@ type strength =
   | NeverDischarge
 
 type section_variable_entry =
-  | SectionLocalDef of constr
-  | SectionLocalAssum of constr
+  | SectionLocalDef of constr * types option
+  | SectionLocalAssum of types
 
 type variable_declaration = dir_path * section_variable_entry * strength
 
diff --git a/library/global.mli b/library/global.mli
index 6e352e2f8f..f10ab98a5a 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -29,7 +29,7 @@ val named_context : unit -> Sign.named_context
 
 (* Extending env with variables, constants and inductives *)
 val push_named_assum : (identifier * types) -> Univ.constraints
-val push_named_def   : (identifier * constr) -> Univ.constraints
+val push_named_def   : (identifier * constr * types option) -> Univ.constraints
 val pop_named_decls  : identifier list -> unit
 
 val add_parameter           : constant -> types -> unit
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1089539c4a..5906d75202 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -64,11 +64,6 @@ let red_constant_entry ce = function
       { ce with const_entry_body = 
 	  reduction_of_redexp red (Global.env()) Evd.empty body }
 
-let constr_of_constr_entry ce =
-  match ce.const_entry_type with
-    | None -> ce.const_entry_body 
-    | Some t -> mkCast (ce.const_entry_body, t)
-
 let declare_global_definition ident ce n local =
   let sp = declare_constant ident (ConstantEntry ce,n) in
   if local then
@@ -83,8 +78,8 @@ let definition_body_red red_option ident (local,n) com comtypeopt =
     | NeverDischarge -> declare_global_definition ident ce' n local
     | DischargeAt (disch_sp,_) ->
         if Lib.is_section_p disch_sp then begin
-	  let c = constr_of_constr_entry ce' in
-          let sp = declare_variable ident (Lib.cwd(),SectionLocalDef c,n) in
+	  let c = SectionLocalDef(ce'.const_entry_body,ce'.const_entry_type) in
+          let sp = declare_variable ident (Lib.cwd(), c, n) in
 	  if_verbose message ((string_of_id ident) ^ " is defined");
           if Pfedit.refining () then 
             mSGERRNL [< 'sTR"Warning: Local definition "; pr_id ident; 
@@ -254,8 +249,8 @@ let collect_non_rec env =
 	    | _ -> [] (* nrec=[] for cofixpoints *)
         with Failure "list_chop" -> []
       in 
-      searchrec ((f,mkCast (def,body_of_type ar))::lnonrec) 
-        (lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv
+      searchrec ((f,def,ar)::lnonrec) 
+	(lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv
     with Failure "try_find_i" -> 
       (List.rev lnonrec,
        (Array.of_list lnamerec, Array.of_list ldefrec,
@@ -318,9 +313,9 @@ let build_recursive lnameargsardef =
   let var_subst id = (id, global_reference id) in
   let _ = 
     List.fold_left
-      (fun subst (f,def) ->
+      (fun subst (f,def,t) ->
 	 let ce = { const_entry_body = replace_vars subst def;
-		    const_entry_type = None;
+		    const_entry_type = Some t;
                     const_entry_opaque = false } in
 	 let _ = declare_constant f (ConstantEntry ce,n) in
       	 warning ((string_of_id f)^" is non-recursively defined");
@@ -350,9 +345,9 @@ let build_corecursive lnameardef =
   let arityl = List.rev arityl in
   let recdef =
     try 
-      List.map (fun (_,arityc,def) -> 
-                  interp_constr sigma rec_sign
-                    (mkCastC(def,arityc)))
+      List.map (fun (_,arityc,def) ->
+		  let arity = interp_constr sigma rec_sign arityc in
+                  interp_casted_constr sigma rec_sign def arity)
         lnameardef
     with e -> 
       States.unfreeze fs; raise e 
@@ -380,9 +375,9 @@ let build_corecursive lnameardef =
   let var_subst id = (id, global_reference id) in
   let _ = 
     List.fold_left
-      (fun subst (f,def) ->
+      (fun subst (f,def,t) ->
 	 let ce = { const_entry_body = replace_vars subst def;
-		    const_entry_type = None;
+		    const_entry_type = Some t;
                     const_entry_opaque = false } in
 	 let _ = declare_constant f (ConstantEntry ce,n) in
       	 warning ((string_of_id f)^" is non-recursively defined");
@@ -454,8 +449,8 @@ let save id const strength =
        const_entry_opaque = opacity } = const in
   begin match strength with
     | DischargeAt (disch_sp,_) when Lib.is_section_p disch_sp && not opacity ->
-	let c = constr_of_constr_entry const in
-	let _ = declare_variable id (Lib.cwd(),SectionLocalDef c,strength)
+	let c = SectionLocalDef (pft, tpo) in
+	let _ = declare_variable id (Lib.cwd(), c, strength)
         in ()
     | NeverDischarge | DischargeAt _ ->
         let _ = declare_constant id (ConstantEntry const,strength)