diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-26 18:50:37 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-26 18:50:37 +0000 |
| commit | 24e09baf09e006021e662529585b94fbf702dde5 (patch) | |
| tree | ff88b80a5a5f0d3f7841ba98872abbfbfe5d3d14 | |
| parent | 27c5ae44f84ce7d23a1c92a382d382c505464573 (diff) | |
sp au lieu de id dans END-SECTION
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@955 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/discharge.ml | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 48056f79c..562605d9f 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -258,15 +258,15 @@ let push_inductive_names ccitab sp mie = (*s Operations performed at section closing. *) -let cache_end_section (_,(s,mc)) = - Nametab.push_module s mc; - Nametab.open_module_contents s +let cache_end_section (_,(sp,mc)) = + Nametab.push_module sp mc; + Nametab.open_module_contents (qualid_of_sp sp) -let load_end_section (_,(s,mc)) = - Nametab.push_module s mc +let load_end_section (_,(sp,mc)) = + Nametab.push_module sp mc -let open_end_section (_,(s,_)) = - Nametab.rec_open_module_contents s +let open_end_section (_,(sp,_)) = + Nametab.rec_open_module_contents (qualid_of_sp sp) let (in_end_section, out_end_section) = declare_object @@ -288,8 +288,9 @@ let rec process_object (ccitab, objtab, modtab as tabs) = function (* Variables are never visible *) | "VARIABLE" -> tabs | "END-SECTION" -> - let (id,mc) = out_end_section obj in - (ccitab, objtab, Stringmap.add id mc modtab) + let (sp,mc) = out_end_section obj in + let id = string_of_id (basename sp) in + (ccitab, objtab, Stringmap.add id (sp,mc) modtab) (* All the rest is visible only at toplevel ??? *) (* Actually it is unsafe, it should be visible only in empty context *) (* ou quelque chose comme cela *) @@ -321,7 +322,7 @@ let close_section _ s = Global.pop_named_decls ids; Summary.unfreeze_lost_summaries fs; let mc = segment_contents decls in - add_anonymous_leaf (in_end_section (s,mc)); + add_anonymous_leaf (in_end_section (sec_sp,mc)); List.iter process_operation (List.rev ops) let save_module_to s f = |