- Cleaning phase of the interfaces of libnames.ml and nametab.ml

  (uniformisation of function names, classification). One of the most
  visible change is the renaming of section_path into full_path (the
  use of name section was obsolete due to the module system, but I
  don't know if the new name is the best chosen one - especially it 
  remains some "sp" here and there).
- Simplification of the interface of classify_object (first argument dropped).
- Simplification of the code for vernac keyword "End".
- Other small cleaning or dead code removal.



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

18 files changed, 284 insertions, 323 deletions

diff --git a/library/declare.ml b/library/declare.ml
index a973e6a55..0cd1250c7 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -141,7 +141,7 @@ let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk
 
 let export_constant cst = Some (dummy_constant cst)
 
-let classify_constant (_,cst) = Substitute (dummy_constant cst)
+let classify_constant cst = Substitute (dummy_constant cst)
 
 let (inConstant,_) =
   declare_object { (default_object "CONSTANT") with
@@ -267,7 +267,7 @@ let (inInductive,_) =
     cache_function = cache_inductive;
     load_function = load_inductive;
     open_function = open_inductive;
-    classify_function = (fun (_,a) -> Substitute (dummy_inductive_entry a));
+    classify_function = (fun a -> Substitute (dummy_inductive_entry a));
     subst_function = ident_subst_function;
     discharge_function = discharge_inductive;
     export_function = export_inductive } 
diff --git a/library/declare.mli b/library/declare.mli
index 32b651122..d5933ffb0 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -65,4 +65,4 @@ val set_xml_declare_constant : (bool * constant -> unit) -> unit
 val set_xml_declare_inductive : (bool * object_name -> unit) -> unit
 
 (* hook for the cache function of constants and inductives *)
-val add_cache_hook : (section_path -> unit) -> unit
+val add_cache_hook : (full_path -> unit) -> unit
diff --git a/library/declaremods.ml b/library/declaremods.ml
index f1a2c9e6c..0aa3d96bb 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -104,7 +104,7 @@ let _ = Summary.declare_summary "MODULE-INFO"
 	    Summary.survive_module = false;
 	    Summary.survive_section = false }
 
-(* auxiliary functions to transform section_path and kernel_name given
+(* auxiliary functions to transform full_path and kernel_name given
    by Lib into module_path and dir_path needed for modules *)
 
 let mp_of_kn kn = 
@@ -116,7 +116,7 @@ let mp_of_kn kn =
 
 let dir_of_sp sp = 
   let dir,id = repr_path sp in
-    extend_dirpath dir id
+    add_dirpath_suffix dir id
 
 let msid_of_mp = function
     MPself msid -> msid
@@ -287,7 +287,7 @@ let subst_module ((sp,kn),subst,(entry,substobjs,_)) =
     (None,substobjs,substituted)
 
 
-let classify_module (_,(_,substobjs,_)) =
+let classify_module (_,substobjs,_) =
   Substitute (None,substobjs,None)
 
 
@@ -449,7 +449,7 @@ and subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) =
 	  end
       | None -> anomaly "Modops: Empty info"
 
-and classify_module_alias (_,(entry,substobjs,_)) =
+and classify_module_alias (entry,substobjs,_) =
   Substitute (entry,substobjs,None)
 	        
 let (in_module_alias,out_module_alias) =
@@ -530,7 +530,7 @@ let cache_modtype ((sp,kn),(entry,modtypeobjs)) =
 
   if Nametab.exists_modtype sp then
     errorlabstrm "cache_modtype"
-      (pr_sp sp ++ str " already exists") ;
+      (pr_path sp ++ str " already exists") ;
 
   Nametab.push_modtype (Nametab.Until 1) sp (mp_of_kn kn);
 
@@ -542,7 +542,7 @@ let load_modtype i ((sp,kn),(entry,modtypeobjs)) =
 
   if Nametab.exists_modtype sp then
     errorlabstrm "cache_modtype"
-      (pr_sp sp ++ str " already exists") ;
+      (pr_path sp ++ str " already exists") ;
 
   Nametab.push_modtype (Nametab.Until i) sp (mp_of_kn kn);
     
@@ -553,11 +553,11 @@ let open_modtype i ((sp,kn),(entry,_)) =
   check_empty "open_modtype" entry;
 
   if 
-    try Nametab.locate_modtype (qualid_of_sp sp) <> (mp_of_kn kn) 
+    try Nametab.locate_modtype (qualid_of_path sp) <> (mp_of_kn kn) 
     with Not_found -> true
   then
     errorlabstrm ("open_modtype") 
-      (pr_sp sp ++ str " should already exist!");
+      (pr_path sp ++ str " should already exist!");
 
   Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn)
 
@@ -566,7 +566,7 @@ let subst_modtype (_,subst,(entry,(subs,mbids,msid,objs))) =
   (entry,(join subs subst,mbids,msid,objs))
 
 
-let classify_modtype (_,(_,substobjs)) =
+let classify_modtype (_,substobjs) =
   Substitute (None,substobjs)
 
 
@@ -726,9 +726,9 @@ let start_module interp_modtype export id args res_o =
   Lib.add_frozen_state (); mp
 
 
-let end_module id =
+let end_module () =
 
-  let oldoname,oldprefix,fs,lib_stack = Lib.end_module id in
+  let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in
   let mbids, res_o, sub_o = !openmod_info in
   let substitute, keep, special = Lib.classify_segment lib_stack in
 
@@ -753,6 +753,7 @@ let end_module id =
     (* must be called after get_modtype_substobjs, because of possible
      dependencies on functor arguments *)
 
+  let id = basename (fst oldoname) in
   let mp = Global.end_module id res_o in
 
   begin match sub_o with
@@ -845,7 +846,7 @@ let cache_import (_,(_,mp)) =
   let mp = Nametab.locate_module (qualid_of_dirpath dir) in  *)
   really_import_module mp
 
-let classify_import (_,(export,_ as obj)) = 
+let classify_import (export,_ as obj) = 
   if export then Substitute obj else Dispose
 
 let subst_import (_,subst,(export,mp as obj)) =
@@ -880,9 +881,10 @@ let start_modtype interp_modtype id args =
   Lib.add_frozen_state (); mp
 
 
-let end_modtype id =
+let end_modtype () =
 
-  let oldoname,prefix,fs,lib_stack = Lib.end_modtype id in
+  let oldoname,prefix,fs,lib_stack = Lib.end_modtype () in
+  let id = basename (fst oldoname) in
   let ln = Global.end_modtype id in
   let substitute, _, special = Lib.classify_segment lib_stack in
 
