- 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

83 files changed, 506 insertions, 585 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 92ea62b5e..ebbcb46ce 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,6 +2,28 @@
 = CHANGES BETWEEN COQ V8.2 AND COQ V8.3 =
 =========================================
 
+** Cleaning in libnames/nametab interfaces
+
+Functions:
+
+dirpath_prefix -> pop_dirpath
+extract_dirpath_prefix pop_dirpath_n
+extend_dirpath -> add_dirpath_suffix
+qualid_of_sp -> qualid_of_path
+pr_sp -> pr_path
+make_short_qualid -> qualid_of_ident
+sp_of_syntactic_definition -> path_of_syntactic_definition 
+sp_of_global -> path_of_global
+id_of_global -> basename_of_global
+absolute_reference -> global_of_path
+locate_syntactic_definition -> locate_syndef
+path_of_syntactic_definition -> path_of_syndef
+push_syntactic_definition -> push_syndef
+
+Types:
+
+section_path -> full_path
+
 ** Cleaning in parsing extensions (commit 12108)
 
 Many moves and renamings, one new file (Extrawit, that contains wit_tactic).
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e3addd6f0..b35d5d489 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -46,7 +46,7 @@ let ppdir dir = pp (pr_dirpath dir)
 let ppmp mp = pp(str (string_of_mp mp))
 let ppcon con = pp(pr_con con)
 let ppkn kn = pp(pr_kn kn)
-let ppsp sp = pp(pr_sp sp)
+let ppsp sp = pp(pr_path sp)
 let ppqualid qid = pp(pr_qualid qid)
 let ppclindex cl = pp(Classops.pr_cl_index cl)
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1d89306ed..e4e625205 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -336,11 +336,11 @@ let check_no_explicitation l =
 
 (* Is it a global reference or a syntactic definition? *)
 let intern_qualid loc qid intern env args =
-  try match Nametab.extended_locate qid with
+  try match Nametab.locate_extended qid with
   | TrueGlobal ref ->
       Dumpglob.add_glob loc ref;
       RRef (loc, ref), args
-  | SyntacticDef sp ->
+  | SynDef sp ->
       Dumpglob.add_glob_kn loc sp;
       let (ids,c) = Syntax_def.search_syntactic_definition loc sp in
       let nids = List.length ids in
@@ -365,7 +365,7 @@ let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function
   | Ident (loc, id) ->
       try intern_var env lvar loc id, args
       with Not_found -> 
-      let qid = make_short_qualid id in
+      let qid = qualid_of_ident id in
       try
 	let r,args2 = intern_non_secvar_qualid loc qid intern env args in
 	find_appl_head_data lvar r, args2
@@ -536,10 +536,10 @@ type pattern_qualid_kind =
 let find_constructor ref f aliases pats scopes =
   let (loc,qid) = qualid_of_reference ref in
   let gref =
-    try extended_locate qid
+    try locate_extended qid
     with Not_found -> raise (InternalisationError (loc,NotAConstructor ref)) in
   match gref with
-  | SyntacticDef sp ->
+  | SynDef sp ->
       let (vars,a) = Syntax_def.search_syntactic_definition loc sp in
       (match a with
        | ARef (ConstructRef cstr) ->
@@ -1357,21 +1357,21 @@ let interp_context_evars ?(fail_anonymous=false) evdref env params =
 (* Locating reference, possibly via an abbreviation *)
 
 let locate_reference qid =
-  match Nametab.extended_locate qid with
+  match Nametab.locate_extended qid with
     | TrueGlobal ref -> ref
-    | SyntacticDef kn -> 
+    | SynDef kn -> 
 	match Syntax_def.search_syntactic_definition dummy_loc kn with
 	  | [],ARef ref -> ref
 	  | _ -> raise Not_found
 
 let is_global id =
   try 
-    let _ = locate_reference (make_short_qualid id) in true
+    let _ = locate_reference (qualid_of_ident id) in true
   with Not_found -> 
     false
 
 let global_reference id = 
-  constr_of_global (locate_reference (make_short_qualid id))
+  constr_of_global (locate_reference (qualid_of_ident id))
 
 let construct_reference ctx id =
   try
@@ -1380,5 +1380,5 @@ let construct_reference ctx id =
     global_reference id
 
 let global_reference_in_absolute_module dir id = 
-  constr_of_global (Nametab.absolute_reference (Libnames.make_path dir id))
+  constr_of_global (Nametab.global_of_path (Libnames.make_path dir id))
 
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index e110ad00a..d38ef592f 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -26,7 +26,7 @@ let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
 
 let find_reference locstr dir s =
   let sp = Libnames.make_path (make_dir dir) (id_of_string s) in
-  try global_of_extended_global (Nametab.extended_absolute_reference sp)
+  try global_of_extended_global (Nametab.extended_global_of_path sp)
   with Not_found -> anomaly (locstr^": cannot find "^(string_of_path sp))
 
 let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s
@@ -36,7 +36,7 @@ let gen_reference = coq_reference
 let gen_constant = coq_constant
 
 let has_suffix_in_dirs dirs ref =
-  let dir = dirpath (sp_of_global ref) in
+  let dir = dirpath (path_of_global ref) in
   List.exists (fun d -> is_dirpath_prefix_of d dir) dirs
 
 let global_of_extended q =
@@ -45,7 +45,7 @@ let global_of_extended q =
 let gen_constant_in_modules locstr dirs s =
   let dirs = List.map make_dir dirs in
   let id = id_of_string s in
-  let all = Nametab.extended_locate_all (make_short_qualid id) in
+  let all = Nametab.locate_extended_all (qualid_of_ident id) in
   let all = list_uniquize (list_map_filter global_of_extended all) in
   let these = List.filter (has_suffix_in_dirs dirs) all in
   match these with
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 5b550a86b..8b0384960 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -59,7 +59,7 @@ val logic_module : dir_path
 val logic_type_module : dir_path
 
 (* Natural numbers *)
-val nat_path : section_path
+val nat_path : full_path
 val glob_nat : global_reference
 val path_of_O : constructor
 val path_of_S : constructor
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 71f38063a..79b58da84 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -118,7 +118,7 @@ let type_of_global_ref gr =
 let remove_sections dir =
   if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then
     (* Not yet (fully) discharged *)
-    Libnames.extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())
+    Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ())
   else
     (* Theorem/Lemma outside its outer section of definition *)
     dir
@@ -139,7 +139,7 @@ let add_glob_gen loc sp lib_dp ty =
 
 let add_glob loc ref = 
   if dump () && loc <> Util.dummy_loc then
-    let sp = Nametab.sp_of_global ref in
+    let sp = Nametab.path_of_global ref in
     let lib_dp = Lib.library_part ref in
     let ty = type_of_global_ref ref in
       add_glob_gen loc sp lib_dp ty
@@ -150,7 +150,7 @@ let mp_of_kn kn =
 
 let add_glob_kn loc kn =
   if dump () && loc <> Util.dummy_loc then
-    let sp = Nametab.sp_of_syntactic_definition kn in
+    let sp = Nametab.path_of_syndef kn in
     let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
       add_glob_gen loc sp lib_dp "syndef"
 
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 4495c22c6..a550111a3 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -30,13 +30,13 @@ let ids_of_list l =
   List.fold_right Idset.add l Idset.empty
 
 let locate_reference qid =
-  match Nametab.extended_locate qid with
+  match Nametab.locate_extended qid with
     | TrueGlobal ref -> true
-    | SyntacticDef kn -> true
+    | SynDef kn -> true
 
 let is_global id =
   try 
-    locate_reference (make_short_qualid id)
+    locate_reference (qualid_of_ident id)
   with Not_found -> 
     false
 
diff --git a/interp/notation.ml b/interp/notation.ml
index e6c627e86..2857f9ad8 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -113,7 +113,7 @@ let subst_scope (_,subst,sc) = sc
 
 open Libobject
 
-let classify_scope (_,(local,_,_ as o)) =
+let classify_scope (local,_,_ as o) =
   if local then Dispose else Substitute o
 
 let export_scope (local,_,_ as x) = if local then None else Some x
@@ -201,7 +201,7 @@ let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
 (**********************************************************************)
 (* Interpreting numbers (not in summary because functional objects)   *)
 
-type required_module = section_path * string list 
+type required_module = full_path * string list 
 
 type 'a prim_token_interpreter =
     loc -> 'a -> rawconstr
@@ -248,7 +248,7 @@ let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
     (patl, (fun r -> Option.map mkString (uninterp r)), inpat)
 
 let check_required_module loc sc (sp,d) =
