Abstraction de l'immplementation de dirpath et implementation dans l'autre sens pour plus de partage entre chemins

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

33 files changed, 236 insertions, 189 deletions

diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 60fe808e0..ad7779036 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -143,7 +143,8 @@ let real_subst_in_constr = replace_vars
 (* Coq constants *)
 
 let coq_constant d s =
-  make_path (List.map id_of_string ("Coq" :: d)) (id_of_string s) CCI
+  make_path
+    (make_dirpath (List.map id_of_string ("Coq" :: d))) (id_of_string s) CCI
 
 let bool_sp = coq_constant ["Init"; "Datatypes"] "bool"
 let coq_true = mkMutConstruct ((bool_sp,0),1)
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 68ff965b2..d726d4fa3 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -229,7 +229,7 @@ let _ =
     those having an ML extraction. *)
 
 let extract_module m =
-  let m = Nametab.locate_loaded_library (Nametab.make_qualid [] m) in
+  let m = Nametab.locate_loaded_library (Nametab.make_short_qualid m) in
   let seg = Library.module_segment (Some m) in
   let get_reference = function
     | sp, Leaf o ->
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 1bc47b1e0..81d77741b 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -82,7 +82,7 @@ let rename_upper_global id = rename_global (uppercase_id id)
 
 (*s Modules considerations *)
 
-let module_of_r r = list_last (dirpath (sp_of_r r))
+let module_of_r r = snd (split_dirpath (dirpath (sp_of_r r)))
 
 let string_of_r r = string_of_id (basename (sp_of_r r))
 
diff --git a/contrib/interface/ctast.ml b/contrib/interface/ctast.ml
index 4ed6dbcd9..5b97716fc 100644
--- a/contrib/interface/ctast.ml
+++ b/contrib/interface/ctast.ml
@@ -16,7 +16,10 @@ type t =
 
 let section_path sl k =
   match List.rev sl with
-    | s::pa -> make_path (List.rev (List.map id_of_string pa)) (id_of_string s) (kind_of_string k)
+    | s::pa ->
+	make_path
+	  (make_dirpath (List.rev (List.map id_of_string pa)))
+	  (id_of_string s) (kind_of_string k)
     | [] -> invalid_arg "section_path"
 
 let is_meta s = String.length s > 0 && s.[0] == '$'
@@ -53,7 +56,7 @@ let rec ast_to_ct = function
   | Coqast.Str (loc,a) -> Str (loc,a)
   | Coqast.Path (loc,a) ->
     let (sl,bn,pk) = repr_path a in
-    Path(loc, (List.map string_of_id sl) @ [string_of_id bn],(* Bidon *) "CCI")
+    Path(loc, (List.map string_of_id (repr_dirpath sl)) @ [string_of_id bn],(* Bidon *) "CCI")
   | Coqast.Dynamic (loc,a) -> Dynamic (loc,a)
 
 let loc = function
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 00259ef99..e4523121c 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -84,9 +84,9 @@ let implicit_args_to_ast_list sp mipv =
 	      
 let convert_qualid qid =
   let d, id = Nametab.repr_qualid qid in
-    match d with
+    match repr_dirpath d with
 	[] -> nvar id
