Branchement sur Objdef

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

2 files changed, 24 insertions, 23 deletions

diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 0451e3db1..8b8279a6a 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -156,7 +156,8 @@ type discharge_operation =
   | Constant of identifier * recipe * strength * opacity * bool
   | Inductive of mutual_inductive_entry * bool
   | Class of cl_typ * cl_info_typ
-  | Struc of inductive_path * struc_typ
+  | Struc of inductive_path * (unit -> struc_typ)
+  | Objdef of constant_path
   | Coercion of ((coe_typ * coe_info_typ) * cl_typ * cl_typ)
 
 (* Main function to traverse the library segment and compute the various
@@ -232,20 +233,17 @@ let process_object oldenv dir sec_sp
     | "STRUCTURE" ->
 	let ((sp,i),info) = outStruc lobj in
 	let newsp = recalc_sp dir sp in
-	let mib = Environ.lookup_mind sp oldenv in
-	let strobj =
+	let strobj () =
+	  let mib = Environ.lookup_mind newsp (Global.env ()) in
 	  { s_CONST = info.s_CONST;
 	    s_PARAM = (mind_nth_type_packet mib 0).mind_nparams;
 	    s_PROJ = List.map (option_app (recalc_sp dir)) info.s_PROJ } in
 	((Struc ((newsp,i),strobj))::ops, ids_to_discard, work_alist)
 
-    (***TODO
     | "OBJDEF1" -> 
 	let sp = outObjDef1 lobj in
-        let ((_,spid,_)) = repr_path sp in
-        begin try objdef_declare spid with _ -> () end;
-        (ids_to_discard,work_alist)
-    ***)
+	let new_sp = recalc_sp dir sp in
+        ((Objdef new_sp)::ops, ids_to_discard, work_alist)
 
     | _ -> (ops,ids_to_discard,work_alist)
 
@@ -272,7 +270,9 @@ let process_operation = function
   | Class (y1,y2) ->
       Lib.add_anonymous_leaf (inClass (y1,y2))
   | Struc (newsp,strobj) ->
-      Lib.add_anonymous_leaf (inStruc (newsp,strobj))
+      Lib.add_anonymous_leaf (inStruc (newsp,strobj ()))
+  | Objdef newsp ->
+      begin try Recordobj.objdef_declare (ConstRef newsp) with _ -> () end
   | Coercion y ->
       Lib.add_anonymous_leaf (inCoercion y) 
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index e204b6d92..67e06e950 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -854,17 +854,17 @@ let _ =
 	     | _ -> bad_vernac_args "DEFINITION"
 	   in 
 	   let local,stre,coe,objdef,idcoe = match kind with
-	     | "DEFINITION" -> false,NeverDischarge,false,false,false
-             | "COERCION" -> false,NeverDischarge,true,false,false
-             | "LCOERCION" -> true,make_strength_0(),true,false,false
-             | "LET" -> true,make_strength_2(),false,false,false
-             | "LOCAL" -> true,make_strength_0(),false,false,false
-             | "OBJECT" -> false,NeverDischarge,false,true,false
-             | "LOBJECT" -> true,make_strength_0(),false,true,false
-             | "OBJCOERCION" -> false,NeverDischarge,true,true,false
-             | "LOBJCOERCION" -> true,make_strength_0(),true,true,false
-             | "SUBCLASS" -> false,NeverDischarge,false,false,true
-             | "LSUBCLASS" -> true,make_strength_0(),false,false,true
+	     | "DEFINITION" -> false,NeverDischarge,   false,false,false
+             | "COERCION" ->   false,NeverDischarge,   true, false,false
+             | "LCOERCION" ->  true, make_strength_0(),true, false,false
+             | "LET" ->        true, make_strength_2(),false,false,false
+             | "LOCAL" ->      true, make_strength_0(),false,false,false
+             | "OBJECT" ->     false,NeverDischarge,   false,true, false
+             | "LOBJECT" ->    true, make_strength_0(),false,true, false
+             | "OBJCOERCION" -> false,NeverDischarge,  true, true, false
+             | "LOBJCOERCION" -> true,make_strength_0(),true,true, false
+             | "SUBCLASS" ->   false,NeverDischarge,   false,false,true
+             | "LSUBCLASS" ->  true, make_strength_0(),false,false,true
              | _       -> anomaly "Unexpected string"
 	   in 
 	   fun () ->
@@ -875,10 +875,11 @@ let _ =
                if not (is_silent()) then
 		 message ((string_of_id id) ^ " is now a coercion")
 	     end;
-	     if idcoe then
+	     if idcoe then begin
 	       let cl = Class.class_of_ref ref in
-	       Class.try_add_new_coercion_subclass cl stre;
-             (***TODO if objdef then Recordobj.objdef_declare id ***)
+	       Class.try_add_new_coercion_subclass cl stre
+	     end;
+             if objdef then Recordobj.objdef_declare ref
        | _ -> bad_vernac_args "DEFINITION")
 
 let _ =