-  try let _ = Nametab.absolute_reference sp in ()
+  try let _ = Nametab.global_of_path sp in ()
   with Not_found ->
     user_err_loc (loc,"prim_token_interpreter",
     str ("Cannot interpret in "^sc^" without requiring first module "
@@ -485,7 +485,7 @@ let (inArgumentsScope,outArgumentsScope) =
       cache_function = cache_arguments_scope;
       load_function = load_arguments_scope;
       subst_function = subst_arguments_scope;
-      classify_function = (fun (_,o) -> Substitute o);
+      classify_function = (fun o -> Substitute o);
       discharge_function = discharge_arguments_scope;
       rebuild_function = rebuild_arguments_scope;
       export_function = (fun x -> Some x) }
diff --git a/interp/notation.mli b/interp/notation.mli
index 06349014d..21d3ae1a0 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -66,7 +66,7 @@ val find_delimiters_scope : loc -> delimiters -> scope_name
    an appropriate error message *)
 
 type notation_location = dir_path * string
-type required_module = section_path * string list 
+type required_module = full_path * string list 
 type cases_pattern_status = bool (* true = use prim token in patterns *)
 
 type 'a prim_token_interpreter =
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index bb8d68323..ef5ecf62a 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -16,6 +16,7 @@ open Topconstr
 open Libobject
 open Lib
 open Nameops
+open Nametab
 
 (* Syntactic definitions. *)
 
@@ -37,13 +38,13 @@ let load_syntax_constant i ((sp,kn),(local,pat,onlyparse)) =
     errorlabstrm "cache_syntax_constant"
       (pr_id (basename sp) ++ str " already exists");
   add_syntax_constant kn pat;
-  Nametab.push_syntactic_definition (Nametab.Until i) sp kn;
+  Nametab.push_syndef (Nametab.Until i) sp kn;
   if not onlyparse then
     (* Declare it to be used as long name *)
     Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
 
 let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
-  Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn;
+  Nametab.push_syndef (Nametab.Exactly i) sp kn;
   if not onlyparse then
     (* Redeclare it to be used as (short) name in case an other (distfix)
        notation was declared inbetween *)
@@ -55,7 +56,7 @@ let cache_syntax_constant d =
 let subst_syntax_constant ((sp,kn),subst,(local,pat,onlyparse)) =
   (local,subst_interpretation subst pat,onlyparse)
 
-let classify_syntax_constant (_,(local,_,_ as o)) =
+let classify_syntax_constant (local,_,_ as o) =
   if local then Dispose else Substitute o
 
 let export_syntax_constant (local,_,_ as o) =
@@ -85,19 +86,19 @@ let search_syntactic_definition loc kn =
 
 let global_of_extended_global = function
   | TrueGlobal ref -> ref
-  | SyntacticDef kn -> 
+  | SynDef kn -> 
   match search_syntactic_definition dummy_loc kn with
   | [],ARef ref -> ref
   | _ -> raise Not_found
 
 let locate_global_with_alias (loc,qid) =
-  let ref = Nametab.extended_locate qid in
+  let ref = Nametab.locate_extended qid in
   try global_of_extended_global ref
   with Not_found ->
     user_err_loc (loc,"",pr_qualid qid ++ 
       str " is bound to a notation that does not denote a reference")
 
-let inductive_of_reference_with_alias r =
+let global_inductive_with_alias r =
   match locate_global_with_alias (qualid_of_reference r) with
   | IndRef ind -> ind
   | ref ->
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 39583d856..fb0c3c9f2 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -13,6 +13,7 @@ open Util
 open Names
 open Topconstr
 open Rawterm
+open Nametab
 open Libnames
 (*i*)
 
@@ -39,4 +40,4 @@ val global_of_extended_global : extended_global_reference -> global_reference
 val global_with_alias : reference -> global_reference
 
 (* The same for inductive types *)
-val inductive_of_reference_with_alias : reference -> inductive
+val global_inductive_with_alias : reference -> inductive
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 32595cdc6..eb46a5d6e 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -770,7 +770,7 @@ let ids_of_cases_tomatch tms =
     tms []
 
 let is_constructor id =
-  try ignore (Nametab.extended_locate (make_short_qualid id)); true
+  try ignore (Nametab.locate_extended (qualid_of_ident id)); true
   with Not_found -> true
  
 let rec cases_pattern_fold_names f a = function
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index a5cda5d13..edd3e498d 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -21,17 +21,17 @@ open Reduction
 
 type work_list = identifier array Cmap.t * identifier array KNmap.t
 
-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
 
 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
 
 type my_global_reference =
   | ConstRef of constant
diff --git a/lib/util.mli b/lib/util.mli
index 04d3a52fc..84762bade 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -171,6 +171,7 @@ val list_lastn : int -> 'a list -> 'a list
 val list_skipn : int -> 'a list -> 'a list 
 val list_addn : int -> 'a -> 'a list -> 'a list
 val list_prefix_of : 'a list -> 'a list -> bool
+(* [list_drop_prefix p l] returns [t] if [l=p++t] else return [l] *)
 val list_drop_prefix : 'a list -> 'a list -> 'a list
 val list_drop_last : 'a list -> 'a list
 (* [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
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
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 524e7b468..0e91fddbd 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -71,7 +71,7 @@ GEXTEND Gram
   ;
   basequalid:
     [ [ id = ident; (l,id')=fields -> local_make_qualid (l@[id]) id'
-      | id = ident -> make_short_qualid id
+      | id = ident -> qualid_of_ident id
       ] ]
   ;
   name:
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index cf88256bc..538828fca 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -191,7 +191,7 @@ let locate_any_name ref =
   let (loc,qid) = qualid_of_reference ref in
   try Term (N.locate qid)
   with Not_found -> 
-  try Syntactic (N.locate_syntactic_definition qid)
+  try Syntactic (N.locate_syndef qid)
   with Not_found ->
   try Dir (N.locate_dir qid)
   with Not_found ->
@@ -205,9 +205,9 @@ let pr_located_qualid = function
 	| IndRef _ -> "Inductive"
 	| ConstructRef _ -> "Constructor"
 	| VarRef _ -> "Variable" in
-      str ref_str ++ spc () ++ pr_sp (Nametab.sp_of_global ref)
+      str ref_str ++ spc () ++ pr_global ref
   | Syntactic kn ->
-      str "Notation" ++ spc () ++ pr_sp (Nametab.sp_of_syntactic_definition kn)
+      str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn)
   | Dir dir ->
       let s,dir = match dir with
 	| DirOpenModule (dir,_) -> "Open Module", dir
@@ -218,7 +218,7 @@ let pr_located_qualid = function
       in
       str s ++ spc () ++ pr_dirpath dir
   | ModuleType (qid,_) ->
-      str "Module Type" ++ spc () ++ pr_sp (Nametab.full_name_modtype qid)
+      str "Module Type" ++ spc () ++ pr_path (Nametab.full_name_modtype qid)
   | Undefined qid ->    
       pr_qualid qid ++ spc () ++ str "not a defined object."
 
@@ -228,9 +228,9 @@ let print_located_qualid ref =
   let expand = function
     | TrueGlobal ref ->
 	Term ref, N.shortest_qualid_of_global Idset.empty ref
-    | SyntacticDef kn ->
+    | SynDef kn ->
 	Syntactic kn, N.shortest_qualid_of_syndef Idset.empty kn in
-  match List.map expand (N.extended_locate_all qid) with
+  match List.map expand (N.locate_extended_all qid) with
     | [] -> 
 	let (dir,id) = repr_qualid qid in
 	if dir = empty_dirpath then
@@ -636,18 +636,6 @@ let print_name ref =
     let (_,c,typ) = Global.lookup_named str in 
     (print_named_decl (str,c,typ))
   with Not_found ->
-  try 
-    let sp = Nametab.locate_obj qid in
-    let (oname,lobj) = 
-      let (oname,entry) =
-	List.find (fun en -> (fst (fst en)) = sp) (Lib.contents_after None)
-      in
-      match entry with
-	| Lib.Leaf obj -> (oname,obj)
-	| _ -> raise Not_found
-    in
-    print_leaf_entry true (oname,lobj)
-  with Not_found ->
     errorlabstrm
       "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
 
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index 596ce6b24..2ec914d6c 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -137,7 +137,7 @@ and print_modexpr locals mexpr = match mexpr with
 
 
 let rec printable_body dir =     
-  let dir = dirpath_prefix dir in
+  let dir = pop_dirpath dir in
     dir = empty_dirpath || 
     try 
       match Nametab.locate_dir (qualid_of_dirpath dir) with
diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index 79ffaf3f9..3a408909d 100644
--- a/plugins/dp/dp.ml
+++ b/plugins/dp/dp.ml
@@ -115,7 +115,7 @@ let rename_global r =
 	s
       end
     in
-    loop (Nametab.id_of_global r)
+    loop (Nametab.basename_of_global r)
 
 let foralls =
   List.fold_right 
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 11c3b3b5b..e1edeec37 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -303,9 +303,9 @@ let ref_renaming_fun (k,r) =
     if l = [""] (* this happens only at toplevel of the monolithic case *)
     then
       let globs = Idset.elements (get_global_ids ()) in
-      let id = next_ident_away (kindcase_id k (safe_id_of_global r)) globs in
+      let id = next_ident_away (kindcase_id k (safe_basename_of_global r)) globs in
       string_of_id id
-    else modular_rename k (safe_id_of_global r)
+    else modular_rename k (safe_basename_of_global r)
   in
   add_global_ids (id_of_string s);
   s::l
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 39e277081..ba4786d37 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -506,7 +506,7 @@ let simple_extraction r = match locate_ref [r] with
 let extraction_library is_rec m =
   init true;
   let dir_m =
-    let q = make_short_qualid m in
+    let q = qualid_of_ident m in
     try Nametab.full_name_module q with Not_found -> error_unknown_module q
   in
   Visit.add_mp (MPfile dir_m);
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 83a780198..13a730ac2 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -182,7 +182,7 @@ let modular () = !modular_ref
    WARNING: for inductive objects, an extract_inductive must have been
    done before. *)
 
-let safe_id_of_global = function
+let safe_basename_of_global = function
   | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
   | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename
   | ConstructRef ((kn,i),j) ->
@@ -191,7 +191,7 @@ let safe_id_of_global = function
 
 let safe_pr_global r =
  try Printer.pr_global r
- with _ -> pr_id (safe_id_of_global r)
+ with _ -> pr_id (safe_basename_of_global r)
 
 (* idem, but with qualification, and only for constants. *)
 
@@ -207,7 +207,7 @@ let pr_long_mp mp =
   let lid = repr_dirpath (Nametab.dir_of_mp mp) in
   str (String.concat "." (List.map string_of_id (List.rev lid)))
 
-let pr_long_global ref = pr_sp (Nametab.sp_of_global ref)
+let pr_long_global ref = pr_path (Nametab.path_of_global ref)
 
 (*S Warning and Error messages. *)
 
@@ -452,7 +452,7 @@ let (inline_extraction,_) =
        cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
        load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
        export_function = (fun x -> Some x);
-       classify_function = (fun (_,o) -> Substitute o);
+       classify_function = (fun o -> Substitute o);
        subst_function =
         (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
     }
@@ -535,7 +535,7 @@ let (blacklist_extraction,_) =
        cache_function = (fun (_,l) -> add_blacklist_entries l);
        load_function = (fun _ (_,l) -> add_blacklist_entries l);
        export_function = (fun x -> Some x);
-       classify_function = (fun (_,o) -> Libobject.Keep o);
+       classify_function = (fun o -> Libobject.Keep o);
        subst_function = (fun (_,_,x) -> x)
     }
 