@@ -1041,7 +1043,7 @@ let subst_include (oname,subst,((me,is_mod),substobj,_)) =
   let substituted = subst_substobjs dir mp1 substobjs in
     ((subst_inc_expr subst' me,is_mod),substobjs,substituted)
 
-let classify_include (_,((me,is_mod),substobjs,_)) =
+let classify_include ((me,is_mod),substobjs,_) =
   Substitute ((me,is_mod),substobjs,None)
 
 let (in_include,out_include) =
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 322078e9b..058bfa6ad 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -46,7 +46,7 @@ val start_module : (env -> 'modtype -> module_struct_entry) ->
   bool option -> identifier -> (identifier located list * 'modtype) list ->
    ('modtype * bool) option -> module_path
 
-val end_module : identifier -> module_path
+val end_module : unit -> module_path
 
 
 
@@ -58,7 +58,7 @@ val declare_modtype : (env -> 'modtype -> module_struct_entry) ->
 val start_modtype : (env -> 'modtype -> module_struct_entry) -> 
   identifier -> (identifier located list * 'modtype) list -> module_path
 
-val end_modtype : identifier -> module_path
+val end_modtype : unit -> module_path
 
 
 (*s Objects of a module. They come in two lists: the substitutive ones
diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
index 4a28c2fa5..7812b1f9e 100644
--- a/library/dischargedhypsmap.ml
+++ b/library/dischargedhypsmap.ml
@@ -20,7 +20,7 @@ open Libobject
 open Lib
 open Nametab
 
-type discharged_hyps = section_path list
+type discharged_hyps = full_path list
 
 let discharged_hyps_map = ref Spmap.empty
 
diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli
index 56e5492d8..f9d0f9b4f 100644
--- a/library/dischargedhypsmap.mli
+++ b/library/dischargedhypsmap.mli
@@ -15,10 +15,10 @@ open Environ
 open Nametab
 (*i*)
 
-type discharged_hyps = section_path list
+type discharged_hyps = full_path list
 
 (*s Discharged hypothesis. Here we store the discharged hypothesis of each *)
 (*  constant or inductive type declaration.                                *)
 
-val set_discharged_hyps : section_path -> discharged_hyps -> unit
-val get_discharged_hyps : section_path -> discharged_hyps
+val set_discharged_hyps : full_path -> discharged_hyps -> unit
+val get_discharged_hyps : full_path -> discharged_hyps
diff --git a/library/goptions.ml b/library/goptions.ml
index 95259c9b5..6e58fd218 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -105,7 +105,7 @@ module MakeTable =
 		Libobject.open_function = load_options;
 		Libobject.cache_function = cache_options;
 		Libobject.subst_function = subst_options;
-		Libobject.classify_function = (fun (_,x) -> Substitute x);
+		Libobject.classify_function = (fun x -> Substitute x);
 		Libobject.export_function = export_options} 
 	in
         ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))),
diff --git a/library/heads.ml b/library/heads.ml
index ea3acbbe8..ba3a45594 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -164,7 +164,7 @@ let (inHead, _) =
     cache_function = cache_head;
     load_function = load_head;
     subst_function = subst_head;
-    classify_function = (fun (_,x) -> Substitute x);
+    classify_function = (fun x -> Substitute x);
     discharge_function = discharge_head;
     rebuild_function = rebuild_head;
     export_function = export_head }
diff --git a/library/impargs.ml b/library/impargs.ml
index 96c5c2a5c..68809d6aa 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -529,7 +529,7 @@ let (inImplicits, _) =
     cache_function = cache_implicits;
     load_function = load_implicits;
     subst_function = subst_implicits;
-    classify_function = (fun (_,x) -> Substitute x);
+    classify_function = (fun x -> Substitute x);
     discharge_function = discharge_implicits;
     rebuild_function = rebuild_implicits;
     export_function = export_implicits }
diff --git a/library/lib.ml b/library/lib.ml
index 9dbf7ddc0..c033a3805 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -58,9 +58,9 @@ let load_and_subst_objects i prefix subst seg =
 let classify_segment seg =
   let rec clean ((substl,keepl,anticipl) as acc) = function
     | (_,CompilingLibrary _) :: _ | [] -> acc
-    | ((sp,kn as oname),Leaf o) :: stk -> 
+    | ((sp,kn),Leaf o) :: stk -> 
 	let id = Names.id_of_label (Names.label kn) in
-	  (match classify_object (oname,o) with 
+	  (match classify_object o with 
 	     | Dispose -> clean acc stk
 	     | Keep o' -> 
 		 clean (substl, (id,o')::keepl, anticipl) stk
@@ -117,7 +117,7 @@ let cwd () = fst !path_prefix
 let current_dirpath sec =
   Libnames.drop_dirpath_prefix (library_dp ()) 
     (if sec then cwd () 
-      else Libnames.extract_dirpath_prefix (sections_depth ()) (cwd ()))
+      else Libnames.pop_dirpath_n (sections_depth ()) (cwd ()))
     
 let make_path id = Libnames.make_path (cwd ()) id
 
@@ -211,10 +211,6 @@ let add_anonymous_entry node =
   add_entry name node;
   name
 
-let add_absolutely_named_leaf sp obj =
-  cache_object (sp,obj);
-  add_entry sp (Leaf obj)
-
 let add_leaf id obj =
   if fst (current_prefix ()) = Names.initial_path then 
     error ("No session module started (use -top dir)");
@@ -250,58 +246,55 @@ let add_frozen_state () =
 (* Modules. *)
 
 
-let is_something_opened = function 
-    (_,OpenedSection _) -> true 
-  | (_,OpenedModule _) -> true
-  | (_,OpenedModtype _) -> true
+let is_opened id = function 
+    oname,(OpenedSection _ | OpenedModule _ | OpenedModtype _) when
+      basename (fst oname) = id -> true
+  | _ -> false
+
+let is_opening_node = function 
+    _,(OpenedSection _ | OpenedModule _ | OpenedModtype _) -> true
   | _ -> false
 
 
 let current_mod_id () = 
-  try match find_entry_p is_something_opened with
-    | oname,OpenedModule (_,_,nametab) -> 
+  try match find_entry_p is_opening_node with
+    | oname,OpenedModule (_,_,fs) -> 
 	basename (fst oname)
-    | oname,OpenedModtype (_,nametab) -> 
+    | oname,OpenedModtype (_,fs) -> 
 	basename (fst oname)
     | _ -> error "you are not in a module"
   with Not_found ->
     error "no opened modules"
 
 
-let start_module export id mp nametab = 
-  let dir = extend_dirpath (fst !path_prefix) id in
+let start_module export id mp fs = 
+  let dir = add_dirpath_suffix (fst !path_prefix) id in
   let prefix = dir,(mp,Names.empty_dirpath) in
   let oname = make_path id, make_kn id in
   if Nametab.exists_module dir then
     errorlabstrm "open_module" (pr_id id ++ str " already exists") ;
-  add_entry oname (OpenedModule (export,prefix,nametab));
+  add_entry oname (OpenedModule (export,prefix,fs));
   path_prefix := prefix;
   prefix
 (*  add_frozen_state () must be called in declaremods *)
+
+let error_still_opened string oname =
+  let id = basename (fst oname) in
+  errorlabstrm "" (str string ++ spc () ++ pr_id id ++ str " is still opened.")
  
-let end_module id = 
-  let oname,nametab = 
-    try match find_entry_p is_something_opened with
-      | oname,OpenedModule (_,_,nametab) -> 
-	  let id' = basename (fst oname) in
-	    if id<>id' then 
-	      errorlabstrm "end_module" (str "last opened module is " ++ pr_id id'); 
-	    oname,nametab
-      | oname,OpenedModtype _ ->
-	  let id' = basename (fst oname) in
-	    errorlabstrm "end_module" 
-	      (str "module type " ++ pr_id id' ++ str " is still opened")
-      | oname,OpenedSection _ ->
-	  let id' = basename (fst oname) in
-	    errorlabstrm  "end_module" 
-	      (str "section " ++ pr_id id' ++ str " is still opened")
+let end_module () = 
+  let oname,fs = 
+    try match find_entry_p is_opening_node with
+      | oname,OpenedModule (_,_,fs) -> oname,fs
+      | oname,OpenedModtype _ -> error_still_opened "Module Type" oname
+      | oname,OpenedSection _ -> error_still_opened "Section" oname
       | _ -> assert false
     with Not_found ->
-      error "no opened modules"
+      error "No opened modules."
   in
   let (after,modopening,before) = split_lib oname in
   lib_stk := before;
-  add_entry (make_oname id) (ClosedModule (List.rev_append after (List.rev modopening)));
+  add_entry oname (ClosedModule (List.rev_append after (List.rev modopening)));
   let prefix = !path_prefix in
   (* LEM: This module business seems more complicated than sections;
           shouldn't a backtrack into a closed module also do something
@@ -311,48 +304,37 @@ let end_module id =
   recalc_path_prefix ();
   (* add_frozen_state must be called after processing the module, 
      because we cannot recache interactive modules  *) 
-  (oname, prefix, nametab,after)
+  (oname, prefix, fs, after)
 
-let start_modtype id mp nametab = 
-  let dir = extend_dirpath (fst !path_prefix) id in
+let start_modtype id mp fs = 
+  let dir = add_dirpath_suffix (fst !path_prefix) id in
   let prefix = dir,(mp,Names.empty_dirpath) in
   let sp = make_path id in
   let name = sp, make_kn id in
   if Nametab.exists_cci sp then
     errorlabstrm "open_modtype" (pr_id id ++ str " already exists") ;
-  add_entry name (OpenedModtype (prefix,nametab));
+  add_entry name (OpenedModtype (prefix,fs));
   path_prefix := prefix;
   prefix
 
-let end_modtype id = 
-  let sp,nametab = 
-    try match find_entry_p is_something_opened with
-      | oname,OpenedModtype (_,nametab) -> 
-	  let id' = basename (fst oname) in
-	  if id<>id' then 
-	    errorlabstrm "end_modtype" (str "last opened module type is " ++ pr_id id'); 
-	    oname,nametab
-      | oname,OpenedModule _ ->
-	  let id' = basename (fst oname) in
-	    errorlabstrm "end_modtype" 
-	      (str "module " ++ pr_id id' ++ str " is still opened")
-      | oname,OpenedSection _ ->
-	  let id' = basename (fst oname) in
-	    errorlabstrm "end_modtype" 
-	      (str "section " ++ pr_id id' ++ str " is still opened")
+let end_modtype () = 
+  let oname,fs = 
+    try match find_entry_p is_opening_node with
+      | oname,OpenedModtype (_,fs) -> oname,fs
+      | oname,OpenedModule _ -> error_still_opened "Module" oname
+      | oname,OpenedSection _ -> error_still_opened "Section" oname
       | _ -> assert false
     with Not_found ->
       error "no opened module types"
   in
-  let (after,modtypeopening,before) = split_lib sp in
+  let (after,modtypeopening,before) = split_lib oname in
   lib_stk := before;
-  add_entry (make_oname id) (ClosedModtype (List.rev_append after (List.rev modtypeopening)));
+  add_entry oname (ClosedModtype (List.rev_append after (List.rev modtypeopening)));
   let dir = !path_prefix in
   recalc_path_prefix ();
   (* add_frozen_state must be called after processing the module type.
      This is because we cannot recache interactive module types *) 
-  (sp,dir,nametab,after)
-
+  (oname,dir,fs,after)
 
 
 let contents_after = function
@@ -381,16 +363,16 @@ let start_compilation s mp =
 
 let end_compilation dir =
   let _ =
-    try match find_entry_p is_something_opened with
-      | _, OpenedSection _ -> error "There are some open sections"
-      | _, OpenedModule _ -> error "There are some open modules"
-      | _, OpenedModtype _ -> error "There are some open module types"
+    try match snd (find_entry_p is_opening_node) with
+      | OpenedSection _ -> error "There are some open sections."
+      | OpenedModule _ -> error "There are some open modules."
+      | OpenedModtype _ -> error "There are some open module types."
       | _ -> assert false
     with
 	Not_found -> () 
   in
   let module_p =
-    function (_,CompilingLibrary _) -> true | x -> is_something_opened x
+    function (_,CompilingLibrary _) -> true | x -> is_opening_node x
   in
   let oname = 
     try match find_entry_p module_p with
@@ -434,8 +416,12 @@ let is_module () =
 	Not_found -> false
 
 
-(* Returns the most recent OpenedThing node *)
-let what_is_opened () = find_entry_p is_something_opened
+(* Returns the opening node of a given name *)
+let find_opening_node id =
+  try snd (find_entry_p (is_opened id))
+  with Not_found -> 
+  try ignore (find_entry_p is_opening_node); error "There is nothing to end."
+  with Not_found -> error "Nothing to end of this name."
 
 (* Discharge tables *)
 
@@ -549,18 +535,18 @@ let set_xml_close_section f = xml_close_section := f
 
 let open_section id =
   let olddir,(mp,oldsec) = !path_prefix in
-  let dir = extend_dirpath olddir id in
-  let prefix = dir, (mp, extend_dirpath oldsec id) in
+  let dir = add_dirpath_suffix olddir id in
+  let prefix = dir, (mp, add_dirpath_suffix oldsec id) in
   let name = make_path id, make_kn id (* this makes little sense however *) in
-    if Nametab.exists_section dir then
-      errorlabstrm "open_section" (pr_id id ++ str " already exists");
-    let sum = freeze_summaries() in
-      add_entry name (OpenedSection (prefix, sum));
-      (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
-      Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
-      path_prefix := prefix;
-      if !Flags.xml_export then !xml_open_section id;
-      add_section ()
+  if Nametab.exists_section dir then
+    errorlabstrm "open_section" (pr_id id ++ str " already exists.");
+  let fs = freeze_summaries() in
+  add_entry name (OpenedSection (prefix, fs));
+  (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
+  Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
+  path_prefix := prefix;
+  if !Flags.xml_export then !xml_open_section id;
+  add_section ()
 
 
 (* Restore lib_stk and summaries as before the section opening, and
@@ -575,14 +561,10 @@ let discharge_item ((sp,_ as oname),e) =
   | OpenedSection _ | OpenedModtype _ | OpenedModule _ | CompilingLibrary _ ->
       anomaly "discharge_item"
 
-let close_section id =
+let close_section () =
   let oname,fs = 
-    try match find_entry_p is_something_opened with
-      | oname,OpenedSection (_,fs) -> 
-	  let id' = basename (fst oname) in 
-	    if id <> id' then 
-	      errorlabstrm "close_section" (str "Last opened section is " ++ pr_id id' ++ str ".");
-	    (oname,fs)
+    try match find_entry_p is_opening_node with
+      | oname,OpenedSection (_,fs) -> oname,fs
       | _ -> assert false 
     with Not_found ->
       error "No opened section."
@@ -591,8 +573,8 @@ let close_section id =
   lib_stk := before;
   let full_olddir = fst !path_prefix in
   pop_path_prefix ();
-  add_entry (make_oname id) (ClosedSection (List.rev_append secdecls (List.rev secopening)));
-  if !Flags.xml_export then !xml_close_section id;
+  add_entry oname (ClosedSection (List.rev_append secdecls (List.rev secopening)));
+  if !Flags.xml_export then !xml_close_section (basename (fst oname));
   let newdecls = List.map discharge_item secdecls in
   Summary.section_unfreeze_summaries fs;
   List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
@@ -826,7 +808,7 @@ let library_part ref =
     | _ -> dp_of_mp (mp_of_global ref)
 
 let remove_section_part ref =
-  let sp = Nametab.sp_of_global ref in
+  let sp = Nametab.path_of_global ref in
   let dir,_ = repr_path sp in
   match ref with
   | VarRef id -> 
@@ -834,7 +816,7 @@ let remove_section_part ref =
   | _ ->
       if is_dirpath_prefix_of dir (cwd ()) then
         (* Not yet (fully) discharged *)
-        extract_dirpath_prefix (sections_depth ()) (cwd ())
+        pop_dirpath_n (sections_depth ()) (cwd ())
       else
 	(* Theorem/Lemma outside its outer section of definition *)
 	dir
@@ -844,11 +826,11 @@ let remove_section_part ref =
 
 let pop_kn kn =
   let (mp,dir,l) = Names.repr_kn kn in
-  Names.make_kn mp (dirpath_prefix dir) l
+  Names.make_kn mp (pop_dirpath dir) l
 
 let pop_con con = 
   let (mp,dir,l) = Names.repr_con con in
-  Names.make_con mp (dirpath_prefix dir) l
+  Names.make_con mp (pop_dirpath dir) l
 
 let con_defined_in_sec kn = 
   let _,dir,_ = Names.repr_con kn in
diff --git a/library/lib.mli b/library/lib.mli
index 3330a20a7..1207511f0 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -52,7 +52,6 @@ val segment_of_objects :
   current list of operations (most recent ones coming first). *)
 
 val add_leaf : Names.identifier -> Libobject.obj -> Libnames.object_name
-val add_absolutely_named_leaf : Libnames.object_name -> Libobject.obj -> unit
 val add_anonymous_leaf : Libobject.obj -> unit
 
 (* this operation adds all objects with the same name and calls [load_object]
@@ -81,8 +80,8 @@ val contents_after : Libnames.object_name option -> library_segment
 (* User-side names *)
 val cwd : unit -> Names.dir_path
 val current_dirpath : bool -> Names.dir_path
-val make_path : Names.identifier -> Libnames.section_path
-val path_of_include : unit -> Libnames.section_path
+val make_path : Names.identifier -> Libnames.full_path
+val path_of_include : unit -> Libnames.full_path
 
 (* Kernel-side names *)
 val current_prefix : unit -> Names.module_path * Names.dir_path
@@ -98,20 +97,19 @@ val is_modtype : unit -> bool
 val is_module : unit -> bool
 val current_mod_id : unit -> Names.module_ident
 
-(* Returns the most recent OpenedThing node *)
-val what_is_opened : unit -> Libnames.object_name * node
-
+(* Returns the opening node of a given name *)
+val find_opening_node : Names.identifier -> node
 
 (*s Modules and module types *)
 
 val start_module : 
   bool option -> Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix
-val end_module : Names.module_ident 
+val end_module : unit
   -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment
 
 val start_modtype : 
   Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix
-val end_modtype : Names.module_ident 
+val end_modtype : unit
   -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment
 (* [Lib.add_frozen_state] must be called after each of the above functions *)
 
@@ -134,7 +132,7 @@ val remove_section_part : Libnames.global_reference -> Names.dir_path
 (*s Sections *)
 
 val open_section : Names.identifier -> unit
-val close_section : Names.identifier -> unit
+val close_section : unit -> unit
 
 (*s Backtracking (undo). *)
 
diff --git a/library/libnames.ml b/library/libnames.ml
index 44da7b6de..650b5c33f 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -66,6 +66,14 @@ module RefOrdered =
 module Refset = Set.Make(RefOrdered)
 module Refmap = Map.Make(RefOrdered)
 
+(* Extended global references *)
+
+type syndef_name = kernel_name
+
+type extended_global_reference =
+  | TrueGlobal of global_reference
+  | SynDef of syndef_name
+
 (**********************************************)
 
 let pr_dirpath sl = (str (string_of_dirpath sl))
@@ -73,10 +81,10 @@ let pr_dirpath sl = (str (string_of_dirpath sl))
 (*s Operations on dirpaths *)
 
 (* Pop the last n module idents *)
-let extract_dirpath_prefix n dir =
+let pop_dirpath_n n dir =
   make_dirpath (list_skipn n (repr_dirpath dir))
 
-let dirpath_prefix p = match repr_dirpath p with
+let pop_dirpath p = match repr_dirpath p with
   | [] -> anomaly "dirpath_prefix: empty dirpath"
   | _::l -> make_dirpath l
 
@@ -99,24 +107,8 @@ let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id])
 let split_dirpath d =
   let l = repr_dirpath d in (make_dirpath (List.tl l), List.hd l)
 
-let extend_dirpath p id = make_dirpath (id :: repr_dirpath p)
-
-
-(*
-let path_of_constructor env ((sp,tyi),ind) =
-   let mib = Environ.lookup_mind sp env in
-   let mip = mib.mind_packets.(tyi) in 
-   let (pa,_) = repr_path sp in 
-   Names.make_path pa (mip.mind_consnames.(ind-1))
+let add_dirpath_suffix p id = make_dirpath (id :: repr_dirpath p)
 
-let path_of_inductive env (sp,tyi) =
-  if tyi = 0 then sp
-  else
-    let mib = Environ.lookup_mind sp env in
-    let mip = mib.mind_packets.(tyi) in 
-    let (pa,_) = repr_path sp in 
-    Names.make_path pa (mip.mind_typename) 
-*)
 (* parsing *)
 let parse_dir s =
   let len = String.length s in
@@ -137,12 +129,15 @@ let parse_dir s =
 let dirpath_of_string s =
   make_dirpath (if s = "" then [] else parse_dir s)
 
+let string_of_dirpath = Names.string_of_dirpath
+
+
 module Dirset = Set.Make(struct type t = dir_path let compare = compare end)
 module Dirmap = Map.Make(struct type t = dir_path let compare = compare end)
 
 (*s Section paths are absolute names *)
 
-type section_path = {
+type full_path = {
   dirpath : dir_path ;
   basename : identifier }
 
@@ -163,7 +158,7 @@ let sp_ord sp1 sp2 =
 
 module SpOrdered =
   struct
-    type t = section_path
+    type t = full_path
     let compare = sp_ord
   end
 
@@ -181,17 +176,13 @@ let path_of_string s =
   with
     | Invalid_argument _ -> invalid_arg "path_of_string"
 
-let pr_sp sp = str (string_of_path sp) 
+let pr_path sp = str (string_of_path sp) 
 
 let restrict_path n sp =
   let dir, s = repr_path sp in
   let dir' = list_firstn n (repr_dirpath dir) in
   make_path (make_dirpath dir') s
 
-type extended_global_reference =
-  | TrueGlobal of global_reference
-  | SyntacticDef of kernel_name
-
 let encode_kn dir id = make_kn (MPfile dir) empty_dirpath (label_of_id id)
 
 let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id)
@@ -223,23 +214,23 @@ let decode_con kn =
       | _ -> anomaly "Section part should be empty!"
 
 (*s qualified names *)
-type qualid = section_path
+type qualid = full_path
 
 let make_qualid = make_path
 let repr_qualid = repr_path
 
 let string_of_qualid = string_of_path
-let pr_qualid = pr_sp
+let pr_qualid = pr_path
 
 let qualid_of_string = path_of_string
 
-let qualid_of_sp sp = sp
-let make_short_qualid id = make_qualid empty_dirpath id
+let qualid_of_path sp = sp
+let qualid_of_ident id = make_qualid empty_dirpath id
 let qualid_of_dirpath dir = 
   let (l,a) = split_dirpath dir in
   make_qualid l a
 
-type object_name = section_path * kernel_name
+type object_name = full_path * kernel_name
 
 type object_prefix = dir_path * (module_path * dir_path)
 
@@ -269,7 +260,7 @@ type reference =
 
 let qualid_of_reference = function
   | Qualid (loc,qid) -> loc, qid
-  | Ident (loc,id) -> loc, make_short_qualid id
+  | Ident (loc,id) -> loc, qualid_of_ident id
 
 let string_of_reference = function
   | Qualid (loc,qid) -> string_of_qualid qid
@@ -287,11 +278,11 @@ let loc_of_reference = function
 
 let pop_con con =
   let (mp,dir,l) = repr_con con in
-  Names.make_con mp (dirpath_prefix dir) l
+  Names.make_con mp (pop_dirpath dir) l
 
 let pop_kn kn =
   let (mp,dir,l) = repr_kn kn in
-  Names.make_kn mp (dirpath_prefix dir) l
+  Names.make_kn mp (pop_dirpath dir) l
 
 let pop_global_reference = function
   | ConstRef con -> ConstRef (pop_con con)
diff --git a/library/libnames.mli b/library/libnames.mli
index 399387dd7..e6591734b 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -42,53 +42,61 @@ val reference_of_constr : constr -> global_reference
 module Refset : Set.S with type elt = global_reference 
 module Refmap : Map.S with type key = global_reference
 
+(*s Extended global references *)
+
+type syndef_name = kernel_name
+
+type extended_global_reference =
+  | TrueGlobal of global_reference
+  | SynDef of syndef_name
+
 (*s Dirpaths *)
 val pr_dirpath : dir_path -> Pp.std_ppcmds
 
 val dirpath_of_string : string -> dir_path
+val string_of_dirpath : dir_path -> string
 
-(* Give the immediate prefix of a [dir_path] *)
-val dirpath_prefix : dir_path -> dir_path 
+(* Pop the suffix of a [dir_path] *)
+val pop_dirpath : dir_path -> dir_path 
+
+(* Pop the suffix n times *)
+val pop_dirpath_n : int -> dir_path -> dir_path
 
 (* Give the immediate prefix and basename of a [dir_path] *)
 val split_dirpath : dir_path -> dir_path * identifier
 
-val extend_dirpath : dir_path -> module_ident -> dir_path
+val add_dirpath_suffix : dir_path -> module_ident -> dir_path
 val add_dirpath_prefix : module_ident -> dir_path -> dir_path
 
 val chop_dirpath : int -> dir_path -> dir_path * dir_path
+val append_dirpath : dir_path -> dir_path -> dir_path
+
 val drop_dirpath_prefix : dir_path -> dir_path -> dir_path
-val extract_dirpath_prefix : int -> dir_path -> dir_path
 val is_dirpath_prefix_of : dir_path -> dir_path -> bool
-val append_dirpath : dir_path -> dir_path -> dir_path
 
 module Dirset : Set.S with type elt = dir_path
 module Dirmap : Map.S with type key = dir_path
 
-(*s Section paths are {\em absolute} names *)
-type section_path
+(*s Full paths are {\em absolute} paths of declarations *)
+type full_path
 
-(* Constructors of [section_path] *)
-val make_path : dir_path -> identifier -> section_path
+(* Constructors of [full_path] *)
+val make_path : dir_path -> identifier -> full_path
 
-(* Destructors of [section_path] *)
-val repr_path : section_path -> dir_path * identifier
-val dirpath : section_path -> dir_path
-val basename : section_path -> identifier
+(* Destructors of [full_path] *)
+val repr_path : full_path -> dir_path * identifier
+val dirpath : full_path -> dir_path
+val basename : full_path -> identifier
 
 (* Parsing and printing of section path as ["coq_root.module.id"] *)
-val path_of_string : string -> section_path
-val string_of_path : section_path -> string
-val pr_sp : section_path -> std_ppcmds
+val path_of_string : string -> full_path
+val string_of_path : full_path -> string
+val pr_path : full_path -> std_ppcmds
 
-module Sppred : Predicate.S with type elt = section_path
-module Spmap  : Map.S with type key = section_path
+module Sppred : Predicate.S with type elt = full_path
+module Spmap  : Map.S with type key = full_path
 
-val restrict_path : int -> section_path -> section_path
-
-type extended_global_reference =
-  | TrueGlobal of global_reference
-  | SyntacticDef of kernel_name
+val restrict_path : int -> full_path -> full_path
 
 (*s Temporary function to brutally form kernel names from section paths *)
 
@@ -100,29 +108,30 @@ val decode_con : constant -> dir_path * identifier
 
 (*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 *)
+    qualifications of absolute names, including single identifiers.
+    The [qualid] are used to access the name table. *)
+
 type qualid
 
 val make_qualid : dir_path -> identifier -> qualid
 val repr_qualid : qualid -> dir_path * identifier
 
-val string_of_qualid : qualid -> string
 val pr_qualid : qualid -> std_ppcmds
-
+val string_of_qualid : qualid -> string
 val qualid_of_string : string -> qualid
 
-(* Turns an absolute name into a qualified name denoting the same name *)
-val qualid_of_sp : section_path -> qualid
+(* Turns an absolute name, a dirpath, or an identifier into a
+   qualified name denoting the same name *)
 
+val qualid_of_path : full_path -> qualid
 val qualid_of_dirpath : dir_path -> qualid
-
-val make_short_qualid : identifier -> qualid
+val qualid_of_ident : identifier -> qualid
 
 (* Both names are passed to objects: a "semantic" [kernel_name], which
-   can be substituted and a "syntactic" [section_path] which can be printed
+   can be substituted and a "syntactic" [full_path] which can be printed
 *)
 
-type object_name = section_path * kernel_name
+type object_name = full_path * kernel_name
 
 type object_prefix = dir_path * (module_path * dir_path)
 
@@ -137,6 +146,10 @@ type global_dir_reference =
   | DirClosedSection of dir_path
       (* this won't last long I hope! *)
 
+(*s A [reference] is the user-level notion of name. It denotes either a
+    global name (referred either by a qualified name or by a single
+    name) or a variable *)
+
 type reference = 
   | Qualid of qualid located
   | Ident of identifier located
@@ -146,7 +159,7 @@ val string_of_reference : reference -> string
 val pr_reference : reference -> std_ppcmds
 val loc_of_reference : reference -> loc
 
-(* popping one level of section in global names *)
+(*s Popping one level of section in global names *)
 
 val pop_con : constant -> constant
 val pop_kn : kernel_name -> kernel_name
diff --git a/library/libobject.ml b/library/libobject.ml
index 90636dbee..504c1ffdd 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -33,7 +33,7 @@ type 'a object_declaration = {
   cache_function : object_name * 'a -> unit;
   load_function : int -> object_name * 'a -> unit;
   open_function : int -> object_name * 'a -> unit;
-  classify_function : object_name * 'a -> 'a substitutivity;
+  classify_function : 'a -> 'a substitutivity;
   subst_function : object_name * substitution * 'a -> 'a;
   discharge_function : object_name * 'a -> 'a option;
   rebuild_function : 'a -> 'a;
@@ -48,7 +48,7 @@ let default_object s = {
   open_function = (fun _ _ -> ());
   subst_function = (fun _ -> 
     yell ("The object "^s^" does not know how to substitute!"));
-  classify_function = (fun (_,obj) -> Keep obj);
+  classify_function = (fun obj -> Keep obj);
   discharge_function = (fun _ -> None);
   rebuild_function = (fun x -> x);
   export_function = (fun _ -> None)} 
@@ -74,7 +74,7 @@ type dynamic_object_declaration = {
   dyn_load_function : int -> object_name * obj -> unit;
   dyn_open_function : int -> object_name * obj -> unit;
   dyn_subst_function : object_name * substitution * obj -> obj;
-  dyn_classify_function : object_name * obj -> obj substitutivity;
+  dyn_classify_function : obj -> obj substitutivity;
   dyn_discharge_function : object_name * obj -> obj option;
   dyn_rebuild_function : obj -> obj;
   dyn_export_function : obj -> obj option }
@@ -100,9 +100,9 @@ let declare_object odecl =
     if Dyn.tag lobj = na then 
       infun (odecl.subst_function (oname,sub,outfun lobj))
     else anomaly "somehow we got the wrong dynamic object in the substfun"
-  and classifier (spopt,lobj) = 
+  and classifier lobj = 
     if Dyn.tag lobj = na then 
-      match odecl.classify_function (spopt,outfun lobj) with
+      match odecl.classify_function (outfun lobj) with
 	| Dispose -> Dispose
 	| Substitute obj -> Substitute (infun obj)
 	| Keep obj -> Keep (infun obj)
@@ -167,14 +167,14 @@ let open_object i ((_,lobj) as node) =
 let subst_object ((_,_,lobj) as node) = 
   apply_dyn_fun lobj (fun d -> d.dyn_subst_function node) lobj
 
-let classify_object ((_,lobj) as node) = 
-  apply_dyn_fun Dispose (fun d -> d.dyn_classify_function node) lobj
+let classify_object lobj = 
+  apply_dyn_fun Dispose (fun d -> d.dyn_classify_function lobj) lobj
 
 let discharge_object ((_,lobj) as node) = 
   apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj
 
-let rebuild_object (lobj as node) =
-  apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function node) lobj
+let rebuild_object lobj =
+  apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj
 
 let export_object lobj =
   apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj
diff --git a/library/libobject.mli b/library/libobject.mli
index d104635cd..f32d3baa7 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -76,7 +76,7 @@ type 'a object_declaration = {
   cache_function : object_name * 'a -> unit;
   load_function : int -> object_name * 'a -> unit;
   open_function : int -> object_name * 'a -> unit;
-  classify_function : object_name * 'a -> 'a substitutivity;
+  classify_function : 'a -> 'a substitutivity;
   subst_function : object_name * substitution * 'a -> 'a;
   discharge_function : object_name * 'a -> 'a option;
   rebuild_function : 'a -> 'a;
@@ -111,7 +111,7 @@ val cache_object : object_name * obj -> unit
 val load_object : int -> object_name * obj -> unit
 val open_object : int -> object_name * obj -> unit
 val subst_object : object_name * substitution * obj -> obj
-val classify_object : object_name * obj -> obj substitutivity
+val classify_object : obj -> obj substitutivity
 val export_object : obj -> obj option
 val discharge_object : object_name * obj -> obj option
 val rebuild_object : obj -> obj
diff --git a/library/library.ml b/library/library.ml
index abca3c7e7..24c2c3803 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -308,7 +308,7 @@ let subst_import (_,_,o) = o
 
 let export_import o = Some o
 
-let classify_import (_,(_,export as obj)) = 
+let classify_import (_,export as obj) = 
   if export then Substitute obj else Dispose
 
 
@@ -367,7 +367,7 @@ let locate_qualified_library warn qid =
     if loadpath = [] then raise LibUnmappedDir;
     let name = string_of_id base ^ ".vo" in
     let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name in
-    let dir = extend_dirpath (List.assoc lpath loadpath) base in
+    let dir = add_dirpath_suffix (List.assoc lpath loadpath) base in
     (* Look if loaded *)
     if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir)
     (* Otherwise, look for it in the file system *)
@@ -540,7 +540,7 @@ let (in_require, out_require) =
        open_function = (fun _ _ -> assert false);
        export_function = export_require;
        discharge_function = discharge_require;
-       classify_function = (fun (_,o) -> Anticipate o) }
+       classify_function = (fun o -> Anticipate o) }
 
 (* Require libraries, import them if [export <> None], mark them for export
    if [export = Some true] *)
@@ -615,7 +615,7 @@ let start_library f =
   let ldir0 = find_logical_path (Filename.dirname longf) in
   let id = id_of_string (Filename.basename f) in
   check_coq_overwriting ldir0 id;
-  let ldir = extend_dirpath ldir0 id in
+  let ldir = add_dirpath_suffix ldir0 id in
   Declaremods.start_library ldir;
   ldir,longf
 
diff --git a/library/nametab.ml b/library/nametab.ml
index 5bb21b3e5..7f148f0d3 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -27,7 +27,9 @@ let error_global_constant_not_found_loc loc q =
 
 let error_global_not_found q = raise (GlobalizationError q)
 
+(* Kinds of global names *)
 
+type ltac_constant = kernel_name
 
 (* The visibility can be registered either 
    - for all suffixes not shorter then a given int - when the object
@@ -42,7 +44,7 @@ type visibility = Until of int | Exactly of int
 (* Data structure for nametabs *******************************************)
 
 
-(* This module type will be instantiated by [section_path] of [dir_path] *)
+(* This module type will be instantiated by [full_path] of [dir_path] *)
 (* The [repr] function is assumed to return the reversed list of idents. *)
 module type UserName = sig 
   type t
@@ -251,7 +253,7 @@ end
 (* Global name tables *************************************************)
 
 module SpTab = Make (struct 
-		       type t = section_path
+		       type t = full_path
 		       let to_string = string_of_path
 		       let repr sp = 
 			 let dir,id = repr_path sp in
@@ -268,9 +270,6 @@ let the_tactictab = ref (SpTab.empty : kntab)
 type mptab = module_path SpTab.t
 let the_modtypetab = ref (SpTab.empty : mptab)
 
-type objtab = unit SpTab.t
-let the_objtab = ref (SpTab.empty : objtab)
-
 
 module DirTab = Make(struct 
 		       type t = dir_path
@@ -294,17 +293,17 @@ module Globrevtab = Map.Make(struct
 			       let compare = compare 
 			     end)
 
-type globrevtab = section_path Globrevtab.t
+type globrevtab = full_path Globrevtab.t
 let the_globrevtab = ref (Globrevtab.empty : globrevtab)
 
 
 type mprevtab = dir_path MPmap.t
 let the_modrevtab = ref (MPmap.empty : mprevtab)
 
-type mptrevtab = section_path MPmap.t
+type mptrevtab = full_path MPmap.t
 let the_modtyperevtab = ref (MPmap.empty : mptrevtab)
 
-type knrevtab = section_path KNmap.t
+type knrevtab = full_path KNmap.t
 let the_tacticrevtab = ref (KNmap.empty : knrevtab)
 
 
@@ -328,8 +327,8 @@ let push_cci visibility sp ref =
   push_xref visibility sp (TrueGlobal ref)
 
 (* This is for Syntactic Definitions *)
-let push_syntactic_definition visibility sp kn =
-  push_xref visibility sp (SyntacticDef kn)
+let push_syndef visibility sp kn =
+  push_xref visibility sp (SynDef kn)
 
 let push = push_cci
 
@@ -344,12 +343,6 @@ let push_tactic vis sp kn =
   the_tacticrevtab := KNmap.add kn sp !the_tacticrevtab
 
 
-(* This is for dischargeable non-cci objects (removed at the end of the
-   section -- i.e. Hints, Grammar ...) *) (* --> Unused *)
-
-let push_object visibility sp =
-  the_objtab := SpTab.push visibility sp () !the_objtab
-
 (* This is to remember absolute Section/Module names and to avoid redundancy *)
 let push_dir vis dir dir_ref = 
   the_dirtab := DirTab.push vis dir dir_ref !the_dirtab;
@@ -362,24 +355,21 @@ let push_dir vis dir dir_ref =
 
 
 (* This should be used when syntactic definitions are allowed *)
-let extended_locate qid = SpTab.locate qid !the_ccitab
+let locate_extended qid = SpTab.locate qid !the_ccitab
 
 (* This should be used when no syntactic definitions is expected *)
-let locate qid = match extended_locate qid with
+let locate qid = match locate_extended qid with
   | TrueGlobal ref -> ref
-  | SyntacticDef _ -> raise Not_found
+  | SynDef _ -> raise Not_found
 let full_name_cci qid = SpTab.user_name qid !the_ccitab
 
-let locate_syntactic_definition qid = match extended_locate qid with
+let locate_syndef qid = match locate_extended qid with
   | TrueGlobal _ -> raise Not_found
-  | SyntacticDef kn -> kn
+  | SynDef kn -> kn
 
 let locate_modtype qid = SpTab.locate qid !the_modtypetab
 let full_name_modtype qid = SpTab.user_name qid !the_modtypetab
 
-let locate_obj qid = SpTab.user_name qid !the_objtab
-
-type ltac_constant = kernel_name
 let locate_tactic qid = SpTab.locate qid !the_tactictab
 let full_name_tactic qid = SpTab.user_name qid !the_tactictab
 
@@ -405,35 +395,35 @@ let locate_all qid =
   List.fold_right (fun a l -> match a with TrueGlobal a -> a::l | _ -> l)
     (SpTab.find_prefixes qid !the_ccitab) []
 
-let extended_locate_all qid = SpTab.find_prefixes qid !the_ccitab
+let locate_extended_all qid = SpTab.find_prefixes qid !the_ccitab
 
 (* Derived functions *)
 
 let locate_constant qid =
-  match extended_locate qid with
+  match locate_extended qid with
     | TrueGlobal (ConstRef kn) -> kn
     | _ -> raise Not_found
 
 let locate_mind qid = 
-  match extended_locate qid with
+  match locate_extended qid with
     | TrueGlobal (IndRef (kn,0)) -> kn
     | _ -> raise Not_found
 
-let absolute_reference sp =
+let global_of_path sp =
   match SpTab.find sp !the_ccitab with
     | TrueGlobal ref -> ref
     | _ -> raise Not_found
 
-let extended_absolute_reference sp = SpTab.find sp !the_ccitab
+let extended_global_of_path sp = SpTab.find sp !the_ccitab
 
 let locate_in_absolute_module dir id =
-  absolute_reference (make_path dir id)
+  global_of_path (make_path dir id)
 
 let global r =
   let (loc,qid) = qualid_of_reference r in
-  try match extended_locate qid with
+  try match locate_extended qid with
     | TrueGlobal ref -> ref
-    | SyntacticDef _ -> 
+    | SynDef _ -> 
         user_err_loc (loc,"global",
           str "Unexpected reference to a notation: " ++
           pr_qualid qid)
@@ -456,18 +446,19 @@ let exists_tactic sp = SpTab.exists sp !the_tactictab
 
 (* Reverse locate functions ***********************************************)
 
-let sp_of_global ref = 
+let path_of_global ref = 
   match ref with
     | VarRef id -> make_path empty_dirpath id
     | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab
 
+let dirpath_of_global ref = 
+  fst (repr_path (path_of_global ref))
 
-let id_of_global ref = 
-  let (_,id) = repr_path (sp_of_global ref) in 
-  id
+let basename_of_global ref = 
+  snd (repr_path (path_of_global ref))
 
-let sp_of_syntactic_definition kn = 
-  Globrevtab.find (SyntacticDef kn) !the_globrevtab
+let path_of_syndef kn = 
+  Globrevtab.find (SynDef kn) !the_globrevtab
 
 let dir_of_mp mp =
   MPmap.find mp !the_modrevtab
@@ -483,7 +474,7 @@ let shortest_qualid_of_global ctx ref =
         SpTab.shortest_qualid ctx sp !the_ccitab
 
 let shortest_qualid_of_syndef ctx kn = 
-  let sp = sp_of_syntactic_definition kn in
+  let sp = path_of_syndef kn in
     SpTab.shortest_qualid ctx sp !the_ccitab
 
 let shortest_qualid_of_module mp = 
@@ -505,7 +496,7 @@ let pr_global_env env ref =
   let s = string_of_qualid (shortest_qualid_of_global env ref) in
   (str s)
 
-let inductive_of_reference r =
+let global_inductive r =
   match global r with
   | IndRef ind -> ind
   | ref ->
@@ -518,13 +509,12 @@ let inductive_of_reference r =
 (********************************************************************)
 (* Registration of tables as a global table and rollback            *)
 
-type frozen = ccitab * dirtab * objtab * kntab * kntab
+type frozen = ccitab * dirtab * kntab * kntab
     * globrevtab * mprevtab * knrevtab * knrevtab
 
 let init () = 
   the_ccitab := SpTab.empty; 
   the_dirtab := DirTab.empty;
-  the_objtab := SpTab.empty;
   the_modtypetab := SpTab.empty;
   the_tactictab := SpTab.empty;
   the_globrevtab := Globrevtab.empty;
@@ -537,7 +527,6 @@ let init () =
 let freeze () =
   !the_ccitab, 
   !the_dirtab,
-  !the_objtab,
   !the_modtypetab,
   !the_tactictab,
   !the_globrevtab,
@@ -545,10 +534,9 @@ let freeze () =
   !the_modtyperevtab,
   !the_tacticrevtab
 
-let unfreeze (ccit,dirt,objt,mtyt,tact,globr,modr,mtyr,tacr) =
+let unfreeze (ccit,dirt,mtyt,tact,globr,modr,mtyr,tacr) =
   the_ccitab := ccit;
   the_dirtab := dirt;
-  the_objtab := objt;
   the_modtypetab := mtyt;
   the_tactictab := tact;
   the_globrevtab := globr;
diff --git a/library/nametab.mli b/library/nametab.mli
index 225a8b080..c529120dd 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -16,7 +16,7 @@ open Libnames
 (*i*)
 
 (*s This module contains the tables for globalization, which
-  associates internal object references to qualified names (qualid). *)
+    associates internal object references to qualified names (qualid). *)
 
 (* Most functions in this module fall into one of the following categories:
    \begin{itemize}
@@ -24,7 +24,7 @@ open Libnames
    
    Registers the [object_reference] to be referred to by the
    [full_user_name] (and its suffixes according to [visibility]).
-   [full_user_name] can either be a [section_path] or a [dir_path].
+   [full_user_name] can either be a [full_path] or a [dir_path].
 
    \item [exists : full_user_name -> bool] 
    
@@ -34,8 +34,12 @@ open Libnames
    \item [locate : qualid -> object_reference]
 
    Finds the object referred to by [qualid] or raises [Not_found]
+
+   \item [full_name : qualid -> full_user_name]
+
+   Finds the full user name referred to by [qualid] or raises [Not_found]
    
-   \item [name_of : object_reference -> user_name]
+   \item [shortest_qualid_of : object_reference -> user_name]
 
    The [user_name] can be for example the shortest non ambiguous [qualid] or 
    the [full_user_name] or [identifier]. Such a function can also have a 
@@ -52,9 +56,6 @@ val error_global_not_found_loc : loc -> qualid -> 'a
 val error_global_not_found     : qualid -> 'a
 val error_global_constant_not_found_loc : loc -> qualid -> 'a
 
-
-
-
 (*s Register visibility of things *)
 
 (* The visibility can be registered either
@@ -70,88 +71,79 @@ val error_global_constant_not_found_loc : loc -> qualid -> 'a
 
 type visibility = Until of int | Exactly of int
 
-val push : visibility -> section_path -> global_reference -> unit
-val push_syntactic_definition : 
-  visibility -> section_path -> kernel_name -> unit
-val push_modtype : visibility -> section_path -> module_path -> unit
+val push : visibility -> full_path -> global_reference -> unit
+val push_modtype : visibility -> full_path -> module_path -> unit
 val push_dir : visibility -> dir_path -> global_dir_reference -> unit
-val push_object : visibility -> section_path -> unit
-val push_tactic : visibility -> section_path -> kernel_name -> unit
-
-
-(*s The following functions perform globalization of qualified names *)
-
-(* This returns the section path of a constant or fails with [Not_found] *)
-val locate : qualid -> global_reference
-
-(* This function is used to transform a qualified identifier into a
-   global reference, with a nice error message in case of failure *)
-val global : reference -> global_reference
-
-(* The same for inductive types *)
-val inductive_of_reference : reference -> inductive
+val push_syndef : visibility -> full_path -> syndef_name -> unit
 
-(* This locates also syntactic definitions; raise [Not_found] if not found *)
-val extended_locate : qualid -> extended_global_reference
+type ltac_constant = kernel_name
+val push_tactic : visibility -> full_path -> ltac_constant -> unit
 
-(* This locates all names with a given suffix, if qualid is valid as
-   such, it comes first in the list *)
-val extended_locate_all : qualid -> extended_global_reference list
 
-(* This locates all global references with a given suffixe *)
-val locate_all : qualid -> global_reference list
+(*s The following functions perform globalization of qualified names *)
 
-val locate_obj : qualid -> section_path
+(* These functions globalize a (partially) qualified name or fail with
+   [Not_found] *)
 
+val locate : qualid -> global_reference
+val locate_extended : qualid -> extended_global_reference
 val locate_constant : qualid -> constant
-val locate_mind : qualid -> mutual_inductive
-val locate_section : qualid -> dir_path
+val locate_syndef : qualid -> syndef_name
 val locate_modtype : qualid -> module_path
-val locate_syntactic_definition : qualid -> kernel_name
-
-type ltac_constant = kernel_name
-val locate_tactic : qualid -> ltac_constant
 val locate_dir : qualid -> global_dir_reference
 val locate_module : qualid -> module_path
+val locate_section : qualid -> dir_path
+val locate_tactic : qualid -> ltac_constant
 
-(* A variant looking up a [section_path] *)
-val absolute_reference : section_path -> global_reference
-val extended_absolute_reference : section_path -> extended_global_reference
+(* These functions globalize user-level references into global
+   references, like [locate] and co, but raise a nice error message
+   in case of failure *)
 
+val global : reference -> global_reference
+val global_inductive : reference -> inductive
 
-(*s These functions tell if the given absolute name is already taken *)
+(* These functions locate all global references with a given suffix;
+   if [qualid] is valid as such, it comes first in the list *)
 
-val exists_cci : section_path -> bool
-val exists_modtype : section_path -> bool
+val locate_all : qualid -> global_reference list
+val locate_extended_all : qualid -> extended_global_reference list
 
-(* Those three functions are the same *)
-val exists_dir : dir_path -> bool
-val exists_section : dir_path -> bool (* deprecated *)
-val exists_module : dir_path -> bool (* deprecated *)
+(* Mapping a full path to a global reference *)
 
+val global_of_path : full_path -> global_reference
+val extended_global_of_path : full_path -> extended_global_reference
 
-(*s These functions turn qualids into full user names: [section_path]s
-  or [dir_path]s *)
+(*s These functions tell if the given absolute name is already taken *)
 
-val full_name_modtype : qualid -> section_path
-val full_name_cci : qualid -> section_path
+val exists_cci : full_path -> bool
+val exists_modtype : full_path -> bool
+val exists_dir : dir_path -> bool
+val exists_section : dir_path -> bool (* deprecated synonym of [exists_dir] *)
+val exists_module : dir_path -> bool (* deprecated synonym of [exists_dir] *)
 
-(* As above but checks that the path found is indeed a module *)
-val full_name_module : qualid -> dir_path
+(*s These functions locate qualids into full user names *)
 
+val full_name_cci : qualid -> full_path
+val full_name_modtype : qualid -> full_path
+val full_name_module : qualid -> dir_path
 
 (*s Reverse lookup -- finding user names corresponding to the given
   internal name *)
 
-val sp_of_syntactic_definition : kernel_name -> section_path
-val shortest_qualid_of_global : Idset.t -> global_reference -> qualid
-val shortest_qualid_of_syndef : Idset.t -> kernel_name -> qualid
-val shortest_qualid_of_tactic : ltac_constant -> qualid
+(* Returns the dirpath associated to a module path *)
 
 val dir_of_mp : module_path -> dir_path
 
-val sp_of_global : global_reference -> section_path
-val id_of_global : global_reference -> identifier
+(* Returns full path bound to a global reference or syntactic definition *)
+
+val path_of_syndef : syndef_name -> full_path
+val path_of_global : global_reference -> full_path
+
+(* Returns in particular the dirpath or the basename of the full path
+   associated to global reference *)
+
+val dirpath_of_global : global_reference -> dir_path
+val basename_of_global : global_reference -> identifier
 
 (* Printing of global references using names as short as possible *)
 val pr_global_env : Idset.t -> global_reference -> std_ppcmds
@@ -161,13 +153,8 @@ val pr_global_env : Idset.t -> global_reference -> std_ppcmds
    Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and
    Coq.A.B.x that denotes the same object. *)
 
-val shortest_qualid_of_module : module_path -> qualid
+val shortest_qualid_of_global : Idset.t -> global_reference -> qualid
+val shortest_qualid_of_syndef : Idset.t -> syndef_name -> qualid
 val shortest_qualid_of_modtype : module_path -> qualid
-
-
-(*
-type frozen
-
-val freeze : unit -> frozen
-val unfreeze : frozen -> unit
-*)
+val shortest_qualid_of_module : module_path -> qualid
+val shortest_qualid_of_tactic : ltac_constant -> qualid