diff options
| author | herbelin | 2001-03-01 14:02:59 +0000 |
|---|---|---|
| committer | herbelin | 2001-03-01 14:02:59 +0000 |
| commit | 7b6ed1e95bef26f4ae85d7471985128c0dfdbc15 (patch) | |
| tree | a2beab552c8e57d5db2833494e5cc79e6374cc84 /library/library.ml | |
| parent | 2a9a43be51ac61e04ebf3fce902899155b48057f (diff) | |
Déplacement de qualid dans Nametab, hors du noyau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1419 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/library.ml')
| -rw-r--r-- | library/library.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/library/library.ml b/library/library.ml index 0ec028963f..d1e162affc 100644 --- a/library/library.ml +++ b/library/library.ml @@ -8,6 +8,7 @@ open Names open Environ open Libobject open Lib +open Nametab (*s Load path. *) @@ -27,7 +28,7 @@ type module_disk = { md_name : string; md_compiled_env : compiled_env; md_declarations : library_segment; - md_nametab : Nametab.module_contents; + md_nametab : module_contents; md_deps : (string * Digest.t * bool) list } (*s Modules loaded in memory contain the following informations. They are @@ -38,7 +39,7 @@ type module_t = { module_filename : load_path_entry * string; module_compiled_env : compiled_env; module_declarations : library_segment; - module_nametab : Nametab.module_contents; + module_nametab : module_contents; mutable module_opened : bool; mutable module_exported : bool; module_deps : (string * Digest.t * bool) list; @@ -117,7 +118,7 @@ let rec open_module force s = if force or not m.module_opened then begin List.iter (fun (m,_,exp) -> if exp then open_module force m) m.module_deps; open_objects m.module_declarations; - Nametab.open_module_contents (make_qualid [] (id_of_string s)); + open_module_contents (make_qualid [] (id_of_string s)); m.module_opened <- true end @@ -155,7 +156,7 @@ let rec load_module_from s f = Global.import m.module_compiled_env; load_objects m.module_declarations; let sp = Names.make_path lpe.coq_dirpath (id_of_string s) CCI in - Nametab.push_module sp m.module_nametab; + push_module sp m.module_nametab; modules_table := Stringmap.add s m !modules_table; m |