@@ -595,7 +595,7 @@ let (in_customs,_) =
        cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
        load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s);
        export_function = (fun x -> Some x);
-       classify_function = (fun (_,o) -> Substitute o);
+       classify_function = (fun o -> Substitute o);
        subst_function =
         (fun (_,s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
     }
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 6e3f2ec56..42ed6eef0 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -13,7 +13,7 @@ open Libnames
 open Miniml
 open Declarations
 
-val safe_id_of_global : global_reference -> identifier
+val safe_basename_of_global : global_reference -> identifier
 
 (*s Warning and Error messages. *)
 
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
index c9b993690..916294774 100644
--- a/plugins/field/field.ml4
+++ b/plugins/field/field.ml4
@@ -75,7 +75,7 @@ let (in_addfield,out_addfield)=
        Libobject.open_function = (fun i o -> if i=1 then cache_addfield o);
        Libobject.cache_function = cache_addfield;
        Libobject.subst_function = subst_addfield;
-       Libobject.classify_function = (fun (_,a) -> Libobject.Substitute a);
+       Libobject.classify_function = (fun a -> Libobject.Substitute a);
        Libobject.export_function = export_addfield }
 
 (* Adds a theory to the table *)
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index fc31ee6fc..75d69099a 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -45,7 +45,7 @@ let wrap n b continue seq gls=
     add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in
     continue seq2 gls
 
-let id_of_global=function
+let basename_of_global=function
     VarRef id->id
   | _->assert false
 
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 1c2c93a49..b804c93ae 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -21,7 +21,7 @@ type 'a with_backtracking = tactic -> 'a
 
 val wrap : int -> bool -> seqtac
 
-val id_of_global: global_reference -> identifier
+val basename_of_global: global_reference -> identifier
 
 val clear_global: global_reference -> tactic
 
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index adfb9ce2f..9087f5179 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1000,7 +1000,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
 	      let finfos = find_Function_infos (destConst f) in 
 	      update_Function 
 		{finfos with
-		   equation_lemma = Some (match Nametab.locate (make_short_qualid equation_lemma_id) with
+		   equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
 					      ConstRef c -> c
 					    | _ -> Util.anomaly "Not a constant" 
 					 )
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 348a17b11..46da3a01d 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -471,7 +471,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b
   in
   let ltof = 
     let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) in 
-    Libnames.Qualid (dummy_loc,Libnames.qualid_of_sp 
+    Libnames.Qualid (dummy_loc,Libnames.qualid_of_path 
       (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (id_of_string "ltof")))
   in
   let fun_from_mes = 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index b29bdf3f1..868a876be 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -350,7 +350,7 @@ let subst_Function (_,subst,finfos) =
       is_general = finfos.is_general
     }
 
-let classify_Function (_,infos) = Libobject.Substitute infos
+let classify_Function infos = Libobject.Substitute infos
 
 let export_Function infos = Some infos
 
@@ -440,7 +440,7 @@ let _ =
 
 let find_or_none id = 
   try Some 
