diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-05 23:06:33 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-05 23:06:33 +0000 |
| commit | 9759a74e3910ba12608f7bcddd40f7d97247dbcc (patch) | |
| tree | e473ca4d9858ba1316212d17217540e61e7b6ba4 /toplevel/discharge.ml | |
| parent | c9aa1b6d908d3a4f8d9906ba0f11c0bb11569ab7 (diff) | |
Restructuration de classops; évolution en une version mieux intégrée au reste du système; conséquences collatérales
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1327 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/discharge.ml')
| -rw-r--r-- | toplevel/discharge.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 8b8279a6a..a3c9586a4 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -216,7 +216,7 @@ let process_object oldenv dir sec_sp | "CLASS" -> let ((cl,clinfo) as x) = outClass lobj in - if clinfo.cL_STRE = (DischargeAt sec_sp) then + if clinfo.cl_strength = (DischargeAt sec_sp) then (ops,ids_to_discard,work_alist) else let (y1,y2) = process_class sec_sp ids_to_discard x in @@ -224,7 +224,7 @@ let process_object oldenv dir sec_sp | "COERCION" -> let (((_,coeinfo),_,_)as x) = outCoercion lobj in - if coeinfo.cOE_STRE = (DischargeAt sec_sp) then + if coercion_strength coeinfo = (DischargeAt sec_sp) then (ops,ids_to_discard,work_alist) else let y = process_coercion sec_sp x in @@ -298,8 +298,8 @@ let push_inductive_names ccitab sp mie = (*s Operations performed at section closing. *) let cache_end_section (_,(sp,mc)) = - Nametab.push_module sp mc; - Nametab.open_module_contents (qualid_of_sp sp) + Nametab.push_section sp mc; + Nametab.open_section_contents (qualid_of_sp sp) let load_end_section (_,(sp,mc)) = Nametab.push_module sp mc |