diff options
| author | filliatr | 2000-11-24 17:30:06 +0000 |
|---|---|---|
| committer | filliatr | 2000-11-24 17:30:06 +0000 |
| commit | 3396e2d3a3abe0a740302a6e87b529a1ebcbc08e (patch) | |
| tree | c68aa163635d586fd9d34d19e29cbae51a72a65e /library/lib.ml | |
| parent | 4fd6bfd7204a2371f7b8f5c3a34fb2feaa273193 (diff) | |
Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametab
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@947 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/library/lib.ml b/library/lib.ml index 9b5ba27b7f..4dd0a36f20 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -11,7 +11,7 @@ type node = | Module of string | OpenedSection of string * Summary.frozen (* bool is to tell if the section must be opened automatically *) - | ClosedSection of bool * string * library_segment * Nametab.module_contents + | ClosedSection of bool * string * library_segment | FrozenState of Summary.frozen and library_entry = section_path * node @@ -137,7 +137,7 @@ let export_segment seg = in clean [] seg -let close_section export f s = +let close_section export s = let sp,fs = try match find_entry_p is_opened_section with | sp,OpenedSection (s',fs) -> @@ -150,12 +150,10 @@ let close_section export f s = lib_stk := before; let after' = export_segment after in pop_path_prefix (); - let contents = f fs sp after in - add_entry (make_path (id_of_string s) OBJ) - (ClosedSection (export, s,after',contents)); - Nametab.push_module s contents; - if export then Nametab.open_module_contents s; - add_frozen_state () + add_entry + (make_path (id_of_string s) OBJ) (ClosedSection (export, s,after')); + add_frozen_state (); + (sp,after,fs) (* The following function exports the whole library segment, that will be saved as a module. Objects are presented in chronological order, and |