-    (match Nametab.locate (make_short_qualid id) with ConstRef c -> c | _ -> Util.anomaly "Not a constant" 
+    (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Util.anomaly "Not a constant" 
     ) 
   with Not_found -> None
 
@@ -467,7 +467,7 @@ let add_Function is_general f =
   and rec_lemma = find_or_none (Nameops.add_suffix f_id "_rec")
   and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
   and graph_ind = 
-    match Nametab.locate (make_short_qualid (mk_rel_id f_id)) 
+    match Nametab.locate (qualid_of_ident (mk_rel_id f_id)) 
     with | IndRef ind -> ind | _ -> Util.anomaly "Not an inductive"
   in
   let finfos = 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 25e664336..876f3de4b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1386,7 +1386,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let tcc_lemma_constr = ref None in 
 (*   let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
   let hook _ _ =   
-    let term_ref = Nametab.locate (make_short_qualid term_id) in
+    let term_ref = Nametab.locate (qualid_of_ident term_id) in
     let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
 (*     message "start second proof"; *)
     let stop = ref false in 
@@ -1404,7 +1404,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
     end;
     if not !stop
     then
-      let eq_ref = Nametab.locate (make_short_qualid equation_id ) in
+      let eq_ref = Nametab.locate (qualid_of_ident equation_id ) in
       let f_ref = destConst (constr_of_global f_ref) 
       and functional_ref = destConst (constr_of_global functional_ref) 
       and eq_ref = destConst (constr_of_global eq_ref) in
diff --git a/plugins/interface/centaur.ml4 b/plugins/interface/centaur.ml4
index f8c088779..c8fc7bdf3 100644
--- a/plugins/interface/centaur.ml4
+++ b/plugins/interface/centaur.ml4
@@ -146,7 +146,7 @@ let ctf_acknowledge_command request_id command_count opt_exn =
         g_count, !current_goal_index
     else
       (0, 0)
-  and statnum = Lib.current_command_label ()
+  and statnum = Lib.current_state_label ()
   and dpth = let d = Pfedit.current_proof_depth() in if d >= 0 then d else 0
   and pending = CT_id_list (List.map xlate_ident (Pfedit.get_all_proof_names())) in
    (ctf_header "acknowledge" request_id ++
@@ -409,12 +409,12 @@ let inspect n =
 		  (match oname, object_tag lobj with
                        (sp,_), "VARIABLE" ->
 			 let (_, _, v) = Global.lookup_named (basename sp) in
-			   add_search2 (Nametab.locate (qualid_of_sp sp)) v
+			   add_search2 (Nametab.locate (qualid_of_path sp)) v
 		     | (sp,kn), "CONSTANT" ->
 			 let typ = Typeops.type_of_constant (Global.env()) (constant_of_kn kn) in
-			   add_search2 (Nametab.locate (qualid_of_sp sp)) typ
+			   add_search2 (Nametab.locate (qualid_of_path sp)) typ
 		     | (sp,kn), "MUTUALINDUCTIVE" ->
-			 add_search2 (Nametab.locate (qualid_of_sp sp))
+			 add_search2 (Nametab.locate (qualid_of_path sp))
 			   (Pretyping.Default.understand Evd.empty (Global.env())
 			      (RRef(dummy_loc, IndRef(kn,0))))
 		     | _ -> failwith ("unexpected value 1 for "^ 
@@ -764,12 +764,12 @@ let full_name_of_ref r =
      | ConstRef _ -> str "CST"
      | IndRef _ -> str "IND"
      | ConstructRef _ -> str "CSR")
-  ++ str " " ++ (pr_sp (Nametab.sp_of_global r))
+  ++ str " " ++ (pr_path (Nametab.path_of_global r))
     (* LEM TODO: Cleanly separate path from id (see Libnames.string_of_path) *)
 
 let string_of_ref =
   (*LEM TODO: Will I need the Var/Const/Ind/Construct info?*)
-  Depends.o Libnames.string_of_path Nametab.sp_of_global
+  Depends.o Libnames.string_of_path Nametab.path_of_global
 
 let print_depends compute_depends ptree =
   output_results (List.fold_left (fun x y -> x ++ (full_name_of_ref y) ++ fnl())
diff --git a/plugins/interface/coqparser.ml b/plugins/interface/coqparser.ml
index a63e18d27..df5e66b50 100644
--- a/plugins/interface/coqparser.ml
+++ b/plugins/interface/coqparser.ml
@@ -335,7 +335,7 @@ let print_version_action () =
 let load_syntax_action reqid module_name =
  msg (str "loading " ++ str module_name ++ str "... ");
  try
-      (let qid = Libnames.make_short_qualid (Names.id_of_string module_name) in
+      (let qid = Libnames.qualid_of_ident (Names.id_of_string module_name) in
       require_library [dummy_loc,qid] None;
       msg (str "opening... ");
       Declaremods.import_module false (Nametab.locate_module qid); 
diff --git a/plugins/interface/name_to_ast.ml b/plugins/interface/name_to_ast.ml
index 668a581e1..f5e8be31e 100644
--- a/plugins/interface/name_to_ast.ml
+++ b/plugins/interface/name_to_ast.ml
@@ -106,7 +106,7 @@ let convert_one_inductive sp tyi =
   let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in
   let env = Global.env () in
   let envpar = push_rel_context params env in
-  let sp = sp_of_global (IndRef (sp, tyi)) in
+  let sp = path_of_global (IndRef (sp, tyi)) in
   (((false,(dummy_loc,basename sp)),
    convert_env(List.rev params),
    Some (extern_constr true envpar arity), Vernacexpr.Inductive_kw ,
@@ -192,18 +192,6 @@ let leaf_entry_to_ast_list ((sp,kn),lobj) =
 let name_to_ast ref =
   let (loc,qid) = qualid_of_reference ref in
   let l = 
-    try
-      let sp = Nametab.locate_obj qid in
-      let (sp,lobj) = 
-      	let (sp,entry) =
-          List.find (fun en -> (fst (fst en)) = sp) (Lib.contents_after None)
-      	in
-	  match entry with
-            | Lib.Leaf obj -> (sp,obj)
-            | _ -> raise Not_found
-      in
-    	leaf_entry_to_ast_list (sp,lobj)
-    with Not_found -> 
       try 
     	match Nametab.locate qid with
 	  | ConstRef sp -> constant_to_ast_list sp
@@ -220,7 +208,7 @@ let name_to_ast ref =
 		   | Some c1 -> make_definition_ast name c1 typ [])
 	  with Not_found ->
 	    try
-	      let _sp = Nametab.locate_syntactic_definition qid in
+	      let _sp = Nametab.locate_syndef qid in
 		errorlabstrm "print"
       		  (str "printing of syntax definitions not implemented")
 	    with Not_found ->
diff --git a/plugins/interface/name_to_ast.mli b/plugins/interface/name_to_ast.mli
index f9e83b5e1..a532604f5 100644
--- a/plugins/interface/name_to_ast.mli
+++ b/plugins/interface/name_to_ast.mli
@@ -2,4 +2,4 @@ val name_to_ast : Libnames.reference -> Vernacexpr.vernac_expr;;
 val inductive_to_ast_list : Names.mutual_inductive -> Vernacexpr.vernac_expr list;;
 val constant_to_ast_list : Names.constant -> Vernacexpr.vernac_expr list;;
 val variable_to_ast_list : Names.variable -> Vernacexpr.vernac_expr list;;
-val leaf_entry_to_ast_list : (Libnames.section_path * Names.mutual_inductive) * Libobject.obj -> Vernacexpr.vernac_expr list;;
+val leaf_entry_to_ast_list : (Libnames.full_path * Names.mutual_inductive) * Libobject.obj -> Vernacexpr.vernac_expr list;;
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 8c8640ea5..075188f54 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -398,11 +398,11 @@ let destructurate_prop t =
     | _, [_;_] when c = Lazy.force coq_ge -> Kapp (Ge,args)
     | _, [_;_] when c = Lazy.force coq_gt -> Kapp (Gt,args)
     | Const sp, args ->
-	Kapp (Other (string_of_id (id_of_global (ConstRef sp))),args)
+	Kapp (Other (string_of_id (basename_of_global (ConstRef sp))),args)
     | Construct csp , args ->
-	Kapp (Other (string_of_id (id_of_global (ConstructRef csp))), args)
+	Kapp (Other (string_of_id (basename_of_global (ConstructRef csp))), args)
     | Ind isp, args ->
-	Kapp (Other (string_of_id (id_of_global (IndRef isp))),args)
+	Kapp (Other (string_of_id (basename_of_global (IndRef isp))),args)
     | Var id,[] -> Kvar id
     | Prod (Anonymous,typ,body), [] -> Kimp(typ,body)
     | Prod (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal"
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index 6dcc1e872..a07ec4757 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -274,7 +274,7 @@ let (theory_to_obj, obj_to_theory) =
 		    open_function = (fun i o -> if i=1 then cache_th o);
                     cache_function = cache_th;
 		    subst_function = subst_th;
-		    classify_function = (fun (_,x) -> Substitute x);
+		    classify_function = (fun x -> Substitute x);
 		    export_function = export_th }
 
 (* from the set A, guess the associated theory *)
@@ -733,7 +733,7 @@ let build_setspolynom gl th lc =
 
 module SectionPathSet =
   Set.Make(struct
-	     type t = section_path
+	     type t = full_path
 	     let compare = Pervasives.compare
 	   end)
 
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index bdec6bf45..1caa5db1c 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -20,15 +20,15 @@ let destructurate t =
   match Term.kind_of_term c, args with
     | Term.Const sp, args ->
 	Kapp (Names.string_of_id
-		(Nametab.id_of_global (Libnames.ConstRef sp)),
+		(Nametab.basename_of_global (Libnames.ConstRef sp)),
 	      args)
     | Term.Construct csp , args ->
 	Kapp (Names.string_of_id
-		(Nametab.id_of_global (Libnames.ConstructRef csp)),
+		(Nametab.basename_of_global (Libnames.ConstructRef csp)),
 	      args)
     | Term.Ind isp, args ->
 	Kapp (Names.string_of_id
-		(Nametab.id_of_global (Libnames.IndRef isp)),
+		(Nametab.basename_of_global (Libnames.IndRef isp)),
 	      args)
     | Term.Var id,[] -> Kvar(Names.string_of_id id)
     | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
@@ -46,7 +46,7 @@ let dest_const_apply t =
     | Term.Construct csp -> Libnames.ConstructRef csp
     | Term.Ind isp       -> Libnames.IndRef isp
     | _ -> raise Destruct
-  in  Nametab.id_of_global ref, args
+  in  Nametab.basename_of_global ref, args
 
 let logic_dir = ["Coq";"Logic";"Decidable"]
 
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 32f36ef85..24cb84ed5 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -352,18 +352,11 @@ let from_name = ref Spmap.empty
 
 let ring_for_carrier r = Cmap.find r !from_carrier
 let ring_for_relation rel = Cmap.find rel !from_relation
-let ring_lookup_by_name ref =
-  Spmap.find (Nametab.locate_obj (snd(qualid_of_reference ref))) !from_name
 
 
-let find_ring_structure env sigma l oname =
-  match oname, l with
-      Some rf, _ ->
-        (try ring_lookup_by_name rf
-        with Not_found ->
-          errorlabstrm "ring"
-            (str "found no ring named "++pr_reference rf))
-    | None, t::cl' ->
+let find_ring_structure env sigma l =
+  match l with
+    | t::cl' ->
         let ty = Retyping.get_type_of env sigma t in
         let check c =
           let ty' = Retyping.get_type_of env sigma c in
@@ -377,7 +370,7 @@ let find_ring_structure env sigma l oname =
           errorlabstrm "ring"
             (str"cannot find a declared ring structure over"++
              spc()++str"\""++pr_constr ty++str"\""))
-    | None, [] -> assert false
+    | [] -> assert false
 (*
         let (req,_,_) = dest_rel cl in
         (try ring_for_relation req
@@ -457,7 +450,7 @@ let (theory_to_obj, obj_to_theory) =
       open_function = (fun i o -> if i=1 then cache_th o);
       cache_function = cache_th;
       subst_function = subst_th;
-      classify_function = (fun (_,x) -> Substitute x);
+      classify_function = (fun x -> Substitute x);
       export_function = export_th }
 
 
@@ -835,7 +828,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl =
   let env = pf_env gl in
   let sigma = project gl in
   let rl = make_args_list rl t in
-  let e = find_ring_structure env sigma rl None in
+  let e = find_ring_structure env sigma rl in
   let rl = carg (make_term_list e.ring_carrier rl) in
   let lH = carg (make_hyp_list env lH) in
   let ring = ltac_ring_structure e in
@@ -941,20 +934,11 @@ let field_from_name = ref Spmap.empty
 
 let field_for_carrier r = Cmap.find r !field_from_carrier
 let field_for_relation rel = Cmap.find rel !field_from_relation
-let field_lookup_by_name ref =
-  Spmap.find (Nametab.locate_obj (snd(qualid_of_reference ref)))
-    !field_from_name
-
 
-let find_field_structure env sigma l oname =
+let find_field_structure env sigma l =
   check_required_library (cdir@["Field_tac"]);
-  match oname, l with
-      Some rf, _ ->
-        (try field_lookup_by_name rf
-        with Not_found ->
-          errorlabstrm "field"
-            (str "found no field named "++pr_reference rf))
-    | None, t::cl' ->
+  match l with
+    | t::cl' ->
         let ty = Retyping.get_type_of env sigma t in
         let check c =
           let ty' = Retyping.get_type_of env sigma c in
@@ -968,7 +952,7 @@ let find_field_structure env sigma l oname =
           errorlabstrm "field"
             (str"cannot find a declared field structure over"++
              spc()++str"\""++pr_constr ty++str"\""))
-    | None, [] -> assert false
+    | [] -> assert false
 (*        let (req,_,_) = dest_rel cl in
         (try field_for_relation req
         with Not_found ->
@@ -1046,7 +1030,7 @@ let (ftheory_to_obj, obj_to_ftheory) =
       open_function = (fun i o -> if i=1 then cache_th o);
       cache_function = cache_th;
       subst_function = subst_th;
-      classify_function = (fun (_,x) -> Substitute x);
+      classify_function = (fun x -> Substitute x);
       export_function = export_th }
 
 let field_equality r inv req =
@@ -1175,7 +1159,7 @@ let field_lookup (f:glob_tactic_expr) lH rl t gl =
   let env = pf_env gl in
   let sigma = project gl in
   let rl = make_args_list rl t in
-  let e = find_field_structure env sigma rl None in
+  let e = find_field_structure env sigma rl in
   let rl = carg (make_term_list e.field_carrier rl) in
   let lH = carg (make_hyp_list env lH) in
   let field = ltac_field_structure e in
diff --git a/plugins/subtac/equations.ml4 b/plugins/subtac/equations.ml4
index 5b76c9587..5ae15e00a 100644
--- a/plugins/subtac/equations.ml4
+++ b/plugins/subtac/equations.ml4
@@ -10,7 +10,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 (*i camlp4use: "pa_extend.cmo" i*) 
 
-(* $Id: subtac_cases.ml 11198 2008-07-01 17:03:43Z msozeau $ *)
+(* $Id$ *)
 
 open Cases
 open Util
@@ -824,13 +824,13 @@ open Decl_kinds
 type equation = constr_expr * (constr_expr, identifier located) rhs
 
 let locate_reference qid =
-  match Nametab.extended_locate qid with
+  match Nametab.locate_extended qid with
     | TrueGlobal ref -> true
-    | SyntacticDef kn -> true
+    | SynDef kn -> true
 
 let is_global id =
   try 
-    locate_reference (make_short_qualid id)
+    locate_reference (qualid_of_ident id)
   with Not_found -> 
     false
 
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index 13e5e6d5f..1ac022159 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -15,7 +15,7 @@
 (* Utility Functions *)
 
 exception TwoModulesWhoseDirPathIsOneAPrefixOfTheOther;;
-let get_module_path_of_section_path path =
+let get_module_path_of_full_path path =
  let dirpath = fst (Libnames.repr_path path) in
  let modules = Lib.library_dp () :: (Library.loaded_libraries ()) in
   match
@@ -177,7 +177,7 @@ let uri_of_kernel_name tag =
 
 let uri_of_declaration id tag =
  let module LN = Libnames in
- let dir = LN.extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()) in
+ let dir = LN.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ()) in
  let tokens = token_list_of_path dir id tag in
   "cic:/" ^ String.concat "/" tokens
 
@@ -468,14 +468,14 @@ print_endline "PASSATO" ; flush stdout ;
                 match g with
                    Libnames.ConstructRef ((induri,_),_)
                  | Libnames.IndRef (induri,_) ->
-                    Nametab.sp_of_global (Libnames.IndRef (induri,0))
+                    Nametab.path_of_global (Libnames.IndRef (induri,0))
                  | Libnames.VarRef id ->
                     (* Invariant: variables are never cooked in Coq *)
                     raise Not_found
-                 | _ -> Nametab.sp_of_global g
+                 | _ -> Nametab.path_of_global g
                in
                Dischargedhypsmap.get_discharged_hyps sp,
-               get_module_path_of_section_path sp
+               get_module_path_of_full_path sp
              with Not_found ->
                 (* no explicit substitution *)
                 [], Libnames.dirpath_of_string "dummy"
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 1ae186614..4a27c3247 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -102,7 +102,7 @@ let filter_params pvars hyps =
  in
   let cwd = Lib.cwd () in
   let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in
-  let modulepath = Cic2acic.get_module_path_of_section_path cwdsp in
+  let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in
    aux (Names.repr_dirpath modulepath) (List.rev pvars)
 ;;
 
@@ -118,7 +118,7 @@ let search_variables () =
  let module N = Names in
   let cwd = Lib.cwd () in
   let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in
-  let modulepath = Cic2acic.get_module_path_of_section_path cwdsp in
+  let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in
    let rec aux =
     function
        [] -> []
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 911ded641..901341e7b 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -384,7 +384,7 @@ let (inCoercion,_) =
     load_function = load_coercion;
     cache_function = cache_coercion;
     subst_function = subst_coercion;
-    classify_function = (fun (_,x) -> Substitute x);
+    classify_function = (fun x -> Substitute x);
     discharge_function = discharge_coercion;
     export_function = (function x -> Some x)  }
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index d43bc0780..2c3de28a5 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -32,7 +32,7 @@ let dl = dummy_loc
 (* Tools for printing of Cases                                              *)
 
 let encode_inductive r =
-  let indsp = inductive_of_reference r in
+  let indsp = global_inductive r in
   let constr_lengths = mis_constr_nargs indsp in
   (indsp,constr_lengths)
 
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index f8dab16cd..6a4c066ce 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -579,14 +579,14 @@ let lookup_eliminator ind_sp s =
   let id = add_suffix ind_id (elimination_suffix s) in
   (* Try first to get an eliminator defined in the same section as the *)
   (* inductive type *)
-  let ref = ConstRef (make_con mp dp (label_of_id id)) in
-  try 
-    let _ = sp_of_global ref in
-    constr_of_global ref
+  try
+    let cst = make_con mp dp (label_of_id id) in
+    let _ = Global.lookup_constant cst in
+    mkConst cst
   with Not_found ->
   (* Then try to get a user-defined eliminator in some other places *)
   (* using short name (e.g. for "eq_rec") *)
-  try constr_of_global (Nametab.locate (make_short_qualid id))
+  try constr_of_global (Nametab.locate (qualid_of_ident id))
   with Not_found ->
     errorlabstrm "default_elim"
       (strbrk "Cannot find the elimination combinator " ++
@@ -594,25 +594,3 @@ let lookup_eliminator ind_sp s =
        pr_global_env Idset.empty (IndRef ind_sp) ++ 
        strbrk " on sort " ++ pr_sort_family s ++
        strbrk " is probably not allowed.")
-
-
-(*  let env = Global.env() in
-  let path = sp_of_global None (IndRef ind_sp) in
-  let dir, base = repr_path path 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 (Names.make_path dir id)
-  with Not_found ->
-  (* Then try to get a user-defined eliminator in some other places *)
-  (* using short name (e.g. for "eq_rec") *)
-    try constr_of_global (Nametab.locate (make_short_qualid id))
-    with Not_found ->
-      errorlabstrm "default_elim"
-	(str "Cannot find the elimination combinator " ++
-           pr_id id ++ spc () ++
-	   str "The elimination of the inductive definition " ++
-           pr_id base ++ spc () ++ str "on sort " ++ 
-           spc () ++ pr_sort_family s ++
-	   str " is probably not allowed")
-*)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 8bf95ecbf..c82589b9a 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -77,7 +77,7 @@ let (inStruc,outStruc) =
     cache_function = cache_structure;
     load_function = load_structure;
     subst_function = subst_structure;
-    classify_function = (fun (_,x) -> Substitute x);
+    classify_function = (fun x -> Substitute x);
     discharge_function = discharge_structure;
     export_function = (function x -> Some x) }
 
@@ -141,7 +141,7 @@ let (in_method,out_method) =
 	cache_function = load_method;
 	subst_function = (fun (_,s,(ty,id)) -> Mod_subst.subst_mps s ty,subst_id s id);
 	export_function = (fun x -> Some x);
-	classify_function = (fun (_,x) -> Substitute x) 
+	classify_function = (fun x -> Substitute x) 
     }
 
 let methods_matching c = MethodsDnet.search_pattern !meth_dnet c
@@ -271,7 +271,7 @@ let (inCanonStruc,outCanonStruct) =
     open_function = open_canonical_structure;
     cache_function = cache_canonical_structure;
     subst_function = subst_canonical_structure;
-    classify_function = (fun (_,x) -> Substitute x);
+    classify_function = (fun x -> Substitute x);
     discharge_function = discharge_canonical_structure;
     export_function = (function x -> Some x) }
 
@@ -281,7 +281,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
 
 let error_not_structure ref =
   errorlabstrm "object_declare"
-    (Nameops.pr_id (id_of_global ref) ++ str" is not a structure object.")
+    (Nameops.pr_id (basename_of_global ref) ++ str" is not a structure object.")
 
 let check_and_decompose_canonical_structure ref =
   let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index b7013a703..024f190f2 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -807,7 +807,7 @@ let unfold env sigma name =
   else
     error (string_of_evaluable_ref env name^" is opaque.")
 
-(* [unfoldoccs : (readable_constraints -> (int list * section_path) -> constr -> constr)]
+(* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)]
  * Unfolds the constant name in a term c following a list of occurrences occl.
  * at the occurrences of occ_list. If occ_list is empty, unfold all occurences.
  * Performs a betaiota reduction after unfolding. *)
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index b7a4fc925..4034d8667 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -34,7 +34,7 @@ let pr_name = function
   | Name id -> pr_id id
   | Anonymous -> str "_"
 
-let pr_sp sp = str(string_of_kn sp)
+let pr_path sp = str(string_of_kn sp)
 let pr_con sp = str(string_of_con sp)
 
 let rec pr_constr c = match kind_of_term c with
@@ -65,9 +65,9 @@ let rec pr_constr c = match kind_of_term c with
       (str"Evar#" ++ int e ++ str"{" ++
        prlist_with_sep spc pr_constr (Array.to_list l) ++str"}")
   | Const c -> str"Cst(" ++ pr_con c ++ str")"
-  | Ind (sp,i) -> str"Ind(" ++ pr_sp sp ++ str"," ++ int i ++ str")"
+  | Ind (sp,i) -> str"Ind(" ++ pr_path sp ++ str"," ++ int i ++ str")"
   | Construct ((sp,i),j) ->
-      str"Constr(" ++ pr_sp sp ++ str"," ++ int i ++ str"," ++ int j ++ str")"
+      str"Constr(" ++ pr_path sp ++ str"," ++ int i ++ str"," ++ int j ++ str")"
   | Case (ci,p,c,bl) -> v 0
       (hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++
              pr_constr c ++ str"of") ++ cut() ++
@@ -711,7 +711,7 @@ let add_vname vars = function
     Name id -> Idset.add id vars
   | _ -> vars
 
-let id_of_global = Nametab.id_of_global
+let basename_of_global = Nametab.basename_of_global
 
 let sort_hdchar = function
   | Prop(_) -> "P"
@@ -731,9 +731,9 @@ let hdchar env c =
 	if i=0 then 
 	  lowercase_first_char (id_of_label (label kn))
 	else 
-	  lowercase_first_char (id_of_global (IndRef x))
+	  lowercase_first_char (basename_of_global (IndRef x))
     | Construct ((sp,i) as x) ->
-	lowercase_first_char (id_of_global (ConstructRef x))
+	lowercase_first_char (basename_of_global (ConstructRef x))
     | Var id  -> lowercase_first_char id
     | Sort s -> sort_hdchar s
     | Rel n ->
@@ -839,14 +839,14 @@ let is_imported_ref = function
 
 let is_global id =
   try 
-    let ref = locate (make_short_qualid id) in
+    let ref = locate (qualid_of_ident id) in
     not (is_imported_ref ref)
   with Not_found -> 
     false
 
 let is_constructor id =
   try 
-    match locate (make_short_qualid id) with 
+    match locate (qualid_of_ident id) with 
       | ConstructRef _ as ref -> not (is_imported_ref ref)
       | _ -> false
   with Not_found -> 
@@ -907,12 +907,12 @@ let occur_rel p env id =
 let occur_id nenv id0 c =
   let rec occur n c = match kind_of_term c with
     | Var id when  id=id0 -> raise Occur
-    | Const kn when id_of_global (ConstRef kn) = id0 -> raise Occur
+    | Const kn when basename_of_global (ConstRef kn) = id0 -> raise Occur
     | Ind ind_sp
-	when id_of_global (IndRef ind_sp) = id0 ->
+	when basename_of_global (IndRef ind_sp) = id0 ->
         raise Occur
     | Construct cstr_sp
-	when id_of_global (ConstructRef cstr_sp) = id0 ->
+	when basename_of_global (ConstructRef cstr_sp) = id0 ->
         raise Occur
     | Rel p when p>n & occur_rel (p-n) nenv id0 -> raise Occur
     | _ -> iter_constr_with_binders succ occur n c
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 2f2796f1c..52e2eb24e 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -168,7 +168,7 @@ let (class_input,class_output) =
       cache_function = cache_class;
       load_function = (fun _ -> load_class);
       open_function = (fun _ -> load_class);
-      classify_function = (fun (_,x) -> Substitute x);
+      classify_function = (fun x -> Substitute x);
       discharge_function = (fun a -> Some (discharge_class a));
       rebuild_function = rebuild_class;
       subst_function = subst_class;
@@ -212,7 +212,7 @@ let (instance_input,instance_output) =
       cache_function = cache_instance;
       load_function = (fun _ -> load_instance);
       open_function = (fun _ -> load_instance);
-      classify_function = (fun (_,x) -> Substitute x);
+      classify_function = (fun x -> Substitute x);
       discharge_function = (fun a -> Some (discharge_instance a));
       rebuild_function = rebuild_instance;
       subst_function = subst_instance;
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index c7d6ffe14..2e10a9f4a 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -77,7 +77,7 @@ let export_strategy (local,obj) =
       EvalVarRef _ -> None
     | EvalConstRef _ as q -> Some q) obj
 
