Parsing

- Typage renforcé dans les grammaires (distinction des vars et des metavars)
- Disparition de SLAM au profit de ABSTRACT
- Paths primitifs dans les quotations (syntaxe concrète à base de .)
- Mise en place de identifier dès le type ast
- Protection de identifier contre les effets de bord via un String.copy
- Utilisation de module_ident (= identifier) dans les dir_path (au
  lieu de string)

Table des noms qualifiés

- Remplacement de la table de visibilité par une table qui ne cache
  plus les noms de modules et sections mais seulement les noms des
  constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel
  module A déjà existant : seuls les noms de constructions de l'ancien
  A qui existent aussi dans le nouveau A seront cachés)
- Renoncement à la possibilité d'accéder les formes non déchargées des
  constantes définies à l'intérieur de sections et simplification
  connexes (suppression de END-SECTION, une seule table de noms qui ne
  survit pas au discharge)
- Utilisation de noms longs pour les modules, de noms qualifiés pour
  Require and co, tests de cohérence; pour être cohérent avec la non
  survie des tables de noms à la sortie des section, les require à
  l'intérieur d'une section eux aussi sont refaits à la fermeture de la
  section


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1889 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 572 insertions, 316 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 34e0c1a12..b360d8e01 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -23,6 +23,7 @@ open Lib
 open Impargs
 open Indrec
 open Nametab
+open Library
 
 type strength = 
   | NotDeclare
@@ -81,7 +82,7 @@ let cache_variable (sp,(id,(d,_,_) as vd)) =
     | SectionLocalAssum ty -> Global.push_named_assum (id,ty)
     | SectionLocalDef c -> Global.push_named_def (id,c)
   end;
-  Nametab.push_local sp (VarRef sp);
+  Nametab.push_short_name id (VarRef sp);
   vartab := let (m,l) = !vartab in (Spmap.add sp vd m, sp::l)
 
 let (in_variable, out_variable) =
