Petit netoyage dans lib

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

9 files changed, 105 insertions, 216 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 4fae644c2..6999ee669 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -405,7 +405,7 @@ let is_section_variable = function
 
 (* TODO temporary hack!!! *)
 let rec is_imported_modpath = function
-  | MPfile dp -> dp <> (Lib.module_dp ())
+  | MPfile dp -> dp <> (Lib.library_dp ())
 (*  | MPdot (mp,_) -> is_imported_modpath mp *)
   | _ -> false
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 74e0c225a..2be5e8a73 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -403,7 +403,7 @@ let rec get_some_body mty env = match mty with
 
 
 let intern_args interp_modtype (env,oldargs) (idl,arg) = 
-  let lib_dir = Lib.module_dp() in
+  let lib_dir = Lib.library_dp() in
   let mbids = List.map (fun id -> make_mbid lib_dir (string_of_id id)) idl in
   let mty = interp_modtype env arg in
   let dirs = List.map (fun id -> make_dirpath [id]) idl in
@@ -446,7 +446,7 @@ let end_module id =
 
   let oldoname,oldprefix,fs,lib_stack = Lib.end_module id in
   let mp = Global.end_module id in
-  let substitute, keep, special = Lib.classify_objects lib_stack in
+  let substitute, keep, special = Lib.classify_segment lib_stack in
 
   let dir = fst oldprefix in
   let msid = msid_of_prefix oldprefix in
@@ -537,7 +537,7 @@ let export_library dir =
   let cenv = Global.export dir in
   let prefix, lib_stack = Lib.end_compilation dir in
   let msid = msid_of_prefix prefix in
-  let substitute, keep, _ = Lib.classify_objects lib_stack in
+  let substitute, keep, _ = Lib.classify_segment lib_stack in
     cenv,(msid,substitute,keep)
 
 
@@ -568,7 +568,7 @@ let end_modtype id =
 
   let oldoname,prefix,fs,lib_stack = Lib.end_modtype id in
   let ln = Global.end_modtype id in