-let classify_strategy (_,(local,_ as obj)) = 
+let classify_strategy (local,_ as obj) = 
   if local then Dispose else Substitute obj
 
 let disch_ref ref =
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 741753521..b998daa74 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -446,7 +446,7 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) =
 	  if hintlist' == hintlist then obj else
 	    (local,name,AddTactic hintlist')
 	      
-let classify_autohint (_,((local,name,hintlist) as obj)) =
+let classify_autohint ((local,name,hintlist) as obj) =
   if local or hintlist = (AddTactic []) then Dispose else Substitute obj
 
 let export_autohint ((local,name,hintlist) as obj) =
@@ -548,7 +548,7 @@ let interp_hints h =
       HintsTransparencyEntry (List.map fr lhints, b)
   | HintsConstructors lqid ->
       let constr_hints_of_ind qid =
-        let isp = inductive_of_reference qid in
+        let isp = global_inductive qid in
         let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in
         list_tabulate (fun i -> None, true, mkConstruct (isp,i+1))
 	  (Array.length consnames) in
@@ -1121,7 +1121,7 @@ let superauto n to_add argl  =
 
 let interp_to_add gl r =
   let r = Syntax_def.locate_global_with_alias (qualid_of_reference r) in
-  let id = id_of_global r in
+  let id = basename_of_global r in
   (next_ident_away id (pf_ids_of_hyps gl), constr_of_global r)
 
 let gen_superauto nopt l a b gl =
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 04c4ed161..63481abde 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -224,7 +224,7 @@ let subst_hintrewrite (_,subst,(rbase,list as node)) =
     if list' == list then node else
       (rbase,list')
       
-let classify_hintrewrite (_,x) = Libobject.Substitute x
+let classify_hintrewrite x = Libobject.Substitute x
 
 
 (* Declaration of the Hint Rewrite library object *)
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 3d34a2d68..be4343b4f 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -206,7 +206,7 @@ let cache_dd (_,(_,na,dd)) =
       (str"The code which adds destructor hints broke;" ++ spc () ++ 
 	 str"this is not supposed to happen")
 
-let classify_dd (_,(local,_,_ as o)) =
+let classify_dd (local,_,_ as o) =
   if local then Dispose else Substitute o
 
 let export_dd (local,_,_ as x) = if local then None else Some x
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index f1c255154..c6c9bdd10 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -408,7 +408,7 @@ let (inTransitivity,_) =
     cache_function = cache_transitivity_lemma;
     open_function = (fun i o -> if i=1 then cache_transitivity_lemma o);
     subst_function = subst_transitivity_lemma;
-    classify_function = (fun (_,o) -> Substitute o);       
+    classify_function = (fun o -> Substitute o);       
     export_function = (fun x -> Some x) }
 
 (* Synchronisation with reset *)
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 43ae99203..385e86587 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -67,7 +67,7 @@ let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
 
 let try_find_global_reference dir s =
   let sp = Libnames.make_path (make_dir ("Coq"::dir)) (id_of_string s) in
-    Nametab.absolute_reference sp
+    Nametab.global_of_path sp
       
 let try_find_reference dir s =
   constr_of_global (try_find_global_reference dir s)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 32c69ddcd..e79174c66 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -374,7 +374,7 @@ let loc_of_by_notation f = function
 let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
 
 let intern_inductive_or_by_notation = function
-  | AN r -> Nametab.inductive_of_reference r
+  | AN r -> Nametab.global_inductive r
   | ByNotation (loc,ntn,sc) ->
       destIndRef (Notation.interp_notation_as_global_reference loc
         (function IndRef ind -> true | _ -> false) ntn sc)
@@ -2847,7 +2847,7 @@ let (inMD,outMD) =
      load_function   = load_md;
      open_function   = open_md;
      subst_function = subst_md;
-     classify_function = (fun (_,o) -> Substitute o);       
+     classify_function = (fun o -> Substitute o);       
      export_function = (fun x -> Some x)}
 
 let print_ltac id =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ca64a8d3d..663c426f9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2054,7 +2054,7 @@ let make_up_names n ind_opt cname =
     if is_hyp then 
       match ind_opt with
 	| None -> id_of_string ind_prefix
