diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-07-05 21:23:30 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-07-05 21:23:30 +0000 |
| commit | 7f8d4cf7dd30ab3d3f1e19094d85164adfc1931e (patch) | |
| tree | b46a26b5fa22535824357157641f321cc373f7e7 /toplevel/discharge.ml | |
| parent | cd9acfec55378cfe1651b910b93387724efe251d (diff) | |
Débogage discharge des coercions; nettoyage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1827 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/discharge.ml')
| -rw-r--r-- | toplevel/discharge.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index a4ab22eed..2b3fd2c5d 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -168,7 +168,7 @@ type discharge_operation = | Class of cl_typ * cl_info_typ | Struc of inductive_path * (unit -> struc_typ) | Objdef of constant_path - | Coercion of ((coe_typ * coe_info_typ) * cl_typ * cl_typ) + | Coercion of coercion_entry (* Main function to traverse the library segment and compute the various discharge operations. *) @@ -237,7 +237,7 @@ let process_object oldenv dir sec_sp if coercion_strength coeinfo = (DischargeAt sec_sp) then (ops,ids_to_discard,work_alist) else - let y = process_coercion sec_sp x in + let y = process_coercion sec_sp ids_to_discard x in ((Coercion y)::ops, ids_to_discard, work_alist) | "STRUCTURE" -> @@ -283,8 +283,7 @@ let process_operation = function 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) + | Coercion y -> add_new_coercion y let push_inductive_names ccitab sp mie = let _,ccitab = |