diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-19 22:09:07 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-19 22:09:07 +0000 |
| commit | 69491a2ef1e21fe2a3678681868f7f364058fbd0 (patch) | |
| tree | f0b8763ea686674c745b54a794c69f9538ab888e /toplevel | |
| parent | 7326d3fd7ba13dcf815e11dcdde1bd81257bdfce (diff) | |
Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIRE
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6330 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/discharge.ml | 10 | ||||
| -rwxr-xr-x | toplevel/recordobj.ml | 7 |
2 files changed, 8 insertions, 9 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 443fd61e1..adca0d47d 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -195,7 +195,7 @@ type discharge_operation = Dischargedhypsmap.discharged_hyps | Class of cl_typ * cl_info_typ | Struc of inductive * (unit -> struc_typ) - | Objdef of constant + | CanonStruc of constant | Coercion of coercion_entry | Require of library_reference | Constraints of Univ.constraints @@ -275,10 +275,10 @@ let process_object oldenv olddir full_olddir newdir s_PROJ = List.map (option_app (fun kn -> recalc_con newdir kn)) info.s_PROJ } in ((Struc ((newkn,i),strobj))::ops, ids_to_discard, work_alist) - | "OBJDEF1" -> - let kn = outObjDef1 lobj in + | "CANONICAL-STRUCTURE" -> + let kn = outCanonicalStructure lobj in let new_kn = recalc_con newdir kn in - ((Objdef new_kn)::ops, ids_to_discard, work_alist) + ((CanonStruc new_kn)::ops, ids_to_discard, work_alist) | "REQUIRE" -> let c = out_require lobj in @@ -306,7 +306,7 @@ let process_operation = function Lib.add_anonymous_leaf (inClass (y1,y2)) | Struc (newsp,strobj) -> Lib.add_anonymous_leaf (inStruc (newsp,strobj ())) - | Objdef newsp -> + | CanonStruc newsp -> begin try Recordobj.objdef_declare (ConstRef newsp) with _ -> () end | Coercion y -> add_new_coercion y | Require y -> reload_library y diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml index 918909c79..6457fb538 100755 --- a/toplevel/recordobj.ml +++ b/toplevel/recordobj.ml @@ -68,9 +68,8 @@ let objdef_declare ref = try (ConstRef proji_sp, reference_of_constr c, args) :: l with Not_found -> l) [] lps in - add_anonymous_leaf (inObjDef1 sp); - List.iter - (fun (refi,c,argj) -> add_new_objdef ((refi,c),v,lt,params,argj)) - comp + let comp' = List.map (fun (refi,c,argj) -> + (refi,c),{o_DEF=v; o_TABS=lt; o_TPARAMS=params; o_TCOMPS=argj}) comp in + add_canonical_structure (sp, comp') let add_object_hook _ = objdef_declare |