-	| Some ind_id -> add_prefix ind_prefix (Nametab.id_of_global ind_id)
+	| Some ind_id -> add_prefix ind_prefix (Nametab.basename_of_global ind_id)
     else add_prefix ind_prefix cname in
   let hyprecname = make_base n base_ind in
   let avoid =
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index bbc1285e2..ad2fd9009 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -277,7 +277,7 @@ let tauto_classical nnpp g =
 
 let tauto g =
   try 
-    let nnpp = constr_of_global (Nametab.absolute_reference coq_nnpp_path) in
+    let nnpp = constr_of_global (Nametab.global_of_path coq_nnpp_path) in
     (* try intuitionistic version first to avoid an axiom if possible *)
     tclORELSE tauto_intuitionistic (tauto_classical nnpp) g
   with Not_found ->
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 919aacbbe..8a39c383a 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -331,12 +331,12 @@ let rec special = function
   | _ :: r -> special r
       
 let custom sps =
-  let pr_sp (file,dependencies,com) =
+  let pr_path (file,dependencies,com) =
     print file; print ": "; print dependencies; print "\n";
     print "\t"; print com; print "\n\n"
   in
     if sps <> [] then section "Custom targets.";
-    List.iter pr_sp sps
+    List.iter pr_path sps
 
 let subdirs sds =
   let pr_subdir s =
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 29bef7b5a..4946ee933 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -161,7 +161,7 @@ let new_inst_no =
   fun () -> incr cnt; string_of_int !cnt
 
 let make_instance_ident gr =