-  let substitute, _, special = Lib.classify_objects lib_stack in
+  let substitute, _, special = Lib.classify_segment lib_stack in
 
   let msid = msid_of_prefix prefix in
   let mbids = !openmodtype_info in
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 5c228d161..9edd051ca 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -31,12 +31,6 @@ val declare_module :
 val start_module : (env -> 'modtype -> module_type_entry) ->
   identifier -> (identifier list * 'modtype) list -> 'modtype option -> unit
 
-(*val declare_module : identifier -> module_entry -> unit
-
-val start_module : 
-  identifier -> identifier list -> (mod_bound_id * module_type_entry) list 
-    -> module_type_entry option -> unit
-*)
 val end_module : identifier -> unit
 
 
diff --git a/library/lib.ml b/library/lib.ml
index 243fc1aca..5ce7cf595 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -20,7 +20,7 @@ open Summary
 
 type node = 
   | Leaf of obj
-  | CompilingModule of object_prefix
+  | CompilingLibrary of object_prefix
   | OpenedModule of object_prefix * Summary.frozen
   | OpenedModtype of object_prefix * Summary.frozen
   | OpenedSection of object_prefix * Summary.frozen
@@ -34,41 +34,6 @@ and library_segment = library_entry list
 
 type lib_objects =  (identifier * obj) list
 
-let rec iter_leaves f i seg =
-  match seg with
-    | [] -> ()
-    | (oname ,Leaf obj)::segtl ->
-	f i (oname,obj);
-	iter_leaves f i segtl
-    | _ -> anomaly "We should have leaves only here"
-
-
-let open_segment = iter_leaves open_object
-
-let load_segment = iter_leaves load_object
-
-let change_kns mp seg = 
-  let subst_one = function
-    | ((sp,kn),(Leaf obj as lobj)) -> 
-	let kn' = make_kn mp empty_dirpath (label kn) in
-	  ((sp,kn'),lobj)
-    | _ -> anomaly "We should have leaves only here"
-  in
-    List.map subst_one seg
-
-let subst_segment (dirpath,(mp,dir)) subst seg = 
-  let subst_one = function
-    | ((sp,kn),Leaf obj) ->
-	let sp' = make_path dirpath (basename sp) in
-	let kn' = make_kn mp dir (label kn) in
-	let oname' = sp',kn' in
-	let obj' = subst_object (oname',subst,obj) in
-	  (oname', Leaf obj')
-    | _ -> anomaly "We should have leaves only here"
-  in
-    List.map subst_one seg
-
-
 let iter_objects f i prefix =
   List.iter (fun (id,obj) -> f i (make_oname prefix id, obj))
 
@@ -83,9 +48,9 @@ let subst_objects prefix subst seg =
   in
     list_smartmap subst_one seg
 
-let classify_objects seg =
+let classify_segment seg =
   let rec clean ((substl,keepl,anticipl) as acc) = function
-    | (_,CompilingModule _) :: _ | [] -> acc
+    | (_,CompilingLibrary _) :: _ | [] -> acc
     | ((sp,kn as oname),Leaf o) as node :: stk -> 
 	let id = id_of_label (label kn) in
 	  (match classify_object (oname,o) with 
@@ -115,22 +80,50 @@ let segment_of_objects prefix =
    sections, but on the contrary there are many constructions of section
    paths based on the library path. *) 
 
-let initial_prefix = default_module,(initial_path,empty_dirpath)
+let initial_prefix = default_library,(initial_path,empty_dirpath)
 
 let lib_stk = ref ([] : library_segment)
 
 let comp_name = ref None
+
+let library_dp () =
+  match !comp_name with Some m -> m | None -> default_library
+
+(* [path_prefix] is a pair of absolute dirpath and a pair of current
+   module path and relative section path *)
 let path_prefix = ref initial_prefix
 
-let module_dp () =
-  match !comp_name with Some m -> m | None -> default_module
+
+let cwd () = fst !path_prefix
+
+let make_path id = Libnames.make_path (cwd ()) id
+
+
+let current_prefix () = snd !path_prefix
+
+let make_kn id = 
+  let mp,dir = current_prefix () in
+    Names.make_kn mp dir (label_of_id id)
+
+
+let make_oname id = make_path id, make_kn id
+
+
+let sections_depth () =
+  List.length (repr_dirpath (snd (snd !path_prefix)))
+
+let sections_are_opened () =
+  match repr_dirpath (snd (snd !path_prefix)) with
+      [] -> false
+    | _ -> true
+
 
 let recalc_path_prefix () =
   let rec recalc = function
     | (sp, OpenedSection (dir,_)) :: _ -> dir
     | (sp, OpenedModule (dir,_)) :: _ -> dir
     | (sp, OpenedModtype (dir,_)) :: _ -> dir
-    | (sp, CompilingModule dir) :: _ -> dir
+    | (sp, CompilingLibrary dir) :: _ -> dir
     | _::l -> recalc l
     | [] -> initial_prefix
   in
@@ -140,20 +133,6 @@ let pop_path_prefix () =
   let dir,(mp,sec) = !path_prefix in
     path_prefix := fst (split_dirpath dir), (mp, fst (split_dirpath sec))
 
-let make_path id = Libnames.make_path (fst !path_prefix) id
-
-let make_kn id = 
-  let mp,dir = snd !path_prefix in
-    Names.make_kn mp dir (label_of_id id)
-
-let make_oname id = make_path id, make_kn id
-
-let sections_depth () =
-  List.length (repr_dirpath (snd (snd !path_prefix)))
-
-let cwd () = fst !path_prefix
-let current_prefix () = snd !path_prefix
-
 let find_entry_p p = 
   let rec find = function
     | [] -> raise Not_found
@@ -225,29 +204,9 @@ let is_something_opened = function
   | (_,OpenedModtype _) -> true
   | _ -> false
 
-let classify_segment seg =
-  let rec clean ((substl,keepl,anticipl) as acc) = function
-    | (_,CompilingModule _) :: _ | [] -> acc
-    | (oname,Leaf o) as node :: stk -> 
-	(match classify_object (oname,o) with 
-	   | Dispose -> clean acc stk
-	   | Keep o' -> 
-	       clean (substl, (oname,Leaf o')::keepl, anticipl) stk
-	   | Substitute o' -> 
-	       clean ((oname,Leaf o')::substl, keepl, anticipl) stk
-	   | Anticipate o' ->
-	       clean (substl, keepl, (oname,Leaf o')::anticipl) stk)
-    | (oname,ClosedSection _ as item) :: stk -> clean acc stk
-    | (_,OpenedSection _) :: _ -> error "there are still opened sections"
-    | (_,OpenedModule _) :: _ -> error "there are still opened modules"
-    | (_,OpenedModtype _) :: _ -> error "there are still opened module types"
-    | (_,FrozenState _) :: stk -> clean acc stk
-  in
-  clean ([],[],[]) (List.rev seg)
-
 let export_segment seg =
   let rec clean acc = function
-    | (_,CompilingModule _) :: _ | [] -> acc
+    | (_,CompilingLibrary _) :: _ | [] -> acc
     | (oname,Leaf o) as node :: stk ->
 	(match export_object o with
 	   | None -> clean acc stk
@@ -352,7 +311,7 @@ let start_compilation s mp =
   if snd (snd (!path_prefix)) <> empty_dirpath then
     error "some sections are already opened";
   let prefix = s, (mp, empty_dirpath) in
-  let _ = add_anonymous_entry (CompilingModule prefix) in
+  let _ = add_anonymous_entry (CompilingLibrary prefix) in
   comp_name := Some s;
   path_prefix := prefix
 
@@ -367,11 +326,11 @@ let end_compilation dir =
 	Not_found -> ()
   in
   let module_p =
-    function (_,CompilingModule _) -> true | x -> is_something_opened x
+    function (_,CompilingLibrary _) -> true | x -> is_something_opened x
   in
   let oname = 
     try match find_entry_p module_p with
-	(oname, CompilingModule prefix) -> oname
+	(oname, CompilingLibrary prefix) -> oname
       | _ -> assert false
     with
 	Not_found -> anomaly "No module declared"
@@ -416,13 +375,6 @@ let open_section id =
   path_prefix := prefix;
   prefix
 
-let sections_are_opened () =
-  try 
-    match find_entry_p is_something_opened with
-      | (_,OpenedSection _) -> true
-      | (_,OpenedModule _) -> false
-      | _ -> false
-  with Not_found -> false
 
 (* Restore lib_stk and summaries as before the section opening, and
    add a ClosedSection object. *)
@@ -499,11 +451,6 @@ let rec back_stk n stk =
 
 let back n = reset_to (back_stk n !lib_stk)
 
-(* [dir] is a section dir if [module] < [dir] <= [path_prefix] *)
-let is_section_p sp =
-  not (is_dirpath_prefix_of sp (module_dp ()))
-  & (is_dirpath_prefix_of sp (fst !path_prefix))
-
 (* State and initialization. *)
 
 type frozen = dir_path option * library_segment
diff --git a/library/lib.mli b/library/lib.mli
index 022ddb5cd..7f22250f1 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -22,57 +22,36 @@ open Summary
 
 type node = 
   | Leaf of obj
-  | CompilingModule of object_prefix
+  | CompilingLibrary of object_prefix
   | OpenedModule of object_prefix * Summary.frozen
   | OpenedModtype of object_prefix * Summary.frozen
   | OpenedSection of object_prefix * Summary.frozen
   | ClosedSection of bool * dir_path * library_segment
   | FrozenState of Summary.frozen
 
-and library_entry = object_name * node
-
-and library_segment = library_entry list
+and library_segment = (object_name * node) list
 
 type lib_objects = (identifier * obj) list
 
-(*s These functions iterate (or map) object functions.
-
-  [subst_segment prefix subst seg] makes an assumption that all
-  objects in [seg] have the same prefix. This prefix is universally
-  changed to [prefix].
-
-  [classify_segment seg] divides segment into objects which responded
-  with [Substitute], [Keep], [Anticipate] respectively, to the
-  [classify_object] function.  The order of each returned list is the
-  same as in the input list.
-
-  [change_kns mp lib] only changes the prefix of the [kernel_name]
-  part of the [object_name] of every object to [(mp,empty_dirpath)].
-  The [section_path] part of the [object_name] and the object itself
-  are unchanged.
-*)
-
-
-val open_segment : int -> library_segment -> unit
-val load_segment : int -> library_segment -> unit
-val subst_segment : 
-  object_prefix -> substitution -> library_segment -> library_segment
-val classify_segment : 
-  library_segment -> library_segment * library_segment * library_segment
-val change_kns : module_path -> library_segment -> library_segment
-
-
+(*s Object iteratation functions. *)
 
 val open_objects : int -> object_prefix -> lib_objects -> unit
 val load_objects : int -> object_prefix -> lib_objects -> unit
-val subst_objects : 
-  object_prefix -> substitution -> lib_objects -> lib_objects
-val classify_objects : 
+val subst_objects : object_prefix -> substitution -> lib_objects -> lib_objects
+
+(* [classify_segment seg] verifies that there are no OpenedThings,
+   clears ClosedSections and FrozenStates and divides Leafs according
+   to their answers to the [classify_object] function in three groups:
+   [Substitute], [Keep], [Anticipate] respectively.  The order of each
+   returned list is the same as in the input list. *)
+val classify_segment : 
   library_segment -> lib_objects * lib_objects * obj list
 
+(* [segment_of_objects prefix objs] forms a list of Leafs *)
 val segment_of_objects :
   object_prefix -> lib_objects -> library_segment
 
+
 (*s Adding operations (which call the [cache] method, and getting the
   current list of operations (most recent ones coming first). *)
 
@@ -87,41 +66,33 @@ val add_leaves : identifier -> obj list -> object_name
 val add_frozen_state : unit -> unit
 val mark_end_of_command : unit -> unit
 
+
 (*s The function [contents_after] returns the current library segment, 
   starting from a given section path. If not given, the entire segment
   is returned. *)
 
 val contents_after : object_name option -> library_segment
 
-(* Returns true if we are inside an opened module type *)
-val is_specification : unit -> bool
-
-(* Returns the most recent OpenedThing node *)
-val what_is_opened : unit -> library_entry
-
-(*s Opening and closing a section. *)
-
-val open_section : identifier -> object_prefix
-
-val close_section : export:bool -> identifier -> 
-  object_prefix * library_segment * Summary.frozen
-
-val sections_are_opened : unit -> bool
+(*s Functions relative to current path *)
 
+(* User-side names *)
+val cwd : unit -> dir_path
 val make_path : identifier -> section_path
+
+(* Kernel-side names *)
+val current_prefix : unit -> module_path * dir_path
 val make_kn : identifier -> kernel_name
 
-val cwd : unit -> dir_path
+(* Are we inside an opened section *)
+val sections_are_opened : unit -> bool
 val sections_depth : unit -> int
-val is_section_p : dir_path -> bool
 
-(*s Compilation units *)
+(* Are we inside an opened module type *)
+val is_specification : unit -> bool
 
-val start_compilation : dir_path -> module_path -> unit
-val end_compilation : dir_path -> object_prefix * library_segment
+(* Returns the most recent OpenedThing node *)
+val what_is_opened : unit -> object_name * node
 
-(* The function [module_dp] returns the [dir_path] of the current module *)
-val module_dp : unit -> dir_path
 
 (*s Modules and module types *)
 
@@ -134,10 +105,23 @@ val start_modtype :
   module_ident -> module_path -> Summary.frozen -> object_prefix
 val end_modtype : module_ident 
   -> object_name * object_prefix * Summary.frozen * library_segment
+(* Lib.add_frozen_state must be called after each of the above functions *)
 
-(* Lib.add_frozen_state must be called after all of the above functions *)
+(*s Compilation units *)
 
-val current_prefix : unit -> module_path * dir_path
+val start_compilation : dir_path -> module_path -> unit
+val end_compilation : dir_path -> object_prefix * library_segment
+
+(* The function [library_dp] returns the [dir_path] of the current
+   compiling library (or [default_library]) *)
+val library_dp : unit -> dir_path
+
+(*s Sections *)
+
+val open_section : identifier -> object_prefix
+
+val close_section : export:bool -> identifier -> 
+  object_prefix * library_segment * Summary.frozen
 
 (*s Backtracking (undo). *)
 
diff --git a/library/library.ml b/library/library.ml
index a653ccc74..e7087438b 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -124,7 +124,7 @@ type library_t = {
   library_imports : compilation_unit_name list;
   library_digest : Digest.t }
 
-module CompilingModuleOrdered = 
+module CompilingLibraryOrdered = 
   struct
     type t = dir_path
     let compare d1 d2 =
@@ -132,10 +132,10 @@ module CompilingModuleOrdered =
         (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
   end
 
-module CompilingModulemap = Map.Make(CompilingModuleOrdered)
+module CompilingLibraryMap = Map.Make(CompilingLibraryOrdered)
 
 (* This is a map from names to libraries *)
-let libraries_table = ref CompilingModulemap.empty
+let libraries_table = ref CompilingLibraryMap.empty
 
 (* These are the _ordered_ lists of loaded, imported and exported libraries *)
 let libraries_loaded_list = ref []
@@ -155,7 +155,7 @@ let unfreeze (mt,mo,mi,me) =
   libraries_exports_list := me
 
 let init () =
-  libraries_table := CompilingModulemap.empty;
+  libraries_table := CompilingLibraryMap.empty;
   libraries_loaded_list := [];
   libraries_imports_list := [];
   libraries_exports_list := []
@@ -169,14 +169,14 @@ let _ =
 
 let find_library s =
   try
-    CompilingModulemap.find s !libraries_table
+    CompilingLibraryMap.find s !libraries_table
   with Not_found ->
     error ("Unknown library " ^ (string_of_dirpath s))
 
 let library_full_filename m = (find_library m).library_filename
 
 let library_is_loaded dir =
-  try let _ = CompilingModulemap.find dir !libraries_table in true
+  try let _ = CompilingLibraryMap.find dir !libraries_table in true
   with Not_found -> false
 
 let library_is_opened dir = 
@@ -200,7 +200,7 @@ let register_loaded_library m =
     | m'::_ as l when m'.library_name = m.library_name -> l
     | m'::l' -> m' :: aux l' in
   libraries_loaded_list := aux !libraries_loaded_list;
-  libraries_table := CompilingModulemap.add m.library_name m !libraries_table
+  libraries_table := CompilingLibraryMap.add m.library_name m !libraries_table
 
   (* ... while if a library is imported/exported several time, then
      only the last occurrence is really needed - though the imported
@@ -220,42 +220,12 @@ let register_open_library export m =
     libraries_exports_list := remember_last_of_each !libraries_exports_list m
 
 (************************************************************************)
-(*s Operations on library objects and opening *)
-
-(*let segment_rec_iter f =
-  let rec apply = function
-    | sp,Leaf obj -> f (sp,obj)
-    | _,OpenedSection _ -> assert false
-    | _,ClosedSection (_,_,seg) -> iter seg
-    | _,(FrozenState _ | CompilingModule _ 
-	| OpenedModule _ | OpenedModtype _) -> ()
-  and iter seg =
-    List.iter apply seg
-  in
-  iter
-
-let segment_iter i v f =
-  let rec apply = function
-    | sp,Leaf obj -> f (i,sp,obj)
-    | _,OpenedSection _ -> assert false
-    | sp,ClosedSection (export,dir,seg) ->
-	push_dir v dir (DirClosedSection dir);
-	if export then iter seg
-    | _,(FrozenState _ | CompilingModule _ 
-	| OpenedModule _ | OpenedModtype _) -> ()
-  and iter seg =
-    List.iter apply seg
-  in
-  iter
-*)
+(*s Opening libraries *)
 
 (*s [open_library s] opens a library. The library [s] and all libraries needed by
     [s] are assumed to be already loaded. When opening [s] we recursively open
     all the libraries needed by [s] and tagged [exported]. *) 
 
-(*let open_objects i decls =
-  segment_iter i (Exactly i) open_object decls*)
-
 let eq_lib_name m1 m2 = m1.library_name = m2.library_name
 
 let open_library export explicit_libs m =
@@ -288,7 +258,7 @@ let open_libraries export modl =
 (************************************************************************)
 (*s Loading from disk to cache (preparation phase) *)
 
-let compunit_cache = ref CompilingModulemap.empty
+let compunit_cache = ref CompilingLibraryMap.empty
 
 let vo_magic_number = 0703 (* V7.3 *)
 
@@ -308,7 +278,7 @@ type library_location = LibLoaded | LibInPath
 let locate_absolute_library dir =
   (* Look if loaded in current environment *)
   try
-    let m = CompilingModulemap.find dir !libraries_table in
+    let m = CompilingLibraryMap.find dir !libraries_table in
     (dir, m.library_filename)
   with Not_found ->
   (* Look if in loadpath *)
@@ -348,11 +318,11 @@ let intern_from_file f =
 let rec intern_library (dir, f) =
   try
     (* Look if in the current logical environment *)
-    CompilingModulemap.find dir !libraries_table
+    CompilingLibraryMap.find dir !libraries_table
   with Not_found ->
   try
     (* Look if already loaded in cache and consequently its dependencies *)
-    CompilingModulemap.find dir !compunit_cache
+    CompilingLibraryMap.find dir !compunit_cache
   with Not_found ->
     (* [dir] is an absolute name which matches [f] which must be in loadpath *)
     let m = intern_from_file f in
@@ -361,12 +331,12 @@ let rec intern_library (dir, f) =
 	(str ("The file " ^ f ^ " contains library") ++ spc () ++
 	 pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
          spc() ++ pr_dirpath dir);
-    compunit_cache := CompilingModulemap.add dir m !compunit_cache;
+    compunit_cache := CompilingLibraryMap.add dir m !compunit_cache;
     try
       List.iter (intern_mandatory_library dir) m.library_deps;
       m
     with e ->
-      compunit_cache := CompilingModulemap.remove dir !compunit_cache; 
+      compunit_cache := CompilingLibraryMap.remove dir !compunit_cache; 
       raise e
 
 and intern_mandatory_library caller (dir,d) =
@@ -406,13 +376,13 @@ let rec_intern_by_filename_only id f =
   check_library_short_name f m.library_name id;
   (* We check no other file containing same library is loaded *)
   try
-    let m' = CompilingModulemap.find m.library_name !libraries_table in
+    let m' = CompilingLibraryMap.find m.library_name !libraries_table in
     Options.if_verbose warning 
       ((string_of_dirpath m.library_name)^" is already loaded from file "^
        m'.library_filename);
     m.library_name
   with Not_found ->
-    compunit_cache := CompilingModulemap.add m.library_name m !compunit_cache;
+    compunit_cache := CompilingLibraryMap.add m.library_name m !compunit_cache;
     List.iter (intern_mandatory_library m.library_name) m.library_deps;
     m.library_name
 
@@ -483,11 +453,11 @@ let string_of_library (_,dir,_) = string_of_id (List.hd (repr_dirpath dir))
 let rec load_library dir =
   try
     (* Look if loaded in current env (and consequently its dependencies) *)
-    CompilingModulemap.find dir !libraries_table
+    CompilingLibraryMap.find dir !libraries_table
   with Not_found ->
     (* [dir] is an absolute name matching [f] which must be in loadpath *)
     let m =
-      try CompilingModulemap.find dir !compunit_cache
+      try CompilingLibraryMap.find dir !compunit_cache
       with Not_found ->
         anomaly ((string_of_dirpath dir)^" should be in cache")
     in
diff --git a/library/library.mli b/library/library.mli
index 43d73d241..d1d345aab 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -54,12 +54,6 @@ val require_library_from_file :
 val start_library : string -> dir_path * string
 val save_library_to : dir_path -> string -> unit
 
-(*s [library_segment m] returns the segment of the loaded library
-    [m]; if not given, the segment of the current library is returned
-    (which is then the same as [Lib.contents_after None]). 
-*)
-(*val library_segment : dir_path option -> Lib.library_segment*)
-
 (* [library_full_filename] returns the full filename of a loaded library. *)
 
 val library_full_filename : dir_path -> string
diff --git a/library/nameops.ml b/library/nameops.ml
index 7a4b67b84..6e5de89ac 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -147,7 +147,7 @@ let next_name_away name l =
 
 let pr_lab l = str (string_of_label l)
 
-let default_module = Names.initial_dir (* = ["Top"] *)
+let default_library = Names.initial_dir (* = ["Top"] *)
 
 (*s Roots of the space of absolute names *)
 let coq_root = id_of_string "Coq"
diff --git a/library/nameops.mli b/library/nameops.mli
index 50260d731..8e751be09 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -38,7 +38,7 @@ val pr_lab : label -> Pp.std_ppcmds
 
 (* some preset paths *)
 
-val default_module : dir_path
+val default_library : dir_path
 
 (* This is the root of the standard library of Coq *)
 val coq_root : module_ident