-      | _ -> ope("QUALID", List.fold_right (fun s l -> (nvar s)::l) d
+      | d -> ope("QUALID", List.fold_right (fun s l -> (nvar s)::l) d
 		   [nvar id]);;
 
 (* This function converts constructors for an inductive definition to a
@@ -228,7 +228,7 @@ let name_to_ast (qid:Nametab.qualid) =
   	with Not_found -> 
 	  try  (* Var locale de but, pas var de section... donc pas d'implicits *)
 	    let dir,name = Nametab.repr_qualid qid in 
-	      if dir <> [] then raise Not_found;
+	      if dir <> make_dirpath [] then raise Not_found;
 	      let (c,typ) = Global.lookup_named name in 
 		(match c with
 		     None -> make_variable_ast name typ []
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index ff76f2c75..42daf3c19 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -58,7 +58,7 @@ let ctf_FileErrorMessage reqid pps =
   function has no effect on parsing *)
 let try_require_module import specif name fname =
  try Library.require_module (if specif = "UNSPECIFIED" then None
-  else Some (specif = "SPECIFICATION")) (Nametab.make_qualid [] (Names.id_of_string name)) fname (import = "IMPORT")
+  else Some (specif = "SPECIFICATION")) (Nametab.make_short_qualid (Names.id_of_string name)) fname (import = "IMPORT")
  with
  | e -> mSGNL [< 'sTR "Reinterning of "; 'sTR name; 'sTR " failed" >];;
 
@@ -292,24 +292,35 @@ let parse_file_action reqid file_name =
 (* This function is taken from Mltop.add_path *)
 
 let add_path dir coq_dirpath =
-  if coq_dirpath = [] then anomaly "add_path: empty path in library";
+(*
+  if coq_dirpath = Names.make_dirpath [] then
+    anomaly "add_path: empty path in library";
+*)
   if exists_dir dir then
     begin
       Library.add_load_path_entry (dir,coq_dirpath);
-      Nametab.push_library_root (List.hd coq_dirpath)
+      Nametab.push_library_root coq_dirpath
     end
   else
     wARNING [< 'sTR ("Cannot open " ^ dir) >]
 
+let convert_string d =
+  try Names.id_of_string d
+  with _ -> failwith "caught"
+
 let add_rec_path dir coq_dirpath =
-  if coq_dirpath = [] then anomaly "add_path: empty path in library";
+(*
+  if coq_dirpath = Names.make_dirpath [] then anomaly "add_path: empty path in library";
+*)
   let dirs = all_subdirs dir in
+  let prefix = Names.repr_dirpath coq_dirpath in
   if dirs <> [] then
-    let convert = List.map Names.id_of_string in
-    let dirs = List.map (fun (lp,cp) -> (lp,coq_dirpath@(convert cp))) dirs in
+    let convert_dirs (lp,cp) =
+      (lp,Names.make_dirpath (prefix@(List.map convert_string cp))) in
+    let dirs = map_succeed convert_dirs dirs in
     begin
       List.iter Library.add_load_path_entry dirs;
-      Nametab.push_library_root (List.hd coq_dirpath)
+      Nametab.push_library_root coq_dirpath
     end
     else
       wARNING [< 'sTR ("Cannot open " ^ dir) >];;
@@ -318,7 +329,7 @@ let add_path_action reqid string_arg =
   let directory_name = glob string_arg in
   let alias = Filename.basename directory_name in
     begin
-      add_path directory_name [Names.id_of_string alias]
+      add_path directory_name (Names.make_dirpath [Names.id_of_string alias])
     end;;
 
 let print_version_action () =
@@ -328,7 +339,7 @@ let print_version_action () =
 let load_syntax_action reqid module_name =
  mSG [< 'sTR "loading "; 'sTR module_name; 'sTR "... " >];
  try
-      (let qid = Nametab.make_qualid [] (Names.id_of_string module_name) in
+      (let qid = Nametab.make_short_qualid (Names.id_of_string module_name) in
       read_module qid;
       mSG [< 'sTR "opening... ">];
       let fullname = Nametab.locate_loaded_library qid in 
@@ -369,9 +380,9 @@ Libobject.relax true;
        else
 	 (mSGNL [< 'sTR "could not find the value of COQDIR" >]; exit 1) in
      begin
-       add_rec_path (Filename.concat coqdir "theories") [Nametab.coq_root];
-       add_path (Filename.concat coqdir "tactics") [Nametab.coq_root];
-       add_rec_path (Filename.concat coqdir "contrib") [Nametab.coq_root];
+       add_rec_path (Filename.concat coqdir "theories") (Names.make_dirpath [Nametab.coq_root]);
+       add_path (Filename.concat coqdir "tactics") (Names.make_dirpath [Nametab.coq_root]);
+       add_rec_path (Filename.concat coqdir "contrib") (Names.make_dirpath [Nametab.coq_root]);
        List.iter (fun a -> mSGNL [< 'sTR a >]) (get_load_path())
      end;
 (try 
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index cefc9f7e0..4ece713f5 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -176,7 +176,7 @@ let (imply_elim2: pbp_rule) = function
   | _ -> None;;
 
 let reference dir s =
-  let dir = List.map id_of_string ("Coq"::"Init"::[dir]) in
+  let dir = make_dirpath (List.map id_of_string ("Coq"::"Init"::[dir])) in
   let id = id_of_string s in
   try 
     Nametab.locate_in_absolute_module dir id
diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index c358e593d..c64038323 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -64,7 +64,7 @@ let recognize_number t =
 let constant dir s =
   try
     Declare.global_absolute_reference
-      (Names.make_path (List.map Names.id_of_string dir)
+      (Names.make_path (Names.make_dirpath (List.map Names.id_of_string dir))
                        (Names.id_of_string s) Names.CCI)
   with e -> print_endline (String.concat "." dir); print_endline s; 
             raise e
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 903a8c0ed..f2de55314 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -100,7 +100,8 @@ let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
 let uri_of_path sp tag =
  let module N = Names in
   let ext_of_sp sp = ext_of_tag tag in
-  let dir = List.map N.string_of_id (N.wd_of_sp sp) in
+  let dir0 = N.extend_dirpath (N.dirpath sp) (N.basename sp) in
+  let dir = List.map N.string_of_id (N.repr_dirpath dir0) in
    "cic:/" ^ (String.concat "/" dir) ^ "." ^ (ext_of_sp sp)
 ;;
 
@@ -797,7 +798,8 @@ let mkfilename dn sp ext =
    match dn with
       None         -> None
     | Some basedir ->
-	let dir = List.map N.string_of_id (N.wd_of_sp sp) in
+	let dir0 = N.extend_dirpath (N.dirpath sp) (N.basename sp) in
+	let dir = List.map N.string_of_id (N.repr_dirpath dir0) in
        Some (basedir ^ join_dirs basedir dir ^ "." ^ ext)
 ;;
 
@@ -918,9 +920,11 @@ with _ -> print_if_verbose ("EXCEPTION RAISED!!!\n");
            print_if_verbose ("Suppongo gia' stampato " ^ Names.string_of_id id ^ "\n")
           end
        end
-   | L.OpenedSection (id,_) ->
+   | L.OpenedSection (dir,_) ->
+       let id = snd (Names.split_dirpath dir) in
        print_if_verbose ("OpenDir " ^ Names.string_of_id id ^ "\n")
-   | L.ClosedSection (_,id,state) ->
+   | L.ClosedSection (_,dir,state) ->
+      let id = snd (Names.split_dirpath dir) in
       print_if_verbose("ClosedDir " ^ Names.string_of_id id ^ "\n") ;
       if bprintleaf then
        begin
@@ -994,7 +998,8 @@ let printSection id dn =
    let rec find_closed_section =
     function
        [] -> raise Not_found
-     | (_,Lib.ClosedSection (_,id',ls))::_ when id' = id -> ls
+     | (_,Lib.ClosedSection (_,dir,ls))::_ when snd (N.split_dirpath dir) = id
+	 -> ls
      | _::t -> find_closed_section t
    in
     print_string ("Searching " ^ Names.string_of_path sp ^ "\n") ;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index bc7a0b836..cf35caf0c 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -244,7 +244,7 @@ let print_pure_constr csr =
     | Anonymous -> print_string "_"
 (* Remove the top names for library and Scratch to avoid long names *)
   and sp_display sp = let ls = 
-    match List.map string_of_id (dirpath sp) with 
+    match List.map string_of_id (repr_dirpath (dirpath sp)) with 
         ("Scratch"::l)-> l
       | ("Coq"::_::l) -> l 
       | l             -> l
diff --git a/kernel/names.ml b/kernel/names.ml
index 3aa20400a..f2fe3be86 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -207,6 +207,22 @@ let kind_of_string = function
   | _ -> invalid_arg "kind_of_string"
 
 (*s Directory paths = section names paths *)
+let parse_fields s =
+  let len = String.length s in
+  let rec decoupe_dirs n =
+    try
+      let pos = String.index_from s n '.' in
+      let dir = String.sub s n (pos-n) in
+      let dirs,n' = decoupe_dirs (succ pos) in
+      (id_of_string dir)::dirs,n'
+    with
+      | Not_found -> [],n
+  in
+  if len = 0 then invalid_arg "parse_section_path";
+  let dirs,n = decoupe_dirs 0 in
+  let id = String.sub s n (len-n) in
+  dirs, (id_of_string id)
+
 type module_ident = identifier
 type dir_path = module_ident list
 
@@ -218,44 +234,43 @@ module ModIdOrdered =
 
 module ModIdmap = Map.Make(ModIdOrdered)
 
-let make_dirpath x = x
-let repr_dirpath x = x
+(* These are the only functions which depend on how a dirpath is encoded *)
+let make_dirpath x = List.rev x
+let repr_dirpath x = List.rev x
+let rev_repr_dirpath x = x
 
 let dirpath_prefix = function 
   | [] -> anomaly "dirpath_prefix: empty dirpath"
-  | l -> snd (list_sep_last l)
+  | _::l -> l
 
-let split_dirpath d = let (b,d) = list_sep_last d in (d,b)
+let split_dirpath = function
+  | [] -> failwith "Empty"
+  | d::b -> (b,d)
 
-let parse_sp s =
-  let len = String.length s in
-  let rec decoupe_dirs n =
-    try
-      let pos = String.index_from s n '.' in
-      let dir = String.sub s n (pos-n) in
-      let dirs,n' = decoupe_dirs (succ pos) in
-      (id_of_string dir)::dirs,n'
-    with
-      | Not_found -> [],n
-  in
-  if len = 0 then invalid_arg "parse_section_path";
-  let dirs,n = decoupe_dirs 0 in
-  let id = String.sub s n (len-n) in
-  dirs, (id_of_string id)
+let extend_dirpath d id = id::d
+let add_dirpath_prefix id d = d@[id]
+
+let is_dirpath_prefix_of d1 d2 = list_prefix_of (List.rev d1) (List.rev d2)
+(**)
+
+let is_empty_dirpath d = (d = [])
 
 let dirpath_of_string s =
   try
-    let sl,s = parse_sp s in
-    sl @ [s]
+    let sl,s = parse_fields s in
+    make_dirpath (sl @ [s])
   with
     | Invalid_argument _ -> invalid_arg "dirpath_of_string"
 
 let string_of_dirpath = function
   | [] -> "<empty>"
-  | sl -> String.concat "." (List.map string_of_id sl)
+  | sl -> String.concat "." (List.map string_of_id (repr_dirpath sl))
 
 let pr_dirpath sl = [< 'sTR (string_of_dirpath sl) >]
 
+let default_module_name = id_of_string "Top"
+let default_module = make_dirpath [default_module_name]
+
 (*s Section paths are absolute names *)
 
 type section_path = {
@@ -278,20 +293,13 @@ let string_of_path sp =
 
 let path_of_string s =
   try
-    let sl,s = parse_sp s in
-    make_path sl s CCI
+    let sl,s = parse_fields s in
+    make_path (make_dirpath sl) s CCI
   with
     | Invalid_argument _ -> invalid_arg "path_of_string"
 
 let pr_sp sp = [< 'sTR (string_of_path sp) >]
 
-let sp_of_wd = function
-  | [] -> invalid_arg "Names.sp_of_wd"
-  | l -> let (bn,dp) = list_sep_last l in make_path dp bn OBJ
-
-let wd_of_sp sp = 
-  let (sp,id,_) = repr_path sp in sp @ [id]
-
 let sp_ord sp1 sp2 =
   let (p1,id1,k) = repr_path sp1
   and (p2,id2,k') = repr_path sp2 in
@@ -302,8 +310,6 @@ let sp_ord sp1 sp2 =
   else
     ck
 
-let is_dirpath_prefix_of = list_prefix_of
-
 module SpOrdered =
   struct
     type t = section_path
@@ -345,6 +351,15 @@ module Hname = Hashcons.Make(
     let hash = Hashtbl.hash
   end)
 
+module Hdir = Hashcons.Make(
+  struct 
+    type t = dir_path
+    type u = identifier -> identifier
+    let hash_sub hident d = List.map hident d
+    let equal d1 d2 = List.for_all2 (==) d1 d2
+    let hash = Hashtbl.hash
+  end)
+
 module Hsp = Hashcons.Make(
   struct 
     type t = section_path
@@ -364,6 +379,6 @@ let hcons_names () =
   let hstring = Hashcons.simple_hcons Hashcons.Hstring.f () in
   let hident = Hashcons.simple_hcons Hident.f hstring in
   let hname = Hashcons.simple_hcons Hname.f hident in
+  let hdir = Hashcons.simple_hcons Hdir.f hident in
   let hspcci = Hashcons.simple_hcons Hsp.f hident in
-  let hspfw = Hashcons.simple_hcons Hsp.f hident in
-  (hspcci,hspfw,hname,hident,hstring)
+  (hspcci,hdir,hname,hident,hstring)
diff --git a/kernel/names.mli b/kernel/names.mli
index a50dc28c4..478b1c8e4 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -63,12 +63,14 @@ val kind_of_string : string -> path_kind
 
 (*s Directory paths = section names paths *)
 type module_ident = identifier
-type dir_path = module_ident list
+type dir_path (*= module_ident list*)
 
 module ModIdmap : Map.S with type key = module_ident
 
 val make_dirpath : module_ident list -> dir_path
 val repr_dirpath : dir_path -> module_ident list
+val rev_repr_dirpath : dir_path -> module_ident list
+val is_empty_dirpath : dir_path -> bool
 
 (* Give the immediate prefix of a [dir_path] *)
 val dirpath_prefix : dir_path -> dir_path 
@@ -76,10 +78,14 @@ val dirpath_prefix : 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_prefix : module_ident -> dir_path -> dir_path
+
 (* Printing of directory paths as ["coq_root.module.submodule"] *)
 val string_of_dirpath : dir_path -> string
 val pr_dirpath : dir_path -> std_ppcmds
 
+val default_module : dir_path
 
 (*s Section paths are {\em absolute} names *)
 type section_path
@@ -93,9 +99,6 @@ val dirpath : section_path -> dir_path
 val basename : section_path -> identifier
 val kind_of_path : section_path -> path_kind
 
-val sp_of_wd : module_ident list -> section_path
-val wd_of_sp : section_path -> module_ident list
-
 (* 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
@@ -128,5 +131,5 @@ type global_reference =
 
 (* Hash-consing *)
 val hcons_names : unit ->
-  (section_path -> section_path) * (section_path -> section_path) *
+  (section_path -> section_path) * (dir_path -> dir_path) *
   (name -> name) * (identifier -> identifier) * (string -> string)
diff --git a/kernel/term.ml b/kernel/term.ml
index ea720dbd3..96a4d0d38 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -246,6 +246,17 @@ let hcons_term (hsorts,hsp,hname,hident) =
 (* Constructs a DeBrujin index with number n *)
 let mkRel   n = IsRel n
 
+let r = ref None
+
+let mkRel n =
+  let rels = match !r with
+    | None -> let a = 
+  [|mkRel  1;mkRel  2;mkRel  3;mkRel  4;mkRel  5;mkRel  6;mkRel  7; mkRel  8;
+    mkRel  9;mkRel 10;mkRel 11;mkRel 12;mkRel 13;mkRel 14;mkRel 15; mkRel 16|]
+      in r := Some a; a
+    | Some a -> a in
+  if 0<n & n<=16 then rels.(n-1) else mkRel n
+
 (* Constructs an existential variable named "?n" *)
 let mkMeta  n =  IsMeta n
 
@@ -254,6 +265,7 @@ let mkVar id = IsVar id
 
 (* Construct a type *)
 let mkSort s = IsSort s
+
 (* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *)
 (* (that means t2 is declared as the type of t1) *)
 let mkCast (t1,t2) =
@@ -1001,10 +1013,13 @@ let mkMeta = mkMeta
 let mkVar = mkVar
 
 (* Construct a type *)
-let mkSort   = mkSort
 let mkProp   = mkSort mk_Prop
 let mkSet    = mkSort mk_Set
 let mkType u = mkSort (Type u)
+let mkSort   = function
+  | Prop Null -> mkProp (* Easy sharing *)
+  | Prop Pos -> mkSet
+  | s -> mkSort s
 
 let prop = mk_Prop
 and spec = mk_Set
@@ -1651,22 +1666,20 @@ module Hsorts =
 
 let hsort = Hsorts.f
 
-let hcons_constr (hspcci,hspfw,hname,hident,hstr) =
+let hcons_constr (hspcci,hdir,hname,hident,hstr) =
   let hsortscci = Hashcons.simple_hcons hsort hcons1_univ in
-  let hsortsfw = Hashcons.simple_hcons hsort hcons1_univ in
   let hcci = hcons_term (hsortscci,hspcci,hname,hident) in
-  let hfw = hcons_term (hsortsfw,hspfw,hname,hident) in
   let htcci = Hashcons.simple_hcons Htype.f (hcci,hsortscci) in
-  (hcci,hfw,htcci)
+  (hcci,htcci)
 
 let hcons1_constr =
   let hnames = hcons_names () in
-  let (hc,_,_) = hcons_constr hnames in
+  let (hc,_) = hcons_constr hnames in
   hc
 
 let hcons1_types =
   let hnames = hcons_names () in
-  let (_,_,ht) = hcons_constr hnames in
+  let (_,ht) = hcons_constr hnames in
   ht
 
 (* Abstract decomposition of constr to deal with generic functions *)
diff --git a/kernel/term.mli b/kernel/term.mli
index 418ce2236..90b1dd807 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -641,13 +641,12 @@ val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
 
 val hcons_constr:
   (section_path -> section_path) *
-  (section_path -> section_path) *
+  (dir_path -> dir_path) *
   (name -> name) *
   (identifier -> identifier) *
   (string -> string) 
   ->
     (constr -> constr) *
-    (constr -> constr) *
     (types -> types)
 
 val hcons1_constr : constr -> constr
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 915092b2e..a74ea74fb 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -67,7 +67,7 @@ let implicit_univ =
     { u_mod = Names.make_dirpath [Names.id_of_string "implicit_univ"];
       u_num = 0 }
 
-let current_module = ref []
+let current_module = ref Names.default_module
 
 let set_module m = current_module := m
 
@@ -461,12 +461,12 @@ module Huniv =
   Hashcons.Make(
     struct
       type t = universe
-      type u = Names.identifier -> Names.identifier
-      let hash_aux hstr {u_mod=sp; u_num=n} = {u_mod=List.map hstr sp; u_num=n}
-      let hash_sub hstr = function
-	| Variable u -> Variable (hash_aux hstr u)
+      type u = Names.dir_path -> Names.dir_path
+      let hash_aux hdir {u_mod=sp; u_num=n} = {u_mod = hdir sp; u_num = n}
+      let hash_sub hdir = function
+	| Variable u -> Variable (hash_aux hdir u)
 	| Max (gel,gtl) ->
-	    Max (List.map (hash_aux hstr) gel, List.map (hash_aux hstr) gtl)
+	    Max (List.map (hash_aux hdir) gel, List.map (hash_aux hdir) gtl)
       let equal u v =
 	match u, v with
 	  | Variable u, Variable v -> u == v
@@ -477,6 +477,6 @@ module Huniv =
     end)
 
 let hcons1_univ u =
-  let _,_,_,hid,_ = Names.hcons_names () in
-  Hashcons.simple_hcons Huniv.f hid u
+  let _,hdir,_,_,_ = Names.hcons_names () in
+  Hashcons.simple_hcons Huniv.f hdir u
 
diff --git a/library/declare.ml b/library/declare.ml
index c2ac0ce45..1c034190e 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -43,24 +43,28 @@ let depth_of_strength = function
 
 let restrict_path n sp =
   let dir, s, k = repr_path sp in
-  let dir' = list_lastn n dir in
-  Names.make_path dir' s k
+  let dir' = list_lastn n (repr_dirpath dir) in
+  Names.make_path (make_dirpath dir') s k
 
 let make_strength_0 () = 
   let depth = Lib.sections_depth () in
   let cwd = Lib.cwd() in
   if depth > 0 then DischargeAt (cwd, depth) else NeverDischarge
 
+let extract_dirpath_prefix n dir =
+  let dir = repr_dirpath dir in
+  make_dirpath (list_firstn (List.length dir -n) dir)
+
 let make_strength_1 () =
   let depth = Lib.sections_depth () in
   let cwd = Lib.cwd() in
-  if depth > 1 then DischargeAt (list_firstn (List.length cwd -1) cwd, depth-1)
+  if depth > 1 then DischargeAt (extract_dirpath_prefix 1 cwd, depth-1)
   else NeverDischarge
 
 let make_strength_2 () =
   let depth = Lib.sections_depth () in
   let cwd = Lib.cwd() in
-  if depth > 2 then DischargeAt (list_firstn (List.length cwd -2) cwd, depth-2)
+  if depth > 2 then DischargeAt (extract_dirpath_prefix 2 cwd, depth-2)
   else NeverDischarge
 
 
@@ -450,10 +454,10 @@ let is_section_variable = function
 
 let is_global id =
   try 
-    let osp = Nametab.locate (make_qualid [] id) in
+    let osp = Nametab.locate (make_short_qualid id) in
     (* Compatibilité V6.3: Les variables de section ne sont pas globales
     not (is_section_variable osp) && *)
-    list_prefix_of (dirpath_of_global osp) (Lib.cwd())
+    is_dirpath_prefix_of (dirpath_of_global osp) (Lib.cwd())
   with Not_found -> 
     false
 
diff --git a/library/global.ml b/library/global.ml
index 1f509bcde..b55f741dd 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -78,9 +78,9 @@ let qualid_of_global ref =
     if (try Nametab.locate qid = ref with Not_found -> false) then qid
     else match dir with
       | [] -> Nametab.qualid_of_sp sp
-      | a::l -> find_visible l (a::qdir)
+      | a::l -> find_visible l (add_dirpath_prefix a qdir)
   in
-  find_visible (List.rev (dirpath sp)) []
+  find_visible (rev_repr_dirpath (dirpath sp)) (make_dirpath [])
 
 let string_of_global ref = Nametab.string_of_qualid (qualid_of_global ref)
 
diff --git a/library/lib.ml b/library/lib.ml
index c6ebfa000..e85e834ec 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -17,9 +17,9 @@ open Summary
 type node = 
   | Leaf of obj
   | Module of dir_path
-  | OpenedSection of module_ident * Summary.frozen
+  | OpenedSection of dir_path * Summary.frozen
   (* bool is to tell if the section must be opened automatically *)
-  | ClosedSection of bool * module_ident * library_segment
+  | ClosedSection of bool * dir_path * library_segment
   | FrozenState of Summary.frozen
 
 and library_entry = section_path * node
@@ -36,9 +36,7 @@ and library_segment = library_entry list
 
 let lib_stk = ref ([] : (section_path * node) list)
 
-let default_module_name = id_of_string "Top"
-let default_module = make_dirpath [default_module_name]
-let init_toplevel_root () = Nametab.push_library_root default_module_name
+let init_toplevel_root () = Nametab.push_library_root default_module
 
 let module_name = ref None
 let path_prefix = ref (default_module : dir_path)
@@ -48,23 +46,19 @@ let module_sp () =
 
 let recalc_path_prefix () =
   let rec recalc = function
-    | (sp, OpenedSection (modid,_)) :: _ -> (dirpath sp)@[modid]
+    | (sp, OpenedSection (dir,_)) :: _ -> dir
     | _::l -> recalc l
     | [] -> module_sp ()
   in
   path_prefix := recalc !lib_stk
 
-let pop_path_prefix () =
-  let rec pop = function
-    | [] -> assert false
-    | [_] -> []
-    | s::l -> s :: (pop l)
-  in
-  path_prefix := pop !path_prefix
+let pop_path_prefix () = path_prefix := fst (split_dirpath !path_prefix)
 
 let make_path id k = Names.make_path !path_prefix id k
 
-let sections_depth () = List.length !path_prefix - List.length (module_sp ())
+let sections_depth () =
+  List.length (rev_repr_dirpath !path_prefix)
+  - List.length (rev_repr_dirpath (module_sp ()))
 
 let cwd () = !path_prefix
 
@@ -122,11 +116,11 @@ let contents_after = function
 (* Sections. *)
 
 let open_section id =
-  let dir = !path_prefix @ [id] in
+  let dir = extend_dirpath !path_prefix id in
   let sp = make_path id OBJ in
   if Nametab.exists_section dir then
     errorlabstrm "open_section" [< pr_id id; 'sTR " already exists" >];
-  add_entry sp (OpenedSection (id, freeze_summaries()));
+  add_entry sp (OpenedSection (dir, freeze_summaries()));
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
   Nametab.push_section dir;
   path_prefix := dir;
@@ -145,7 +139,7 @@ let start_module s =
   if !path_prefix <> default_module then
     error "some sections are already opened";
   module_name := Some s;
-  (match split_dirpath s with [],id -> Nametab.push_library_root id | _ -> ());
+  Nametab.push_library_root s;
   Univ.set_module s;
   let _ = add_anonymous_entry (Module s) in
   path_prefix := s
@@ -179,10 +173,12 @@ let export_segment seg =
   clean [] seg
 
 let close_section export id =
-  let sp,fs = 
+  let sp,dir,fs = 
     try match find_entry_p is_opened_section with
-      | sp,OpenedSection (id',fs) -> 
-	  if id<>id' then error "this is not the last opened section"; (sp,fs)
+      | sp,OpenedSection (dir,fs) -> 
+	  if id<>snd(split_dirpath dir) then
+	    error "this is not the last opened section";
+	  (sp,dir,fs)
       | _ -> assert false
     with Not_found ->
       error "no opened section"
@@ -191,8 +187,8 @@ let close_section export id =
   lib_stk := before;
   let after' = export_segment after in
   pop_path_prefix ();
-  add_entry (make_path id OBJ) (ClosedSection (export, id, after'));
-  (sp,after,fs)
+  add_entry (make_path id OBJ) (ClosedSection (export, dir, after'));
+  (dir,after,fs)
 
 (* The following function exports the whole library segment, that will be 
    saved as a module. Objects are presented in chronological order, and
@@ -252,7 +248,7 @@ let init () =
   lib_stk := [];
   add_frozen_state ();
   module_name := None;
-  path_prefix := [];
+  path_prefix := make_dirpath [];
   init_summaries()
 
 (* Initial state. *)
diff --git a/library/lib.mli b/library/lib.mli
index 0421f0812..faf80428a 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -21,8 +21,8 @@ open Summary
 type node = 
   | Leaf of obj
   | Module of dir_path
-  | OpenedSection of module_ident * Summary.frozen
-  | ClosedSection of bool * module_ident * library_segment
+  | OpenedSection of dir_path * Summary.frozen
+  | ClosedSection of bool * dir_path * library_segment
   | FrozenState of Summary.frozen
 
 and library_entry = section_path * node
@@ -50,7 +50,7 @@ val contents_after : section_path option -> library_segment
 
 val open_section : identifier -> section_path
 val close_section : 
-  export:bool -> identifier -> section_path * library_segment * Summary.frozen
+  export:bool -> identifier -> dir_path * library_segment * Summary.frozen
 val sections_are_opened : unit -> bool
 
 val make_path : identifier -> path_kind -> section_path
diff --git a/library/library.ml b/library/library.ml
index df5d588bd..46c6b8b50 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -145,7 +145,8 @@ let module_is_loaded dir =
   try let _ = CompUnitmap.find dir !modules_table in true
   with Not_found -> false
 
-let module_is_opened s = (find_module [id_of_string s]).module_opened
+let module_is_opened s =
+  (find_module (make_dirpath [id_of_string s])).module_opened
 
 let loaded_modules () =
   CompUnitmap.fold (fun s _ l -> s :: l) !modules_table []
@@ -183,8 +184,8 @@ let segment_iter f =
   let rec apply = function
     | sp,Leaf obj -> f (sp,obj)
     | _,OpenedSection _ -> assert false
-    | sp,ClosedSection (export,s,seg) ->
-	push_section (wd_of_sp sp);
+    | sp,ClosedSection (export,dir,seg) ->
+	push_section dir;
 	if export then iter seg
     | _,(FrozenState _ | Module _) -> ()
   and iter seg =
@@ -263,9 +264,7 @@ let rec load_module = function
 	  [< 'sTR ("The file " ^ f ^ " contains module"); 'sPC;
 	  pr_dirpath md.md_name; 'sPC; 'sTR "and not module"; 'sPC;
 	  pr_dirpath dir >];
-      (match split_dirpath dir with
-	| [], id -> Nametab.push_library_root id
-	| _ -> ());
+      Nametab.push_library_root dir;
       compunit_cache := Stringmap.add f (md, digest) !compunit_cache;
       (md, digest) in
     intern_module digest f md
@@ -317,7 +316,7 @@ let locate_qualified_library qid =
   try
     let dir, base = repr_qualid qid in 
     let loadpath =
-      if dir = [] then get_load_path ()
+      if is_empty_dirpath dir then get_load_path ()
       else 
         (* we assume dir is an absolute dirpath *)
 	load_path_of_logical_path dir
@@ -325,7 +324,7 @@ let locate_qualified_library qid =
     if loadpath = [] then raise LibUnmappedDir;
     let name =  (string_of_id base)^".vo" in
     let path, file = System.where_in_path loadpath name in
-    (LibInPath, find_logical_path path@[base], file)
+    (LibInPath, extend_dirpath (find_logical_path path) base, file)
   with Not_found -> raise LibNotFound
 
 let try_locate_qualified_library qid =
@@ -365,9 +364,7 @@ let locate_by_filename_only id f =
        m.module_filename);
     (LibLoaded, md.md_name, m.module_filename)
   with Not_found ->
-    (match split_dirpath md.md_name with
-      | [], id -> Nametab.push_library_root id
-      | _ -> ());
+    Nametab.push_library_root md.md_name;
     compunit_cache := Stringmap.add f (md, digest) !compunit_cache;
     (LibInPath, md.md_name, f)
 
@@ -375,7 +372,7 @@ let locate_module qid = function
   | Some f ->
       (* A name is specified, we have to check it contains module id *)
       let prefix, id = repr_qualid qid in
-      assert (prefix = []);
+      assert (is_empty_dirpath prefix);
       let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in
       locate_by_filename_only (Some id) f
   | None ->
diff --git a/library/nametab.ml b/library/nametab.ml
index f09787866..309841796 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -18,14 +18,16 @@ type qualid = dir_path * identifier
 let make_qualid p id = (p,id)
 let repr_qualid q = q
 
-let string_of_qualid (l,id) =
-  let dir = if l = [] then "" else string_of_dirpath l ^ "." in
-  dir ^ string_of_id id
+let empty_dirpath = make_dirpath []
+let make_short_qualid id = (empty_dirpath,id)
+
+let string_of_qualid (l,id) = string_of_path (make_path l id CCI)
+
 let pr_qualid p = pr_str (string_of_qualid p)
 
 let qualid_of_sp sp = make_qualid (dirpath sp) (basename sp)
 let qualid_of_dirpath dir = 
-  let a,l = list_sep_last (repr_qualid dir) in
+  let (l,a) = split_dirpath dir in
   make_qualid l a
 
 exception GlobalizationError of qualid
@@ -42,11 +44,13 @@ let error_global_not_found q = raise (GlobalizationError q)
 (*s Roots of the space of absolute names *)
 
 let coq_root = id_of_string "Coq"
-let default_root_prefix = []
+let default_root_prefix = make_dirpath []
 
 (* Obsolète
 let roots = ref []
-let push_library_root s = roots := list_add_set s !roots
+let push_library_root = function
+  | [] -> ()
+  | s::_ -> roots := list_add_set s !roots
 *)
 let push_library_root s = ()
 
@@ -90,6 +94,7 @@ let dirpath_of_extended_ref = function
 (* We add a binding of [[modid1;...;modidn;id]] to [o] in the name tab *)
 (* We proceed in the reverse way, looking first to [id] *)
 let push_tree extract_dirpath tab visibility dir o =
+  let extract = option_app (fun c -> rev_repr_dirpath (extract_dirpath c)) in
   let rec push level (current,dirmap) = function
     | modid :: path as dir ->
 	let mc = 
@@ -98,7 +103,7 @@ let push_tree extract_dirpath tab visibility dir o =
 	in
 	let this =
           if level >= visibility then
-            if option_app extract_dirpath current = Some dir then
+            if extract current = Some dir then
               (* This is an absolute name, we must keep it otherwise it may
                  become unaccessible forever *)
               current
@@ -107,7 +112,7 @@ let push_tree extract_dirpath tab visibility dir o =
           else current in
 	(this, ModIdmap.add modid (push (level+1) mc path) dirmap)
     | [] -> (Some o,dirmap) in
-  push 0 tab (List.rev dir)
+  push 0 tab (rev_repr_dirpath dir)
 
 let push_idtree extract_dirpath tab n dir id o =
   let modtab =
@@ -149,14 +154,14 @@ let push_syntactic_definition sp =
 
 let push_short_name_syntactic_definition sp =
   let _, s = repr_qualid (qualid_of_sp sp) in
-  push_short_name_ccipath Pervasives.max_int [] s (SyntacticDef sp)
+  push_short_name_ccipath Pervasives.max_int empty_dirpath s (SyntacticDef sp)
 
 (* This is for dischargeable non-cci objects (removed at the end of the
    section -- i.e. Hints, Grammar ...) *) (* --> Unused *)
 
 let push_short_name_object sp =
   let _, s = repr_qualid (qualid_of_sp sp) in
-  push_short_name_objpath 0 [] s sp
+  push_short_name_objpath 0 empty_dirpath s sp
 
 (* This is to remember absolute Section/Module names and to avoid redundancy *)
 
@@ -164,18 +169,18 @@ let push_section fulldir =
   let dir, s = split_dirpath fulldir in
   (* We push all partially qualified name *)
   push_long_names_secpath dir s fulldir;
-  push_long_names_secpath [] s fulldir
+  push_long_names_secpath empty_dirpath s fulldir
 
 (* These are entry points to locate names *)
 let locate_in_tree tab dir =
-  let dir = List.rev dir in
+  let dir = rev_repr_dirpath dir in
   let rec search (current,modidtab) = function
     | modid :: path -> search (ModIdmap.find modid modidtab) path
     | [] -> match current with Some o -> o | _ -> raise Not_found
   in
   search tab dir
 
-let locate_cci qid =
+let locate_cci (qid:qualid) =
   let (dir,id) = repr_qualid qid in
   locate_in_tree (Idmap.find id !the_ccitab) dir
 
@@ -196,7 +201,7 @@ let locate_obj qid =
 let push_loaded_library fulldir =
   let dir, s = split_dirpath fulldir in
   push_long_names_libpath dir s fulldir;
-  push_long_names_libpath [] s fulldir
+  push_long_names_libpath empty_dirpath s fulldir
 
 let locate_loaded_library qid =
   let (dir,id) = repr_qualid qid in
@@ -215,14 +220,14 @@ let locate_constant qid =
     | TrueGlobal (VarRef sp) -> sp
     | _ -> raise Not_found
 
-let sp_of_id _ id = match locate_cci (make_qualid [] id) with
+let sp_of_id _ id = match locate_cci (make_short_qualid id) with
   | TrueGlobal ref -> ref
   | SyntacticDef _ ->
       anomaly ("sp_of_id: "^(string_of_id id)
 	       ^" is not a true global reference but a syntactic definition")
 
 let constant_sp_of_id id =
-  match locate_cci (make_qualid [] id) with
+  match locate_cci (make_short_qualid id) with
     | TrueGlobal (ConstRef sp) -> sp
     | _ -> raise Not_found
 
diff --git a/library/nametab.mli b/library/nametab.mli
index 44e4e6b44..5fb7eb237 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -28,6 +28,7 @@ type qualid
 
 val make_qualid : dir_path -> identifier -> qualid
 val repr_qualid : qualid -> dir_path * identifier
+val make_short_qualid : identifier -> qualid
 
 val string_of_qualid : qualid -> string
 val pr_qualid : qualid -> std_ppcmds
@@ -89,7 +90,7 @@ val coq_root : module_ident
 val default_root_prefix : dir_path
 
 (* This is to declare a new root *)
-val push_library_root : module_ident -> unit
+val push_library_root : dir_path -> unit
 
 (* This turns a "user" absolute name into a global reference;
    especially, constructor/inductive names are turned into internal
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 3d1ce4533..f9a0fdc3c 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -135,7 +135,7 @@ let interp_qualid p =
     | [] -> anomaly "interp_qualid: empty qualified identifier"
     | l -> 
 	let p, r = list_chop (List.length l -1) (List.map outnvar l) in
-	make_qualid p (List.hd r)
+	make_qualid (make_dirpath p) (List.hd r)
 
 let maybe_variable = function
   | [Nvar (_,s)] -> Some s
@@ -255,7 +255,7 @@ let rawconstr_of_qualid env vars loc qid =
   (* Is it a bound variable? *)
   try
     match repr_qualid qid with
-      | [],s -> ast_to_var env vars loc s
+      | d,s when is_empty_dirpath d -> ast_to_var env vars loc s
       | _ -> raise Not_found
   with Not_found ->
   (* Is it a global reference or a syntactic definition? *)
@@ -573,7 +573,7 @@ let adjust_qualid env loc ast qid =
   (* Is it a bound variable? *)
   try
     match repr_qualid qid with
-      | [],id -> ast_of_var env ast id
+      | d,id when is_empty_dirpath d -> ast_of_var env ast id
       | _ -> raise Not_found
   with Not_found ->
   (* Is it a global reference or a syntactic definition? *)
@@ -592,7 +592,7 @@ let ast_adjust_consts sigma =
     | Nmeta (loc, s) as ast -> ast
     | Nvar (loc, id) as ast ->
         if Idset.mem id env then ast
-        else adjust_qualid env loc ast (make_qualid [] id)
+        else adjust_qualid env loc ast (make_short_qualid id)
     | Node (loc, "QUALID", p) as ast ->
 	adjust_qualid env loc ast (interp_qualid p)
     | Slam (loc, None, t) -> Slam (loc, None, dbrec env t)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f98746a25..af4df3b6f 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -149,12 +149,6 @@ GEXTEND Gram
           <:ast< (PARAMETER $hyp (BINDERLIST ($LIST $bl))) >>
       ] ]
   ;
-  gallina_ext:
-      [ [ IDENT "Abstraction"; id = identarg; "["; l = ne_numarg_list; "]";
-        ":="; c = constrarg ->
-          <:ast< (ABSTRACTION $id $c ($LIST $l)) >>
-      ] ]
-  ;
   END
 
 (* Gallina inductive declarations *)
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 5f804f3f2..7baad745a 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -350,8 +350,8 @@ let rec print_library_entry with_values ent =
   match ent with
     | (sp,Lib.Leaf lobj) -> 
 	[< print_leaf_entry with_values sep (sp,lobj) >]
-    | (_,Lib.OpenedSection (id,_)) -> 
-        [< 'sTR " >>>>>>> Section "; pr_id id; 'fNL >]
+    | (sp,Lib.OpenedSection (dir,_)) -> 
+        [< 'sTR " >>>>>>> Section "; pr_id (basename sp); 'fNL >]
     | (sp,Lib.ClosedSection _) -> 
         [< 'sTR " >>>>>>> Closed Section "; pr_id (basename sp); 'fNL >]
     | (_,Lib.Module dir) ->
@@ -391,8 +391,7 @@ let read_sec_context qid =
     try Nametab.locate_section qid
     with Not_found -> error "Unknown section" in
   let rec get_cxt in_cxt = function
-    | ((sp,Lib.OpenedSection (_,_)) as hd)::rest ->
-	let dir' = make_dirpath (wd_of_sp sp) in
+    | ((sp,Lib.OpenedSection (dir',_)) as hd)::rest ->
         if dir = dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
     | ((sp,Lib.ClosedSection (_,_,ctxt)) as hd)::rest ->
         error "Cannot print the contents of a closed section"
@@ -440,7 +439,7 @@ let print_name qid =
   with Not_found -> 
   try  (* Var locale de but, pas var de section... donc pas d'implicits *)
     let dir,str = repr_qualid qid in 
-    if dir <> [] then raise Not_found;
+    if not (is_empty_dirpath dir) then raise Not_found;
     let (c,typ) = Global.lookup_named str in 
     [< print_named_decl (str,c,typ) >]
   with Not_found ->
diff --git a/parsing/termast.ml b/parsing/termast.ml
index d84c5e952..4a686a17e 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -107,7 +107,7 @@ let ast_of_ref = function
 
 let ast_of_qualid p =
   let dir, s = repr_qualid p in
-  let args = List.map nvar (dir@[s]) in
+  let args = List.map nvar ((repr_dirpath dir)@[s]) in
   ope ("QUALID", args)
 
 (**********************************************************************)
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 0013fc32f..8d44d146e 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -104,7 +104,7 @@ let make_ids ast = function
 (* Gives Qualid's and makes the possible injection identifier -> qualid *)
 let make_qid = function
   | VArg (Qualid _) as arg -> arg
-  | VArg (Identifier id) -> VArg (Qualid (make_qualid [] id))
+  | VArg (Identifier id) -> VArg (Qualid (make_short_qualid id))
   | VArg (Constr c) ->
     (match (kind_of_term c) with
     | IsConst cst -> VArg (Qualid (qualid_of_sp cst))
@@ -122,7 +122,7 @@ let constr_of_id id = function
     if mem_named_context id hyps then
       mkVar id
     else
-      let csr = global_qualified_reference (make_qualid [] id) in
+      let csr = global_qualified_reference (make_short_qualid id) in
       (match kind_of_term csr with
       | IsVar _ -> raise Not_found
       | _ -> csr)
@@ -209,7 +209,7 @@ let glob_const_nvar loc env qid =
   try
     (* We first look for a variable of the current proof *)
     match Nametab.repr_qualid qid with
-      | [],id ->
+      | d,id when is_empty_dirpath d ->
 	  (* lookup_value may raise Not_found *)
 	  (match Environ.lookup_named_value id env with
 	     | Some _ ->
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 61b2da2f9..cb244786d 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -53,8 +53,8 @@ let add_ml_include s =
   Mltop.add_ml_dir s
 
 (* Puts dir in the path of ML and in the LoadPath *)
-let coq_add_path s = Mltop.add_path s [Nametab.coq_root]
-let coq_add_rec_path s = Mltop.add_rec_path s [Nametab.coq_root]
+let coq_add_path s = Mltop.add_path s (Names.make_dirpath [Nametab.coq_root])
+let coq_add_rec_path s = Mltop.add_rec_path s (Names.make_dirpath [Nametab.coq_root])
 
 (* By the option -include -I or -R of the command line *)
 let includes = ref []
@@ -95,10 +95,7 @@ let init_load_path () =
 
 (* Must be done after restoring initial state! *)
 let init_library_roots () =
-  List.iter
-    (fun (_,alias,_) ->
-      if alias <> [] then Nametab.push_library_root (List.hd alias))
-    !includes;
+  List.iter (fun (_,alias,_) -> Nametab.push_library_root alias) !includes;
   includes := []
 
 (* Initialises the Ocaml toplevel before launching it, so that it can
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index e777a067b..7825b2b1a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -68,7 +68,7 @@ let add_require s = require_list := s :: !require_list
 let require () =
   List.iter
     (fun s -> 
-      let qid = Nametab.make_qualid [] (id_of_string (Filename.basename s)) in
+      let qid = Nametab.make_short_qualid (id_of_string (Filename.basename s)) in
       Library.require_module None qid  (Some s) false)
     (List.rev !require_list)
 
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 01b868aa2..f6d96e292 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -310,9 +310,8 @@ let catch_not_found f x =
 
 let close_section _ s = 
   let oldenv = Global.env() in
-  let sec_sp,decls,fs = close_section false s in
-  let newdir = dirpath sec_sp in
-  let olddir = wd_of_sp sec_sp in
+  let olddir,decls,fs = close_section false s in
+  let newdir = fst (split_dirpath olddir) in
   let (ops,ids,_) = 
     List.fold_left 
       (process_item oldenv newdir olddir) ([],[],([],[],[])) decls 
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index e50af4664..378ab7412 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -152,7 +152,7 @@ let add_path dir coq_dirpath =
     begin
       add_ml_dir dir;
       Library.add_load_path_entry (dir,coq_dirpath);
-      if coq_dirpath <> [] then Nametab.push_library_root (List.hd coq_dirpath)
+      Nametab.push_library_root coq_dirpath
     end
   else
     wARNING [< 'sTR ("Cannot open " ^ dir) >]
@@ -167,14 +167,16 @@ let convert_string d =
 
 let add_rec_path dir coq_dirpath =
   let dirs = all_subdirs dir in
+  let prefix = Names.repr_dirpath coq_dirpath in
   if dirs <> [] then
-    let convert_dirs (lp,cp) = (lp,coq_dirpath@(List.map convert_string cp)) in
+    let convert_dirs (lp,cp) =
+      (lp,Names.make_dirpath (prefix@(List.map convert_string cp))) in
     let dirs = map_succeed convert_dirs dirs in
     begin
       List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs;
       List.iter Library.add_load_path_entry dirs;
-      if coq_dirpath <> [] then Nametab.push_library_root (List.hd coq_dirpath)
-      else List.iter (fun (_, cp) -> if cp <> [] then Nametab.push_library_root (List.hd cp)) dirs
+      if prefix <> [] then Nametab.push_library_root coq_dirpath
+      else List.iter (fun (_, cp) -> Nametab.push_library_root cp) dirs
     end
   else
     wARNING [< 'sTR ("Cannot open " ^ dir) >]
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 41574a726..98414bf53 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -181,7 +181,8 @@ let compile verbosely f =
     let s = Filename.basename f in
     let m = Names.id_of_string s in
     let _,longf = find_file_in_path (Library.get_load_path ()) (f^".v") in
-    let ldir = (Library.find_logical_path (Filename.dirname longf)) @ [m] in
+    let ldir0 = Library.find_logical_path (Filename.dirname longf) in
+    let ldir = Names.extend_dirpath ldir0 m in
     Lib.start_module ldir;
     load_vernac verbosely longf;
     let mid = Lib.end_module m in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d37c00b24..715270e39 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -196,7 +196,7 @@ let _ =
 	   (fun () -> Mltop.add_path dir Nametab.default_root_prefix)
        | [VARG_STRING dir ; VARG_QUALID alias] ->
            let aliasdir,aliasname = Nametab.repr_qualid alias in
-	   (fun () -> Mltop.add_path dir (aliasdir@[aliasname]))
+	   (fun () -> Mltop.add_path dir (extend_dirpath aliasdir aliasname))
        | _ -> bad_vernac_args "ADDPATH")
 
 (* For compatibility *)
@@ -213,7 +213,7 @@ let _ =
 	   (fun () -> Mltop.add_rec_path dir Nametab.default_root_prefix)
        | [VARG_STRING dir ; VARG_QUALID alias] ->
            let aliasdir,aliasname = Nametab.repr_qualid alias in
-	    (fun () -> Mltop.add_rec_path dir (aliasdir@[aliasname]))
+	   (fun () ->Mltop.add_rec_path dir (extend_dirpath aliasdir aliasname))
        | _ -> bad_vernac_args "RECADDPATH")
 
 (* For compatibility *)
@@ -320,7 +320,7 @@ let _ =
        | [VARG_IDENTIFIER id] ->
 	   let s = string_of_id id in
 	   let lpe,_ = System.find_file_in_path (Library.get_load_path ()) (s^".v") in
-	   let dir = (Library.find_logical_path lpe) @ [id] in
+	   let dir = extend_dirpath (Library.find_logical_path lpe) id in
 	   fun () ->
 	     Lib.start_module dir
        | _ -> bad_vernac_args "BeginModule")
@@ -1289,8 +1289,10 @@ let _ =
 
 let cl_of_qualid qid =
   match Nametab.repr_qualid qid with
-    | [], id when string_of_id id = "FUNCLASS" -> Classops.CL_FUN
-    | [], id when string_of_id id = "SORTCLASS" -> Classops.CL_SORT
+    | d, id when string_of_id id = "FUNCLASS" & is_empty_dirpath d ->
+	Classops.CL_FUN
+    | d, id when string_of_id id = "SORTCLASS"  & is_empty_dirpath d ->
+	Classops.CL_SORT
     | _ -> Class.class_of_ref (Nametab.global dummy_loc qid)	
 
 let _ =
@@ -1309,7 +1311,7 @@ let _ =
 	   let source = cl_of_qualid qids in
 	   fun () ->
 	     if isid then match Nametab.repr_qualid qid with
-	       | [], id ->
+	       | d, id when is_empty_dirpath d ->
 		   Class.try_add_new_identity_coercion id stre source target
 	       | _ -> bad_vernac_args "COERCION"
 	     else
@@ -1685,7 +1687,7 @@ let _ =
             if (string_of_id t) = "Tables" then 
 	      print_tables ()
 	    else 
-	      mSG(print_name (Nametab.make_qualid [] t)))
+	      mSG(print_name (Nametab.make_short_qualid t)))
      | _ -> bad_vernac_args "TableField")