-  Nameops.add_suffix (Nametab.id_of_global gr) ("_autoinstance_"^new_inst_no())
+  Nameops.add_suffix (Nametab.basename_of_global gr) ("_autoinstance_"^new_inst_no())
 
 let new_instance_message ident typ def =
   Flags.if_verbose
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 48a5119d1..82fd9bc1a 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -612,7 +612,7 @@ let eq_local_binders bl1 bl2 =
   List.length bl1 = List.length bl2 && List.for_all2 eq_local_binder bl1 bl2
 
 let extract_coercions indl =
-  let mkqid (_,((_,id),_)) = make_short_qualid id in
+  let mkqid (_,((_,id),_)) = qualid_of_ident id in
   let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in
   List.map mkqid (List.flatten(List.map (fun (_,_,_,lc) -> extract lc) indl))
 
@@ -930,7 +930,7 @@ requested
        let l1,l2 = split_scheme q in
     ( match t with
       | InductionScheme (x,y,z) ->
-             let ind = mkInd (Nametab.inductive_of_reference y) in
+             let ind = mkInd (Nametab.global_inductive y) in
              let sort_of_ind = family_of_sort (Typing.sort_of env Evd.empty ind)
 in
              let z' = family_of_sort (interp_sort z) in
@@ -969,7 +969,7 @@ let build_induction_scheme lnamedepindsort =
   let lrecspec =
     List.map
       (fun (_,dep,indid,sort) ->
-        let ind = Nametab.inductive_of_reference indid in
+        let ind = Nametab.global_inductive indid in
         let (mib,mip) = Global.lookup_inductive ind in
          (ind,mib,mip,dep,interp_elimination_sort sort)) 
       lnamedepindsort
@@ -998,7 +998,7 @@ tried to declare different schemes at once *)
     else (
       if ischeme <> [] then build_induction_scheme ischeme;
       List.iter ( fun indname -> 
-        let ind = Nametab.inductive_of_reference indname
+        let ind = Nametab.global_inductive indname
         in declare_eq_scheme (fst ind);
         try
            make_eq_decidability ind 
diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml
index 6fd49b15b..4e10d1d52 100644
--- a/toplevel/libtypes.ml
+++ b/toplevel/libtypes.ml
@@ -74,7 +74,7 @@ let (input,output) =
 	load_function = (fun _ -> load);
 	subst_function = (fun (_,s,t) -> subst s t);
 	export_function = (fun x -> Some x);
-	classify_function = (fun (_,x) -> Substitute x) 
+	classify_function = (fun x -> Substitute x) 
     }
 
 let update () = Lib.add_anonymous_leaf (input !defined_types)
@@ -102,7 +102,7 @@ let add a b = Profile.profile1 add_key add a b
 
 let _ = Declare.add_cache_hook 
   ( fun sp ->
-      let gr = Nametab.absolute_reference sp in
+      let gr = Nametab.global_of_path sp in
       let ty = Global.type_of_global gr in
       add ty gr )
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index d08558426..e6c469974 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -35,7 +35,7 @@ let (inToken, outToken) =
        open_function = (fun i o -> if i=1 then cache_token o);
        cache_function = cache_token;
        subst_function = Libobject.ident_subst_function;
-       classify_function = (fun (_,o) -> Substitute o);
+       classify_function = (fun o -> Substitute o);
        export_function = (fun x -> Some x)}
 
 let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
@@ -74,7 +74,7 @@ let (inTacticGrammar, outTacticGrammar) =
        open_function = (fun i o -> if i=1 then cache_tactic_notation o);
        cache_function = cache_tactic_notation;
        subst_function = subst_tactic_notation;
-       classify_function = (fun (_,o) -> Substitute o);
+       classify_function = (fun o -> Substitute o);
        export_function = (fun x -> Some x)}
 
 let cons_production_parameter l = function
@@ -681,7 +681,7 @@ let subst_syntax_extension (_,subst,(local,sy)) =
   (local, List.map (fun (prec,ntn,gr,pp) ->
      (prec,ntn, subst_parsing_rule subst gr, subst_printing_rule subst pp)) sy)
 