@@ -105,11 +106,17 @@ let cache_parameter (sp,c) =
     errorlabstrm "cache_parameter"
       [< pr_id (basename sp); 'sTR " already exists" >];
   Global.add_parameter sp c (current_section_context ());
-  Nametab.push sp (ConstRef sp)
+  Nametab.push sp (ConstRef sp);
+  Nametab.push_short_name (basename sp) (ConstRef sp)
 
-let load_parameter _ = ()
+let load_parameter (sp,_) =
+  if Nametab.exists_cci sp then
+    errorlabstrm "cache_parameter"
+      [< pr_id (basename sp); 'sTR " already exists" >];
+  Nametab.push sp (ConstRef sp)
 
-let open_parameter (sp,_) = ()
+let open_parameter (sp,_) =
+  Nametab.push_short_name (basename sp) (ConstRef sp)
 
 let export_parameter x = Some x
 
@@ -155,13 +162,19 @@ let cache_constant (sp,(cdt,stre,op)) =
     | ConstantRecipe r -> Global.add_discharged_constant sp r sc
   end;
   Nametab.push sp (ConstRef sp);
+  Nametab.push_short_name (basename sp) (ConstRef sp);
   if op then Global.set_opaque sp;
   csttab := Spmap.add sp stre !csttab
 
 let load_constant (sp,(ce,stre,op)) =
-  csttab := Spmap.add sp stre !csttab
+  if Nametab.exists_cci sp then
+    errorlabstrm "cache_constant"
+      [< pr_id (basename sp); 'sTR " already exists" >] ;
+  csttab := Spmap.add sp stre !csttab;
+  Nametab.push sp (ConstRef sp)
 
-let open_constant (sp,_) = ()
+let open_constant (sp,_) =
+  Nametab.push_short_name (basename sp) (ConstRef sp)
 
 let export_constant x = Some x
 
@@ -216,11 +229,17 @@ let cache_inductive (sp,mie) =
   let names = inductive_names sp mie in
   List.iter check_exists_inductive names;
   Global.add_mind sp mie (current_section_context ());
-  List.iter (fun (sp, ref) -> Nametab.push sp ref) names
+  List.iter (fun (sp, ref) -> Nametab.push sp ref; Nametab.push_short_name
+  (basename sp) ref) names
 
-let load_inductive _ = ()
+let load_inductive (sp,mie) =
+  let names = inductive_names sp mie in
+  List.iter check_exists_inductive names;
+  List.iter (fun (sp, ref) -> Nametab.push sp ref) names
 
-let open_inductive (sp,mie) = ()
+let open_inductive (sp,mie) =
+  let names = inductive_names sp mie in
+  List.iter (fun (sp, ref) -> Nametab.push_short_name (basename sp) ref) names
 
 let export_inductive x = Some x
 
@@ -481,8 +500,7 @@ let elimination_suffix = function
   | Prop Null -> "_ind"
   | Prop Pos  -> "_rec"
 
-let make_elimination_ident id s = 
-  id_of_string ((string_of_id id) ^ (elimination_suffix s))
+let make_elimination_ident id s = add_suffix id (elimination_suffix s)
   
 let declare_one_elimination mispec =
   let mindstr = string_of_id (mis_typename mispec) in
@@ -524,7 +542,7 @@ let declare_eliminations sp =
 
 let lookup_eliminator env path s =
   let dir, base,k = repr_path path in
-  let id = id_of_string ((string_of_id base)^(elimination_suffix s)) in
+  let id = add_suffix base (elimination_suffix s) in
   (* Try first to get an eliminator defined in the same section as the *)
   (* inductive type *)
   try construct_absolute_reference env (Names.make_path dir id k)
diff --git a/library/declare.mli b/library/declare.mli
index ad462534f..9bbd0b8f4 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -14,6 +14,7 @@ open Term
 open Sign
 open Declarations
 open Inductive
+open Library
 (*i*)
 
 (* This module provides the official functions to declare new variables, 
@@ -23,7 +24,7 @@ open Inductive
    reset works properly --- and will fill some global tables such as 
    [Nametab] and [Impargs]. *)
 
-type strength =
+type strength = 
   | NotDeclare
   | DischargeAt of dir_path
   | NeverDischarge
@@ -64,7 +65,7 @@ val declare_eliminations : mutual_inductive_path -> unit
 
 val out_inductive : Libobject.obj -> mutual_inductive_entry 
 
-val make_strength : string list -> strength
+val make_strength : dir_path -> strength
 val make_strength_0 : unit -> strength
 val make_strength_1 : unit -> strength
 val make_strength_2 : unit -> strength
diff --git a/library/global.ml b/library/global.ml
index b4f45ad69..ea5506969 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -31,7 +31,7 @@ let _ =
     { freeze_function = (fun () -> !global_env);
       unfreeze_function = (fun fr -> global_env := fr);
       init_function = (fun () -> global_env := empty_environment);
-      survive_section = true }
+      survive_section = false }
 
 (* Then we export the functions of [Typing] on that environment. *)
 
diff --git a/library/global.mli b/library/global.mli
index c463bd153..51acc840e 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -50,7 +50,7 @@ val lookup_mind_specif : inductive -> inductive_instance
 val set_opaque : section_path -> unit
 val set_transparent : section_path -> unit
 
-val export : string -> compiled_env
+val export : dir_path -> compiled_env
 val import : compiled_env -> unit
 
 (*s Some functions of [Environ] instanciated on the global environment. *)
diff --git a/library/lib.ml b/library/lib.ml
index 9438713d6..8fc7a4e9c 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -17,9 +17,9 @@ open Summary
 type node = 
   | Leaf of obj
   | Module of dir_path
-  | OpenedSection of string * Summary.frozen
+  | OpenedSection of module_ident * Summary.frozen
   (* bool is to tell if the section must be opened automatically *)
-  | ClosedSection of bool * string * library_segment
+  | ClosedSection of bool * module_ident * library_segment
   | FrozenState of Summary.frozen
 
 and library_entry = section_path * node
@@ -36,16 +36,16 @@ and library_segment = library_entry list
 
 let lib_stk = ref ([] : (section_path * node) list)
 
+let default_module = make_dirpath [id_of_string "Scratch"]
 let module_name = ref None
-let path_prefix = ref ([Nametab.default_root] : dir_path)
+let path_prefix = ref (default_module : dir_path)
 
 let module_sp () =
-  match !module_name with Some m -> m | None -> [Nametab.default_root]
+  match !module_name with Some m -> m | None -> default_module
 
 let recalc_path_prefix () =
   let rec recalc = function
-    | (sp, OpenedSection _) :: _ ->
-	let (pl,id,_) = repr_path sp in pl@[string_of_id id]
+    | (sp, OpenedSection (modid,_)) :: _ -> (dirpath sp)@[modid]
     | _::l -> recalc l
     | [] -> module_sp ()
   in
@@ -112,12 +112,13 @@ let contents_after = function
 
 (* Sections. *)
 
-let open_section s =
-  let sp = make_path (id_of_string s) OBJ in
-  if Nametab.exists_module sp then
-    errorlabstrm "open_section" [< 'sTR (s^" already exists") >];
-  add_entry sp (OpenedSection (s, freeze_summaries()));
-  path_prefix := !path_prefix @ [s];
+let open_section id =
+  let dir = !path_prefix @ [id] in
+  let sp = make_path id OBJ in
+  if Nametab.exists_section dir then
+    errorlabstrm "open_section" [< pr_id id; 'sTR " already exists" >];
+  add_entry sp (OpenedSection (id, freeze_summaries()));
+  path_prefix := dir;
   sp
 
 let check_for_module () =
@@ -130,13 +131,23 @@ let check_for_module () =
 let start_module s =
   if !module_name <> None then
     error "a module is already started";
-  if !path_prefix <> [Nametab.default_root] then
+  if !path_prefix <> default_module then
     error "some sections are already opened";
   module_name := Some s;
+  (match split_dirpath s with [],id -> Nametab.push_library_root id | _ -> ());
   Univ.set_module s;
   let _ = add_anonymous_entry (Module s) in
   path_prefix := s
 
+let end_module s =
+  match !module_name with
+    | None -> error "no module declared"
+    | Some m ->
+	let bm = snd (split_dirpath m) in
+	if bm <> s then
+	  error ("The current open module has basename "^(string_of_id bm));
+	m
+
 let is_opened_section = function (_,OpenedSection _) -> true | _ -> false
 
 let sections_are_opened () =
@@ -156,11 +167,11 @@ let export_segment seg =
   in
   clean [] seg
 
-let close_section export s =
+let close_section export id =
   let sp,fs = 
     try match find_entry_p is_opened_section with
-      | sp,OpenedSection (s',fs) -> 
-	  if s <> s' then error "this is not the last opened section"; (sp,fs)
+      | sp,OpenedSection (id',fs) -> 
+	  if id<>id' then error "this is not the last opened section"; (sp,fs)
       | _ -> assert false
     with Not_found ->
       error "no opened section"
@@ -169,16 +180,14 @@ let close_section export s =
   lib_stk := before;
   let after' = export_segment after in
   pop_path_prefix ();
-  add_entry 
-    (make_path (id_of_string s) OBJ) (ClosedSection (export, s,after'));
+  add_entry (make_path id OBJ) (ClosedSection (export, id, after'));
   (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
    frozen states are removed. *)
 
-let export_module f =
-  if !module_name = None then error "no module declared";
+let export_module s =
   export_segment !lib_stk
 
 (* Backtracking. *)
@@ -214,8 +223,8 @@ let reset_name id =
 
 (* [dir] is a section dir if [module] < [dir] <= [path_prefix] *)
 let is_section_p sp =
-  not (dirpath_prefix_of sp (module_sp ()))
-  & (dirpath_prefix_of sp !path_prefix)
+  not (is_dirpath_prefix_of sp (module_sp ()))
+  & (is_dirpath_prefix_of sp !path_prefix)
 
 (* State and initialization. *)
 
diff --git a/library/lib.mli b/library/lib.mli
index 9b5326db1..b22839a3d 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -21,8 +21,8 @@ open Summary
 type node = 
   | Leaf of obj
   | Module of dir_path
-  | OpenedSection of string * Summary.frozen
-  | ClosedSection of bool * string * library_segment
+  | OpenedSection of module_ident * Summary.frozen
+  | ClosedSection of bool * module_ident * library_segment
   | FrozenState of Summary.frozen
 
 and library_entry = section_path * node
@@ -47,9 +47,9 @@ val contents_after : section_path option -> library_segment
 
 (*s Opening and closing a section. *)
 
-val open_section : string -> section_path
+val open_section : identifier -> section_path
 val close_section : 
-  export:bool -> string -> section_path * library_segment * Summary.frozen
+  export:bool -> identifier -> section_path * library_segment * Summary.frozen
 val sections_are_opened : unit -> bool
 
 val make_path : identifier -> path_kind -> section_path
@@ -57,7 +57,8 @@ val cwd : unit -> dir_path
 val is_section_p : dir_path -> bool
 
 val start_module : dir_path -> unit
-val export_module : unit -> library_segment
+val end_module : module_ident -> dir_path
+val export_module : dir_path -> library_segment
 
 
 (*s Backtracking (undo). *)
diff --git a/library/library.ml b/library/library.ml
index a6b7b5012..5556bf32e 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -10,7 +10,7 @@
 
 open Pp
 open Util
-open System
+
 open Names
 open Environ
 open Libobject
@@ -19,72 +19,112 @@ open Nametab
 
 (*s Load path. *)
 
-let load_path = ref ([] : load_path)
+type logical_path = dir_path
+
+let load_path = ref ([],[] : System.physical_path list * logical_path list)
 
-let get_load_path () = !load_path
+let get_load_path () = fst !load_path
 
-let add_load_path_entry lpe = load_path := lpe :: !load_path
+let find_logical_path dir = 
+  match list_filter2 (fun p d -> p = dir) !load_path with
+  | _,[dir] -> dir
+  | _ -> anomaly ("Two logical paths are associated to "^dir)
 
 let remove_path dir =
-  load_path := List.filter (fun lpe -> lpe.directory <> dir) !load_path
+  load_path := list_filter2 (fun p d -> p <> dir) !load_path
+
+let add_load_path_entry (phys_path,coq_path) =
+  match list_filter2 (fun p d -> p = phys_path) !load_path with
+  | _,[dir] ->
+      if dir <> coq_path && coq_path <> Nametab.default_root_prefix then
+	  (* Assume the user is concerned by module naming *)
+	begin
+	  if dir <> Nametab.default_root_prefix then
+	    warning (phys_path^" was previously bound to "
+	    ^(string_of_dirpath dir)
+	    ^("\nIt is remapped to "^(string_of_dirpath coq_path)));
+	  remove_path phys_path;
+	  load_path := (phys_path::fst !load_path, coq_path::snd !load_path)
+	end
+  | _,[] ->
+      load_path := (phys_path :: fst !load_path, coq_path :: snd !load_path)
+  | _ -> anomaly ("Two logical paths are associated to "^phys_path)
+
+let physical_paths (dp,lp) = dp
+
+let load_path_of_logical_path dir =
+  fst (list_filter2 (fun p d -> d = dir) !load_path)
+
+let get_full_load_path () = List.combine (fst !load_path) (snd !load_path)
 
 (*s Modules on disk contain the following informations (after the magic 
     number, and before the digest). *)
 
+type compilation_unit_name = dir_path
+
 type module_disk = { 
-  md_name : string;
+  md_name : compilation_unit_name;
   md_compiled_env : compiled_env;
   md_declarations : library_segment;
-  md_nametab : module_contents;
-  md_deps : (string * Digest.t * bool) list }
+  md_deps : (compilation_unit_name * Digest.t * bool) list }
 
 (*s Modules loaded in memory contain the following informations. They are
     kept in the global table [modules_table]. *)
 
 type module_t = {
-  module_name : string;
-  module_filename : load_path_entry * string;
+  module_name : compilation_unit_name;
+  module_filename : System.physical_path;
   module_compiled_env : compiled_env;
   module_declarations : library_segment;
-  module_nametab : module_contents;
   mutable module_opened : bool;
   mutable module_exported : bool;
-  module_deps : (string * Digest.t * bool) list;
+  module_deps : (compilation_unit_name * Digest.t * bool) list;
   module_digest : Digest.t }
 
-let modules_table = ref Stringmap.empty
+module CompUnitOrdered = 
+  struct
+    type t = dir_path
+    let compare = Pervasives.compare
+  end
+
+module CompUnitmap = Map.Make(CompUnitOrdered)
+
+let modules_table = ref CompUnitmap.empty
 
 let _ = 
   Summary.declare_summary "MODULES"
     { Summary.freeze_function = (fun () -> !modules_table);
       Summary.unfreeze_function = (fun ft -> modules_table := ft);
-      Summary.init_function = (fun () -> modules_table := Stringmap.empty);
-      Summary.survive_section = true }
+      Summary.init_function = (fun () -> modules_table := CompUnitmap.empty);
+      Summary.survive_section = false }
 
 let find_module s =
   try
-    Stringmap.find s !modules_table
+    CompUnitmap.find s !modules_table
   with Not_found ->
-    error ("Unknown module " ^ s)
+    error ("Unknown module " ^ (string_of_dirpath s))
 
-let module_is_loaded s =
-  try let _ = Stringmap.find s !modules_table in true with Not_found -> false
+let module_is_loaded dir =
+  try let _ = CompUnitmap.find dir !modules_table in true
+  with Not_found -> false
 
-let module_is_opened s = (find_module s).module_opened
+let module_is_opened s = (find_module [id_of_string s]).module_opened
 
 let loaded_modules () =
-  Stringmap.fold (fun s _ l -> s :: l) !modules_table []
+  CompUnitmap.fold (fun s _ l -> s :: l) !modules_table []
 
 let opened_modules () =
-  Stringmap.fold 
+  CompUnitmap.fold 
     (fun s m l -> if m.module_opened then s :: l else l) 
     !modules_table []
 
+let compunit_cache = ref Stringmap.empty
+
 let module_segment = function
   | None -> contents_after None
   | Some m -> (find_module m).module_declarations
 
-let module_filename m = (find_module m).module_filename
+let module_full_filename m = (find_module m).module_filename
 
 let vo_magic_number = 0700
 
@@ -106,7 +146,9 @@ let segment_iter f =
   let rec apply = function
     | sp,Leaf obj -> f (sp,obj)
     | _,OpenedSection _ -> assert false
-    | _,ClosedSection (export,s,seg) -> if export then iter seg
+    | sp,ClosedSection (export,s,seg) ->
+	push_section (wd_of_sp sp);
+	if export then iter seg
     | _,(FrozenState _ | Module _) -> ()
   and iter seg =
     List.iter apply seg
@@ -125,7 +167,6 @@ 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;
-    open_module_contents (make_qualid [] (id_of_string s)); 
     m.module_opened <- true
   end
 
@@ -138,60 +179,198 @@ let import_module = open_module true
    then same value as for caller is reused in recursive loadings). *)
 
 let load_objects decls =
-  segment_rec_iter load_object decls
+(*  segment_rec_iter load_object decls*)
+  segment_iter load_object decls
+
+exception LibUnmappedDir
+exception LibNotFound
+type library_location = LibLoaded | LibInPath
 
-let rec load_module_from s f =
+let locate_absolute_library dir =
+  (* Look if loaded *)
   try
-    Stringmap.find s !modules_table
+    let m = CompUnitmap.find dir !modules_table in
+    (LibLoaded, dir, m.module_filename)
   with Not_found ->
-    let (lpe,fname,ch) =
-      try raw_intern_module (get_load_path ()) f
-      with System.Bad_magic_number fname ->
-        errorlabstrm "load_module_from"
-          [< 'sTR"file "; 'sTR fname; 'sPC; 'sTR"has bad magic number.";
-             'sPC; 'sTR"It is corrupted"; 'sPC;
-             'sTR"or was compiled with another version of Coq." >] in
-    let md = System.marshal_in ch in
-    let digest = System.marshal_in ch in
-    close_in ch;
-    let m = { module_name = md.md_name;
-	      module_filename = (lpe,fname);
-	      module_compiled_env = md.md_compiled_env;
-	      module_declarations = md.md_declarations;
-	      module_nametab = md.md_nametab;
-	      module_opened = false;
-	      module_exported = false;
-	      module_deps = md.md_deps;
-	      module_digest = digest } in
-    if s <> md.md_name then
-      error ("The file " ^ fname ^ " does not contain module " ^ s);
-    List.iter (load_mandatory_module s) m.module_deps;
-    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
-    push_module sp m.module_nametab;
-    modules_table := Stringmap.add s m !modules_table;
-    m
-
-and load_mandatory_module caller (s,d,_) =
-  let m = load_module_from s s in
+  (* Look if in loadpath *)
+  try
+    let pref, base = split_dirpath dir in
+    let loadpath = load_path_of_logical_path pref in
+    if loadpath = [] then raise LibUnmappedDir;
+    let name = (string_of_id base)^".vo" in
+    let _, file = System.where_in_path loadpath name in
+    (LibInPath, dir, file)
+  with Not_found ->  raise LibNotFound
+
+let with_magic_number_check f a =
+  try f a
+  with System.Bad_magic_number fname ->
+    errorlabstrm "load_module_from"
+    [< 'sTR"file "; 'sTR fname; 'sPC; 'sTR"has bad magic number.";
+    'sPC; 'sTR"It is corrupted"; 'sPC;
+    'sTR"or was compiled with another version of Coq." >]
+
+let rec load_module = function
+  | (LibLoaded, dir, _) ->
+      CompUnitmap.find dir !modules_table
+  | (LibInPath, dir, f) ->
+    (* [dir] is an absolute name which matches [f] *)
+    let md, digest =
+      try Stringmap.find f !compunit_cache
+      with Not_found ->
+      let ch = with_magic_number_check raw_intern_module f in
+      let md = System.marshal_in ch in
+      let digest = System.marshal_in ch in
+      close_in ch;
+      if dir <> md.md_name then
+	errorlabstrm "load_module"
+	  [< 'sTR ("The file " ^ f ^ " contains module"); 'sPC;
+	  pr_dirpath md.md_name; 'sPC; 'sTR "and not module"; 'sPC;
+	  pr_dirpath dir >];
+      (match split_dirpath dir with
+	| [], id -> Nametab.push_library_root id
+	| _ -> ());
+      compunit_cache := Stringmap.add f (md, digest) !compunit_cache;
+      (md, digest) in
+    intern_module digest f md
+
+and intern_module digest fname md =
+  let m = { module_name = md.md_name;
+            module_filename = fname;
+	    module_compiled_env = md.md_compiled_env;
+	    module_declarations = md.md_declarations;
+	    module_opened = false;
+	    module_exported = false;
+	    module_deps = md.md_deps;
+	    module_digest = digest } in
+  List.iter (load_mandatory_module md.md_name) m.module_deps;
+  Global.import m.module_compiled_env;
+  load_objects m.module_declarations;
+  modules_table := CompUnitmap.add md.md_name m !modules_table;
+  Nametab.push_loaded_library md.md_name;
+  m
+
+and load_mandatory_module caller (dir,d,_) =
+  let m = load_absolute_module_from dir in
   if d <> m.module_digest then
-    error ("module "^caller^" makes inconsistent assumptions over module "^s)
-
-let load_module s = function
-  | None -> ignore (load_module_from s s)
-  | Some f -> ignore (load_module_from s f)
+    error ("compiled module "^(string_of_dirpath caller)^
+	   " makes inconsistent assumptions over module "
+	   ^(string_of_dirpath dir))
 
+and load_absolute_module_from dir =
+  try
+    load_module (locate_absolute_library dir)
+  with
+  | LibUnmappedDir ->
+      let prefix, dir = fst (split_dirpath dir), string_of_dirpath dir in
+      errorlabstrm "load_module"
+      [< 'sTR ("Cannot load "^dir^":"); 'sPC; 
+      'sTR "no physical path bound to"; 'sPC; pr_dirpath prefix; 'fNL >]
+  | LibNotFound ->
+      errorlabstrm "load_module"
+      [< 'sTR"Cannot find module "; pr_dirpath dir; 'sTR" in loadpath">]
+  | _ -> assert false
+
+let try_locate_qualified_library qid =
+  (* Look if loaded *)
+  try 
+    let dir = Nametab.locate_loaded_library qid in
+    (LibLoaded, dir, module_full_filename dir)
+  with Not_found ->
+  (* Look if in loadpath *)
+  try
+    let dir, base = repr_qualid qid in 
+    let loadpath =
+      if dir = [] then get_load_path ()
+      else if is_absolute_dirpath dir then
+	load_path_of_logical_path dir
+      else
+	error
+	  ("Not loaded partially qualified library names not implemented: "
+	  ^(string_of_qualid qid))
+    in
+    if loadpath = [] then raise LibUnmappedDir;
+    let name =  (string_of_id base)^".vo" in
+    let path, file = System.where_in_path loadpath name in
+    (LibInPath, find_logical_path path@[base], file)
+  with Not_found -> raise LibNotFound
+
+let locate_qualified_library qid =
+  try
+    try_locate_qualified_library qid
+  with
+  | LibUnmappedDir ->
+      let prefix, id = repr_qualid qid in
+      errorlabstrm "load_module"
+      [< 'sTR ("Cannot load "^(string_of_id id)^":"); 'sPC; 
+      'sTR "no physical path bound to"; 'sPC; pr_dirpath prefix; 'fNL >]
+  | LibNotFound ->
+      errorlabstrm "load_module"
+      [< 'sTR"Cannot find module "; pr_qualid qid; 'sTR" in loadpath">]
+  | _ -> assert false
+
+let check_module_short_name f dir = function
+  | Some id when id <> snd (split_dirpath dir) ->
+      errorlabstrm "load_module"
+      [< 'sTR ("The file " ^ f ^ " contains module"); 'sPC;
+      pr_dirpath dir; 'sPC; 'sTR "and not module"; 'sPC;
+      pr_id id >]
+  | _ -> ()
+
+let locate_by_filename_only id f =
+  let ch = with_magic_number_check raw_intern_module f in
+  let md = System.marshal_in ch in
+  let digest = System.marshal_in ch in
+  close_in ch;
+  (* Only the base name is expected to match *)
+  check_module_short_name f md.md_name id;
+  (* We check no other file containing same module is loaded *)
+  try
+    let m = CompUnitmap.find md.md_name !modules_table in
+    warning ((string_of_dirpath md.md_name)^" is already loaded from file "^
+    m.module_filename);
+    (LibLoaded, md.md_name, m.module_filename)
+  with Not_found ->
+    (match split_dirpath md.md_name with
+      | [], id -> Nametab.push_library_root id
+      | _ -> ());
+    compunit_cache := Stringmap.add f (md, digest) !compunit_cache;
+    (LibInPath, md.md_name, f)
+
+let locate_module qid = function
+  | Some f ->
+      (* A name is specified, we have to check it contains module id *)
+      let prefix, id = repr_qualid qid in
+      assert (prefix = []);
+      let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in
+      locate_by_filename_only (Some id) f
+  | None ->
+      (* No name, we need to find the file name *)
+      locate_qualified_library qid
+
+let read_module qid =
+  ignore (load_module (locate_qualified_library qid))
+
+let read_module_from_file f =
+  let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in
+  ignore (load_module (locate_by_filename_only None f))
+
+let reload_module (modref, export) =
+  let m = load_module modref in
+  if export then m.module_exported <- true;
+  open_module false m.module_name
 
 (*s [require_module] loads and opens a module. This is a synchronized
     operation. *)
 
-let cache_require (_,(name,file,export)) =
-  let m = load_module_from name file in
+type module_reference = (library_location * CompUnitmap.key * Util.Stringmap.key) * bool
+
+let cache_require (_,(modref,export)) =
+  let m = load_module modref in
   if export then m.module_exported <- true;
-  open_module false name
+  open_module false m.module_name
 
-let (in_require, _) =
+let (in_require, out_require) =
   declare_object
     ("REQUIRE",
      { cache_function = cache_require;
@@ -199,32 +378,28 @@ let (in_require, _) =
        open_function = (fun _ -> ());
        export_function = (fun _ -> None) })
   
-let require_module spec name fileopt export =
+let require_module spec qid fileopt export =
 (* Trop contraignant
   if sections_are_opened () then
     warning ("Objets of "^name^" not surviving sections (e.g. Grammar \nand Hints) will be removed at the end of the section");
 *)
-  let file = match fileopt with
-    | None -> name
-    | Some f -> f 
-  in
-  add_anonymous_leaf (in_require (name,file,export));
+  let modref = locate_module qid fileopt in
+  add_anonymous_leaf (in_require (modref,export));
   add_frozen_state ()
 
 (*s [save_module s] saves the module [m] to the disk. *)
 
 let current_imports () =
-  Stringmap.fold
+  CompUnitmap.fold
     (fun _ m l -> (m.module_name, m.module_digest, m.module_exported) :: l)
     !modules_table []
 
-let save_module_to process s f =
-  let seg = export_module () in
+let save_module_to s f =
+  let seg = export_module s in
   let md = { 
     md_name = s;
     md_compiled_env = Global.export s;
     md_declarations = seg;
-    md_nametab = process seg;
     md_deps = current_imports () } in
   let (f',ch) = raw_extern_module f in
   try
@@ -234,6 +409,7 @@ let save_module_to process s f =
     System.marshal_out ch di;
     close_out ch
   with e -> (warning ("Removed file "^f');close_out ch; Sys.remove f'; raise e)
+
 (*s Iterators. *)
 
 let fold_all_segments insec f x =
@@ -244,7 +420,7 @@ let fold_all_segments insec f x =
     | _ -> acc
   in
   let acc' = 
-    Stringmap.fold 
+    CompUnitmap.fold 
       (fun _ m acc -> List.fold_left apply acc m.module_declarations) 
       !modules_table x
   in
@@ -256,7 +432,7 @@ let iter_all_segments insec f =
     | _, ClosedSection (_,_,seg) -> if insec then List.iter apply seg
     | _ -> ()
   in
-  Stringmap.iter 
+  CompUnitmap.iter 
     (fun _ m -> List.iter apply m.module_declarations) !modules_table;
   List.iter apply (Lib.contents_after None)
 
@@ -266,9 +442,9 @@ let fmt_modules_state () =
   let opened = opened_modules ()
   and loaded = loaded_modules () in
   [< 'sTR "Imported (open) Modules: " ;
-     prlist_with_sep pr_spc (fun s -> [< 'sTR s >]) opened ; 'fNL ;
-     'sTR "Loaded Modules: " ;
-     prlist_with_sep pr_spc (fun s -> [< 'sTR s >]) loaded ; 'fNL >]
+     prlist_with_sep pr_spc pr_dirpath opened ; 'fNL ;
+     'sTR "Loaded Modules: ";
+     prlist_with_sep pr_spc pr_dirpath loaded ; 'fNL >]
 
 (*s Display the memory use of a module. *)
 
@@ -276,6 +452,6 @@ open Printf
 
 let mem s =
   let m = find_module s in
-  h 0 [< 'sTR (sprintf "%dk (cenv = %dk / seg = %dk / nmt = %dk)"
+  h 0 [< 'sTR (sprintf "%dk (cenv = %dk / seg = %dk)"
 		 (size_kb m) (size_kb m.module_compiled_env) 
-		 (size_kb m.module_declarations) (size_kb m.module_nametab)) >]
+		 (size_kb m.module_declarations)) >]
diff --git a/library/library.mli b/library/library.mli
index e5ad55e48..3274f7361 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -20,14 +20,15 @@ open Libobject
    provides a high level function [require] which corresponds to the 
    vernacular command [Require]. *)
 
-val load_module : string -> string option -> unit
-val import_module : string -> unit
+val read_module : Nametab.qualid -> unit
+val read_module_from_file : System.physical_path -> unit
+val import_module : dir_path -> unit
 
-val module_is_loaded : string -> bool
+val module_is_loaded : dir_path -> bool
 val module_is_opened : string -> bool
 
-val loaded_modules : unit -> string list
-val opened_modules : unit -> string list
+val loaded_modules : unit -> dir_path list
+val opened_modules : unit -> dir_path list
 
 val fmt_modules_state : unit -> Pp.std_ppcmds
 
@@ -37,21 +38,21 @@ val fmt_modules_state : unit -> Pp.std_ppcmds
   ([false]), if not [None]. And [export] specifies if the module must be 
   exported. *)
 
-val require_module : bool option -> string -> string option -> bool -> unit
+val require_module :
+  bool option -> Nametab.qualid -> string option -> bool -> unit
 
 (*s [save_module_to s f] saves the current environment as a module [s]
   in the file [f]. *)
 
-val save_module_to : (Lib.library_segment -> Nametab.module_contents) -> 
-  string -> string -> unit
+val save_module_to : dir_path -> string -> unit
 
 (*s [module_segment m] returns the segment of the loaded module
     [m]; if not given, the segment of the current module is returned
     (which is then the same as [Lib.contents_after None]). 
-    [module_filename] returns the full filename of a loaded module. *)
+    [module_full_filename] returns the full filename of a loaded module. *)
 
-val module_segment : string option -> Lib.library_segment
-val module_filename : string -> System.load_path_entry * string
+val module_segment : dir_path option -> Lib.library_segment
+val module_full_filename : dir_path -> string
 
 (*s [fold_all_segments] and [iter_all_segments] iterate over all
     segments, the modules' segments first and then the current
@@ -63,10 +64,28 @@ val fold_all_segments : bool -> ('a -> section_path -> obj -> 'a) -> 'a -> 'a
 val iter_all_segments : bool -> (section_path -> obj -> unit) -> unit
 
 (*s Global load path *)
-val get_load_path : unit -> System.load_path
-val add_load_path_entry : System.load_path_entry -> unit
-val remove_path : string -> unit
+type logical_path = dir_path
+
+val get_load_path : unit -> System.physical_path list
+val get_full_load_path : unit -> (System.physical_path * logical_path) list
+val add_load_path_entry : System.physical_path * logical_path -> unit
+val remove_path : System.physical_path -> unit
+val find_logical_path : System.physical_path -> logical_path
+val load_path_of_logical_path : dir_path -> System.physical_path list
+
+exception LibUnmappedDir
+exception LibNotFound
+type library_location = LibLoaded | LibInPath
+
+val locate_qualified_library :
+  Nametab.qualid -> library_location * dir_path * System.physical_path
 
 (*s Displays the memory use of a module. *)
 
-val mem : string -> Pp.std_ppcmds
+val mem : dir_path -> Pp.std_ppcmds
+
+(* For discharge *)
+type module_reference
+
+val out_require : Libobject.obj -> module_reference
+val reload_module : module_reference -> unit
diff --git a/library/nametab.ml b/library/nametab.ml
index aec5da6f9..3d7ca98f4 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -16,16 +16,20 @@ open Declarations
 open Term
 
 (*s qualified names *)
-type qualid = string list * identifier
+type qualid = dir_path * identifier
 
 let make_qualid p id = (p,id)
 let repr_qualid q = q
 
-let string_of_qualid (l,id) = String.concat "." (l@[string_of_id id])
-let pr_qualid (l,id) =
-  prlist_with_sep (fun () -> pr_str ".") pr_str (l@[string_of_id id])
+let string_of_qualid (l,id) =
+  let dir = if l = [] then "" else string_of_dirpath l ^ "." in
+  dir ^ string_of_id id
+let pr_qualid p = pr_str (string_of_qualid p)
 
 let qualid_of_sp sp = make_qualid (dirpath sp) (basename sp)
+let qualid_of_dirpath dir = 
+  let a,l = list_sep_last (repr_qualid dir) in
+  make_qualid l a
 
 exception GlobalizationError of qualid
 
@@ -39,141 +43,161 @@ let error_global_not_found q = raise (GlobalizationError q)
 let roots = ref []
 let push_library_root s = roots := list_add_set s !roots
 
-let coq_root = "Coq"
-let default_root = "Scratch"
-
-(* Names tables *)
-type cci_table = global_reference Idmap.t
-type obj_table = (section_path * obj) Idmap.t
-type mod_table = (section_path * module_contents) Stringmap.t
-and module_contents = Closed of cci_table * obj_table * mod_table
-
-let empty =
-  Closed (Idmap.empty, Idmap.empty, Stringmap.empty)
- 
-let persistent_nametab = ref (empty : module_contents)
-let local_nametab = ref (empty : module_contents)
-
-let push_cci (Closed (ccitab, objtab, modtab)) s ref =
-  Closed (Idmap.add s ref ccitab, objtab, modtab)
-
-let push_obj (Closed (ccitab, objtab, modtab)) s obj =
-  Closed (ccitab, Idmap.add s obj objtab, modtab)
-
-let push_mod (Closed (ccitab, objtab, modtab)) s mc =
-  (* devrait pas mais ca plante en décommentant la ligne ci-dessous *)
- (* assert (not (Stringmap.mem s modtab)); *)
-  Closed (ccitab, objtab, Stringmap.add s mc modtab)
-
-let push_tree push dir id o =
-  let rec search (Closed (ccitab, objtab, modtab) as tabs) pref = function
-    | id :: dir' ->
-	let sp, mc = 
-	  try Stringmap.find id modtab
-	  with Not_found ->
-	    let pref = List.rev pref in
-	    (make_path dir (id_of_string id) CCI, empty)
+let coq_root = id_of_string "Coq"
+let default_root_prefix = []
+
+(* Constructions and syntactic definitions live in the same space *)
+type extended_global_reference =
+  | TrueGlobal of global_reference
+  | SyntacticDef of section_path
+
+type 'a nametree = ('a option * 'a nametree ModIdmap.t)
+type ccitab = extended_global_reference nametree Idmap.t
+type objtab = section_path nametree Idmap.t
+type dirtab = dir_path nametree ModIdmap.t
+
+let the_ccitab = ref (Idmap.empty : ccitab)
+let the_libtab = ref (ModIdmap.empty : dirtab)
+let the_sectab = ref (ModIdmap.empty : dirtab)
+let the_objtab = ref (Idmap.empty : objtab)
+
+(* How necessarily_open works: concretely, roots and directory are
+   always open but libraries are open only during their interactive
+   construction or on demand if a precompiled one; then for a name
+   "Root.Rep.Lib.name", then "Lib.name", "Rep.Lib.name" and
+   "Root.Rep.Lib.name", but not "name" are pushed *)
+
+(* We add a binding of [[modid1;...;modidn;id]] to [o] in the name tab *)
+(* We proceed in the reverse way, looking first to [id] *)
+let push_tree tab dir o =
+  let rec push necessarily_open (current,dirmap) = function
+    | modid :: path as dir ->
+	let mc = 
+	  try ModIdmap.find modid dirmap
+	  with Not_found -> (None, ModIdmap.empty)
 	in
-	Closed (ccitab, objtab,
-		Stringmap.add id (sp,search mc (id::pref) dir') modtab)
-    | [] ->
-	push tabs id o in
-  persistent_nametab := search !persistent_nametab [] dir
-
-(* This pushes a name at the current level (for relative qualified use) *)
-let push_cci_current = push_tree push_cci []
-let push_obj_current = push_tree push_obj []
-let push_mod_current = push_tree push_mod []
-
-(* This pushes a name at the root level (for absolute access) *)
-let push_cci_absolute = push_tree push_cci
-let push_obj_absolute = push_tree push_obj
-let push_mod_absolute = push_tree push_mod
+	let this = if necessarily_open then Some o else current in
+	(this, ModIdmap.add modid (push true mc path) dirmap)
+    | [] -> (Some o,dirmap) in
+  push false tab (List.rev dir)
+
+let push_idtree tab dir id o =
+  let modtab =
+    try Idmap.find id !tab
+    with Not_found -> (None, ModIdmap.empty) in
+  tab := Idmap.add id (push_tree modtab dir o) !tab
+
+let push_long_names_ccipath = push_idtree the_ccitab
+let push_short_name_ccipath = push_idtree the_ccitab
+let push_short_name_objpath = push_idtree the_objtab
+
+let push_modidtree tab dir id o =
+  let modtab =
+    try ModIdmap.find id !tab
+    with Not_found -> (None, ModIdmap.empty) in
+  tab := ModIdmap.add id (push_tree modtab dir o) !tab
+
+let push_long_names_secpath = push_modidtree the_sectab
+let push_long_names_libpath = push_modidtree the_libtab
 
 (* These are entry points for new declarations at toplevel *)
-(* Do not use with "open" since it pushes an absolute name too *)
-let push sp ref =
-  let dir, s = repr_qualid (qualid_of_sp sp) in
-  push_cci_absolute dir s ref;
-  push_cci_current s ref
 
-let push_object sp obj =
-  let dir, s = repr_qualid (qualid_of_sp sp) in
-  push_obj_absolute dir s (sp,obj);
-  push_obj_current s (sp,obj)
+(* This is for permanent constructions (never discharged -- but with
+   possibly limited visibility, i.e. Theorem, Lemma, Definition, Axiom,
+   Parameter but also Remark and Fact) *)
 
-let push_module sp mc =
-  let dir, s = repr_qualid (qualid_of_sp sp) in
-  let s = string_of_id s in
-  push_mod_absolute dir s (sp,mc);
-  if List.mem s !roots then 
-    warning ("Cannot allow access to "^s^" by relative paths: it is already registered as a root of the Coq library")
-  else push_mod_current s (sp,mc)
-
-(* Sections are not accessible by basename *)
-let push_section sp mc =
+let push_cci sp ref =
   let dir, s = repr_qualid (qualid_of_sp sp) in
-  push_mod_absolute dir (string_of_id s) (sp,mc)
+  (* We push partially qualified name (with at least one prefix) *)
+  push_long_names_ccipath dir s (TrueGlobal ref)
 
-(* This is an entry point for local declarations at toplevel *)
-(* Do not use with "open" since it pushes an absolute name too *)
+let push = push_cci
 
-let push_cci_local s ref =
-  local_nametab := push_cci !local_nametab s ref
+let push_short_name id ref =
+  (* We push a volatile unqualified name *)
+  push_short_name_ccipath [] id (TrueGlobal ref)
 
-let push_obj_local s o =
-  local_nametab := push_obj !local_nametab s o
+(* This is for Syntactic Definitions *)
 
-let push_local sp ref =
+let push_syntactic_definition sp =
   let dir, s = repr_qualid (qualid_of_sp sp) in
-  push_cci_absolute dir s ref;
-  push_cci_local s ref
+  push_long_names_ccipath dir s (SyntacticDef sp)
 
-let push_local_object sp obj =
-  let dir, s = repr_qualid (qualid_of_sp sp) in
-  push_obj_absolute dir s (sp,obj);
-  push_obj_local s (sp,obj)
+let push_short_name_syntactic_definition sp =
+  let _, s = repr_qualid (qualid_of_sp sp) in
+  push_short_name_ccipath [] s (SyntacticDef sp)
+
+(* This is for dischargeable non-cci objects (removed at the end of the
+   section -- i.e. Hints, Grammar ...) *) (* --> Unused *)
+
+let push_short_name_object sp =
+  push_short_name_objpath [] (basename sp) sp
+
+(* This is to remember absolute Section/Module names and to avoid redundancy *)
+
+let push_section fulldir =
+  let dir, s = split_dirpath fulldir in
+  (* We push all partially qualified name *)
+  push_long_names_secpath dir s fulldir;
+  push_long_names_secpath [] s fulldir
 
 (* These are entry points to locate names *)
 (* If the name starts with the coq_root name, then it is an absolute name *)
-let locate qid =
-  let (dir,id) = repr_qualid qid in
-  let rec search (Closed (ccitab,_,modtab)) = function
-    | id :: dir' -> search (snd (Stringmap.find id modtab)) dir'
-    | [] -> Idmap.find id ccitab
+let locate_in_tree tab dir =
+  let dir = List.rev dir in
+  let rec search (current,modidtab) = function
+    | modid :: path -> search (ModIdmap.find modid modidtab) path
+    | [] -> match current with Some o -> o | _ -> raise Not_found
   in
-  try search !local_nametab dir
-  with Not_found -> search !persistent_nametab dir
+  search tab dir
+
+let locate_cci qid =
+  let (dir,id) = repr_qualid qid in
+  locate_in_tree (Idmap.find id !the_ccitab) dir
+
+(* This should be used when syntactic definitions are allowed *)
+let extended_locate = locate_cci
+
+(* This should be used when no syntactic definitions is expected *)
+let locate qid = match locate_cci qid with
+  | TrueGlobal ref -> ref
+  | SyntacticDef _ -> raise Not_found
 
 let locate_obj qid =
   let (dir,id) = repr_qualid qid in
-  let rec search (Closed (_,objtab,modtab)) = function
-    | id :: dir' -> search (snd (Stringmap.find id modtab)) dir'
-    | [] -> Idmap.find id objtab
-  in
-  try search !local_nametab dir
-  with Not_found -> search !persistent_nametab dir
+  locate_in_tree (Idmap.find id !the_objtab) dir
+
+(* Actually, this table has only two levels, since only basename and *)
+(* fullname are registered *)
+let push_loaded_library fulldir =
+  let dir, s = split_dirpath fulldir in
+  push_long_names_libpath dir s fulldir;
+  push_long_names_libpath [] s fulldir
 
-let locate_module qid =
+let locate_loaded_library qid =
   let (dir,id) = repr_qualid qid in
-  let s = string_of_id id in
-  let rec search (Closed (_,_,modtab)) = function
-    | id :: dir' -> search (snd (Stringmap.find id modtab)) dir'
-    | [] -> Stringmap.find s modtab
-  in
-  try search !local_nametab dir
-  with Not_found -> search !persistent_nametab dir
+  locate_in_tree (ModIdmap.find id !the_libtab) dir
+
+let locate_section qid =
+  let (dir,id) = repr_qualid qid in
+  locate_in_tree (ModIdmap.find id !the_sectab) dir
+
+(* Derived functions *)
 
 let locate_constant qid =
-  match locate qid with
-    | ConstRef sp -> sp
+  match locate_cci qid with
+    | TrueGlobal (ConstRef sp) -> sp
     | _ -> raise Not_found
 
-let sp_of_id _ id = locate (make_qualid [] id)
+let sp_of_id _ id = match locate_cci (make_qualid [] id) with
+  | TrueGlobal ref -> ref
+  | SyntacticDef _ ->
+      anomaly ("sp_of_id: "^(string_of_id id)
+	       ^" is not a true global reference but a syntactic definition")
 
 let constant_sp_of_id id =
-  match locate (make_qualid [] id) with
-    | ConstRef sp -> sp
+  match locate_cci (make_qualid [] id) with
+    | TrueGlobal (ConstRef sp) -> sp
     | _ -> raise Not_found
 
 let check_absoluteness dir =
@@ -181,29 +205,19 @@ let check_absoluteness dir =
     | a::_ when List.mem a !roots -> ()
     | _ -> anomaly ("Not an absolute dirpath: "^(string_of_dirpath dir))
 
+let is_absolute_dirpath = function
+    | a::_ when List.mem a !roots -> true
+    | _ -> false
+
 let absolute_reference sp =
   check_absoluteness (dirpath sp);
   locate (qualid_of_sp sp)
 
-exception Found of global_reference
-let locate_in_module dir id =
-  let rec exists_in id (Closed (ccitab,_,modtab)) =
-    try raise (Found (Idmap.find id ccitab))
-    with Not_found -> 
-      Stringmap.iter (fun _ (sp,mc) -> exists_in id mc) modtab
-  in
-  let rec search (Closed (ccitab,_,modtab) as mc) = function
-    | modid :: dir' -> search (snd (Stringmap.find modid modtab)) dir'
-    | [] -> 
-	try exists_in id mc; raise Not_found
-	with Found ref -> ref
-  in
-  search !persistent_nametab dir
-
 let locate_in_absolute_module dir id =
   check_absoluteness dir;
-  locate_in_module dir id
+  locate (make_qualid dir id)
 
+(*
 (* These are entry points to make the contents of a module/section visible *)
 (* in the current env (does not affect the absolute name space `coq_root') *)
 let open_module_contents qid =
@@ -229,40 +243,46 @@ let rec rec_open_module_contents qid =
        push_mod_current m mt;
        rec_open_module_contents (qualid_of_sp sp))
     modtab
-
+*)
 let exists_cci sp =
-  try let _ = locate (qualid_of_sp sp) in true with Not_found -> false
+  try let _ = locate_cci (qualid_of_sp sp) in true
+  with Not_found -> false
 
-let exists_module sp =
-  try let _ = locate_module (qualid_of_sp sp) in true with Not_found -> false
+let exists_section dir =
+  try let _ = locate_section (qualid_of_dirpath dir) in true
+  with Not_found -> false
 
 (********************************************************************)
-(* Registration of persistent tables as a global table and rollback *)
-
-type frozen = module_contents
-
-let init () = persistent_nametab := empty; roots := []
-let freeze () = !persistent_nametab, !roots
-let unfreeze (mc,r) = persistent_nametab := mc; roots := r
-
-let _ = 
-  Summary.declare_summary "persistent-names"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init;
-      Summary.survive_section = true }
 
 (********************************************************************)
-(* Registration of persistent tables as a global table and rollback *)
-
-let init () = local_nametab := empty
-let freeze () = !local_nametab
-let unfreeze mc = local_nametab := mc
+(* Registration of tables as a global table and rollback            *)
+
+type frozen = ccitab * dirtab * dirtab * objtab * identifier list
+
+let init () = 
+  the_ccitab := Idmap.empty; 
+  the_libtab := ModIdmap.empty;
+  the_sectab := ModIdmap.empty;
+  the_objtab := Idmap.empty;
+  roots := []
+
+let freeze () =
+  !the_ccitab, 
+  !the_libtab,
+  !the_sectab,
+  !the_objtab,
+  !roots
+
+let unfreeze (mc,ml,ms,mo,r) =
+  the_ccitab := mc;
+  the_libtab := ml;
+  the_sectab := ms;
+  the_objtab := mo;
+  roots := r
 
 let _ = 
-  Summary.declare_summary "local-names"
+  Summary.declare_summary "names"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
       Summary.init_function = init;
       Summary.survive_section = false }
-
diff --git a/library/nametab.mli b/library/nametab.mli
index 8506c7a5b..927205dea 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -18,6 +18,10 @@ open Term
 (*s This module contains the table for globalization, which associates global
    names (section paths) to qualified names. *)
 
+type extended_global_reference =
+  | TrueGlobal of global_reference
+  | SyntacticDef of section_path
+
 (*s A [qualid] is a partially qualified ident; it includes fully
     qualified names (= absolute names) and all intermediate partial
     qualifications of absolute names, including single identifiers *)
@@ -38,19 +42,17 @@ exception GlobalizationError of qualid
 val error_global_not_found_loc : loc -> qualid -> 'a
 val error_global_not_found     : qualid -> 'a
 
-(*s Names tables *)
-type cci_table = global_reference Idmap.t
-type obj_table = (section_path * Libobject.obj) Idmap.t
-type mod_table = (section_path * module_contents) Stringmap.t
-and module_contents = Closed of cci_table * obj_table * mod_table
-
-(*s Registers absolute paths *)
+(*s Register visibility of absolute paths by qualified names *)
 val push : section_path -> global_reference -> unit
-val push_object : section_path -> Libobject.obj -> unit
-val push_module : section_path -> module_contents -> unit
+val push_syntactic_definition : section_path -> unit
+
+(*s Register visibility of absolute paths by short names *)
+val push_short_name : identifier -> global_reference -> unit
+val push_short_name_syntactic_definition : section_path -> unit
+val push_short_name_object : section_path -> unit
 
-val push_local : section_path -> global_reference -> unit
-val push_local_object : section_path -> Libobject.obj -> unit
+(*s Register visibility by all qualifications *)
+val push_section : dir_path -> unit
 
 (* This should eventually disappear *)
 val sp_of_id : path_kind -> identifier -> global_reference
@@ -61,37 +63,47 @@ val sp_of_id : path_kind -> identifier -> global_reference
 val constant_sp_of_id : identifier -> section_path
 
 val locate : qualid -> global_reference
-val locate_obj : qualid -> (section_path * Libobject.obj)
+
+(* This locates also syntactic definitions *)
+val extended_locate : qualid -> extended_global_reference
+
+val locate_obj : qualid -> section_path
+
 val locate_constant : qualid -> constant_path
-val locate_module : qualid -> section_path * module_contents
+val locate_section : qualid -> dir_path
 
 (* [exists sp] tells if [sp] is already bound to a cci term *)
 val exists_cci : section_path -> bool
-val exists_module : section_path -> bool
-
+val exists_section : dir_path -> bool
+(*
 val open_module_contents : qualid -> unit
 val rec_open_module_contents : qualid -> unit
 
 (*s Entry points for sections *)
 val open_section_contents : qualid -> unit
 val push_section : section_path -> module_contents -> unit
-
+*)
 (*s Roots of the space of absolute names *)
 
 (* This is the root of the standard library of Coq *)
-val coq_root : string
+val coq_root : module_ident
 
-(* This is the default root for developments which doesn't mention a root *)
-val default_root : string
+(* This is the default root prefix for developments which doesn't mention a root *)
+val default_root_prefix : dir_path
 
 (* This is to declare a new root *)
-val push_library_root : string -> unit
+val push_library_root : module_ident -> unit
 
 (* This turns a "user" absolute name into a global reference;
    especially, constructor/inductive names are turned into internal
    references inside a block of mutual inductive *)
 val absolute_reference : section_path -> global_reference
 
+val is_absolute_dirpath : dir_path -> bool
+
 (* [locate_in_absolute_module dir id] finds [id] in module [dir] or in
    one of its section/subsection *)
 val locate_in_absolute_module : dir_path -> identifier -> global_reference
+
+val push_loaded_library : dir_path -> unit
+val locate_loaded_library : qualid -> dir_path