-let classify_syntax_definition (_,(local,_ as o)) =
+let classify_syntax_definition (local,_ as o) =
   if local then Dispose else Substitute o
 
 let export_syntax_definition (local,_ as o) =
@@ -873,7 +873,7 @@ let cache_notation o =
 let subst_notation (_,subst,(lc,scope,pat,b,ndf)) =
   (lc,scope,subst_interpretation subst pat,b,ndf)
 
-let classify_notation (_,(local,_,_,_,_ as o)) =
+let classify_notation (local,_,_,_,_ as o) =
   if local then Dispose else Substitute o
 
 let export_notation (local,_,_,_,_ as o) =
@@ -1058,7 +1058,7 @@ let (inScopeCommand,outScopeCommand) =
       open_function = open_scope_command;
       load_function = load_scope_command;
       subst_function = subst_scope_command;
-      classify_function = (fun (_,obj) -> Substitute obj);
+      classify_function = (fun obj -> Substitute obj);
       export_function = (fun x -> Some x) }
 
 let add_delimiters scope key =
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 334b4d82a..837d50207 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -309,7 +309,7 @@ let (inMLModule,outMLModule) =
                     cache_function = cache_ml_module_object;
                     export_function = export_ml_module_object;
                     subst_function = (fun (_,_,o) -> o);
-                    classify_function = (fun (_,o) -> Substitute o) }
+                    classify_function = (fun o -> Substitute o) }
 
 let declare_ml_modules l =
   Lib.add_anonymous_leaf (inMLModule {mnames=l})
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 481d91787..66dc28e2d 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -47,7 +47,7 @@ let rec head_const c = match kind_of_term c with
 
 let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
   let env = Global.env () in
-  let crible_rec (sp,_) lobj = match object_tag lobj with
+  let crible_rec (sp,kn) lobj = match object_tag lobj with
     | "VARIABLE" ->
 	(try 
 	   let (id,_,typ) = Global.lookup_named (basename sp) in 
@@ -57,14 +57,13 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
 	     fn (VarRef id) env typ
 	 with Not_found -> (* we are in a section *) ())
     | "CONSTANT" ->
-	let cst = locate_constant (qualid_of_sp sp) in
+	let cst = constant_of_kn kn in
 	let typ = Typeops.type_of_constant env cst in
         if refopt = None
 	  || head_const typ = constr_of_global (Option.get refopt)
 	then
 	  fn (ConstRef cst) env typ
     | "INDUCTIVE" -> 
-	let kn = locate_mind (qualid_of_sp sp) in
         let mib = Global.lookup_mind kn in 
         (match refopt with 
 	  | Some (IndRef ((kn',tyi) as ind)) when kn=kn' ->
@@ -86,7 +85,7 @@ let crible ref = gen_crible (Some ref)
 
 (* Fine Search. By Yves Bertot. *)
 
-exception No_section_path
+exception No_full_path
 
 let rec head c = 
   let c = strip_outer_cast c in
@@ -95,9 +94,9 @@ let rec head c =
   | LetIn (_,_,_,c) -> head c
   | _              -> c
       
-let constr_to_section_path c = match kind_of_term c with
+let constr_to_full_path c = match kind_of_term c with
   | Const sp -> sp
-  | _ -> raise No_section_path
+  | _ -> raise No_full_path
       
 let xor a b = (a or b) & (not (a & b))
 
@@ -109,14 +108,14 @@ let plain_display ref a c =
 let filter_by_module (module_list:dir_path list) (accept:bool) 
   (ref:global_reference) _ _ =
   try
-    let sp = sp_of_global ref in
+    let sp = path_of_global ref in
     let sl = dirpath sp in
     let rec filter_aux = function
       | m :: tl -> (not (is_dirpath_prefix_of m sl)) && (filter_aux tl)
       | [] -> true 
     in
     xor accept (filter_aux module_list)
-  with No_section_path -> 
+  with No_full_path -> 
     false
 
 let ref_eq = Libnames.encode_kn Coqlib.logic_module (id_of_string "eq"), 0
@@ -209,7 +208,7 @@ let gen_filtered_search filter_function display_function =
 
 (** SearchAbout *)
 
-let name_of_reference ref = string_of_id (id_of_global ref)
+let name_of_reference ref = string_of_id (basename_of_global ref)
 
 type glob_search_about_item =
   | GlobSearchSubPattern of constr_pattern
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fa56e60f6..1de9d739a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -506,12 +506,11 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
          Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)])
            export
 
-let vernac_end_module export (loc,id) =
-  let mp = Declaremods.end_module id in
-    Dumpglob.dump_modref loc mp "mod";
-    if_verbose message ("Module "^ string_of_id id ^" is defined") ;
-    Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
-
+let vernac_end_module export (loc,id as lid) =
+  let mp = Declaremods.end_module () in
+  Dumpglob.dump_modref loc mp "mod";
+  if_verbose message ("Module "^ string_of_id id ^" is defined") ;
+  Option.iter (fun export -> vernac_import export [Ident lid]) export
 
 let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
   if Lib.sections_are_opened () then
@@ -549,46 +548,43 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
 	  if_verbose message 
 	    ("Module Type "^ string_of_id id ^" is defined")
 
-
 let vernac_end_modtype (loc,id) =
-  let mp = Declaremods.end_modtype id in
-    Dumpglob.dump_modref loc mp "modtype";
-    if_verbose message 
-      ("Module Type "^ string_of_id id ^" is defined")
-
+  let mp = Declaremods.end_modtype () in
+  Dumpglob.dump_modref loc mp "modtype";
+  if_verbose message ("Module Type "^ string_of_id id ^" is defined")
+	  
 let vernac_include = function
   | CIMTE mty_ast ->
       Declaremods.declare_include Modintern.interp_modtype mty_ast false
   | CIME mexpr_ast ->
       Declaremods.declare_include Modintern.interp_modexpr mexpr_ast true
 	  
-	  
-	  
 (**********************)
 (* Gallina extensions *)
 
-  (* Sections *)
+(* Sections *)
 
 let vernac_begin_section (_, id as lid) =
   check_no_pending_proofs ();
   Dumpglob.dump_definition lid true "sec";
   Lib.open_section id
 
-let vernac_end_section (loc, id) = 
-  
-    Dumpglob.dump_reference loc 
-      (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec";
-  Lib.close_section id
+let vernac_end_section (loc,_) =
+  Dumpglob.dump_reference loc 
+    (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec";
+  Lib.close_section ()
+
+(* Dispatcher of the "End" command *)
 
-let vernac_end_segment lid =
+let vernac_end_segment (_,id as lid) =
   check_no_pending_proofs ();
-  let o = try Lib.what_is_opened () with 
-      Not_found -> error "There is nothing to end." in
-    match o with
-      | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export lid
-      | _,Lib.OpenedModtype _ -> vernac_end_modtype lid
-      | _,Lib.OpenedSection _ -> vernac_end_section lid
-      | _ -> anomaly "No more opened things"
+  match Lib.find_opening_node id with
+  | Lib.OpenedModule (export,_,_) -> vernac_end_module export lid
+  | Lib.OpenedModtype _ -> vernac_end_modtype lid
+  | Lib.OpenedSection _ -> vernac_end_section lid
+  | _ -> anomaly "No more opened things"
+
+(* Libraries *)
 
 let vernac_require import _ qidl =
   let qidl = List.map qualid_of_reference qidl in
@@ -597,6 +593,8 @@ let vernac_require import _ qidl =
     List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl);
   Library.require_library_from_dirpath modrefl import
 
+(* Coercions and canonical structures *)
+
 let vernac_canonical r =
   Recordops.declare_canonical_structure (global_with_alias r)
 
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 63d93a767..b844f03ca 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -131,9 +131,9 @@ let get_discharged_hyp_names sp = List.map basename (get_discharged_hyps sp)
 
 let section_parameters = function
   | RRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_))) ->
-      get_discharged_hyp_names (sp_of_global (IndRef(induri,0)))
+      get_discharged_hyp_names (path_of_global (IndRef(induri,0)))
   | RRef (_,(ConstRef cst as ref)) ->
-      get_discharged_hyp_names (sp_of_global ref)
+      get_discharged_hyp_names (path_of_global ref)
   | _ -> []
 
 let merge vl al =
@@ -217,7 +217,7 @@ END
 VERNAC COMMAND EXTEND Whelp
 | [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ] 
 | [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ] 
-| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (inductive_of_reference_with_alias r) ] 
+| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (global_inductive_with_alias r) ] 
 | [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c]
 END