Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisation (add_glob* et dump_*)

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

3 files changed, 143 insertions, 129 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 5e22c4d225..bb0ad74ca3 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -10,7 +10,6 @@
 
 open Pp
 open Util
-open Names
 open Libnames
 open Nameops
 open Libobject
@@ -33,7 +32,7 @@ and library_entry = object_name * node
 
 and library_segment = library_entry list
 
-type lib_objects =  (identifier * obj) list
+type lib_objects =  (Names.identifier * obj) list
 
 let iter_objects f i prefix =
   List.iter (fun (id,obj) -> f i (make_oname prefix id, obj))
@@ -53,7 +52,7 @@ let classify_segment seg =
   let rec clean ((substl,keepl,anticipl) as acc) = function
     | (_,CompilingLibrary _) :: _ | [] -> acc
     | ((sp,kn as oname),Leaf o) :: stk -> 
-	let id = id_of_label (label kn) in
+	let id = Names.id_of_label (Names.label kn) in
 	  (match classify_object (oname,o) with 
 	     | Dispose -> clean acc stk
 	     | Keep o' -> 
@@ -85,7 +84,7 @@ 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_library,(initial_path,empty_dirpath)
+let initial_prefix = default_library,(Names.initial_path,Names.empty_dirpath)
 
 let lib_stk = ref ([] : library_segment)
 
@@ -98,8 +97,21 @@ let library_dp () =
    module path and relative section path *)
 let path_prefix = ref initial_prefix
 
+let sections_depth () =
+  List.length (Names.repr_dirpath (snd (snd !path_prefix)))
+
+let sections_are_opened () =
+  match Names.repr_dirpath (snd (snd !path_prefix)) with
+      [] -> false
+    | _ -> true
+
 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 ()))
+    
 let make_path id = Libnames.make_path (cwd ()) id
 
 let path_of_include () =
@@ -112,25 +124,15 @@ 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)
+    Names.make_kn mp dir (Names.label_of_id id)
 
 let make_con id = 
   let mp,dir = current_prefix () in
-    Names.make_con mp dir (label_of_id id)
+    Names.make_con mp dir (Names.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
@@ -194,7 +196,7 @@ let add_entry sp node =
 
 let anonymous_id = 
   let n = ref 0 in
-  fun () -> incr n; id_of_string ("_" ^ (string_of_int !n))
+  fun () -> incr n; Names.id_of_string ("_" ^ (string_of_int !n))
 
 let add_anonymous_entry node =
   let id = anonymous_id () in
@@ -207,7 +209,7 @@ let add_absolutely_named_leaf sp obj =
   add_entry sp (Leaf obj)
 
 let add_leaf id obj =
-  if fst (current_prefix ()) = initial_path then 
+  if fst (current_prefix ()) = Names.initial_path then 
     error ("No session module started (use -top dir)");
   let oname = make_oname id in
   cache_object (oname,obj);
@@ -261,7 +263,7 @@ let current_mod_id () =
 
 let start_module export id mp nametab = 
   let dir = extend_dirpath (fst !path_prefix) id in
-  let prefix = dir,(mp,empty_dirpath) 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") ;
@@ -306,7 +308,7 @@ let end_module id =
 
 let start_modtype id mp nametab = 
   let dir = extend_dirpath (fst !path_prefix) id in
-  let prefix = dir,(mp,empty_dirpath) 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
@@ -363,9 +365,9 @@ let check_for_comp_unit () =
 let start_compilation s mp =
   if !comp_name <> None then
     error "compilation unit is already started";
-  if snd (snd (!path_prefix)) <> empty_dirpath then
+  if snd (snd (!path_prefix)) <> Names.empty_dirpath then
     error "some sections are already opened";
-  let prefix = s, (mp, empty_dirpath) in
+  let prefix = s, (mp, Names.empty_dirpath) in
   let _ = add_anonymous_entry (CompilingLibrary prefix) in
   comp_name := Some s;
   path_prefix := prefix
@@ -395,8 +397,8 @@ let end_compilation dir =
       | None -> anomaly "There should be a module name..."
       | Some m ->
 	  if m <> dir then anomaly 
-	    ("The current open module has name "^ (string_of_dirpath m) ^ 
-	       " and not " ^ (string_of_dirpath m));
+	    ("The current open module has name "^ (Names.string_of_dirpath m) ^ 
+	       " and not " ^ (Names.string_of_dirpath m));
   in
   let (after,_,before) = split_lib oname in
     comp_name := None;
@@ -437,13 +439,13 @@ let what_is_opened () = find_entry_p is_something_opened
    - the list of substitution to do at section closing 
 *)
 
-type abstr_list = Sign.named_context Cmap.t * Sign.named_context KNmap.t
+type abstr_list = Sign.named_context Names.Cmap.t * Sign.named_context Names.KNmap.t
 
 let sectab =
-  ref ([] : ((identifier * bool * Term.types option) list * Cooking.work_list * abstr_list) list)
+  ref ([] : ((Names.identifier * bool * Term.types option) list * Cooking.work_list * abstr_list) list)
 
 let add_section () =
-  sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab
+  sectab := ([],(Names.Cmap.empty,Names.KNmap.empty),(Names.Cmap.empty,Names.KNmap.empty)) :: !sectab
 
 let add_section_variable id impl keep =
   match !sectab with
@@ -465,11 +467,11 @@ let add_section_replacement f g hyps =
     sectab := (vars,f (Array.map Term.destVar args) exps,g sechyps abs)::sl
 	
 let add_section_kn kn =
-  let f = (fun x (l1,l2) -> (l1,KNmap.add kn x l2)) in
+  let f = (fun x (l1,l2) -> (l1,Names.KNmap.add kn x l2)) in
   add_section_replacement f f
 
 let add_section_constant kn =
-  let f = (fun x (l1,l2) -> (Cmap.add kn x l1,l2)) in
+  let f = (fun x (l1,l2) -> (Names.Cmap.add kn x l1,l2)) in
   add_section_replacement f f
 
 let replacement_context () = pi2 (List.hd !sectab)
@@ -477,17 +479,17 @@ let replacement_context () = pi2 (List.hd !sectab)
 let variables_context () = pi1 (List.hd !sectab)
 
 let section_segment_of_constant con =
-  Cmap.find con (fst (pi3 (List.hd !sectab)))
+  Names.Cmap.find con (fst (pi3 (List.hd !sectab)))
 
 let section_segment_of_mutual_inductive kn =
-  KNmap.find kn (snd (pi3 (List.hd !sectab)))
+  Names.KNmap.find kn (snd (pi3 (List.hd !sectab)))
 
 let section_instance = function
   | VarRef id -> [||]
   | ConstRef con ->
-      Cmap.find con (fst (pi2 (List.hd !sectab)))
+      Names.Cmap.find con (fst (pi2 (List.hd !sectab)))
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-      KNmap.find kn (snd (pi2 (List.hd !sectab)))
+      Names.KNmap.find kn (snd (pi2 (List.hd !sectab)))
 
 let init_sectab () = sectab := []
 let freeze_sectab () = !sectab
@@ -713,7 +715,7 @@ let back n = reset_to (back_stk n !lib_stk)
 
 (* State and initialization. *)
 
-type frozen = dir_path option * library_segment
+type frozen = Names.dir_path option * library_segment
 
 let freeze () = (!comp_name, !lib_stk)
 
@@ -757,16 +759,37 @@ let reset_initial () =
 let mp_of_global ref = 
   match ref with
     | VarRef id -> fst (current_prefix ())
-    | ConstRef cst -> con_modpath cst
-    | IndRef ind -> ind_modpath ind
-    | ConstructRef constr -> constr_modpath constr
+    | ConstRef cst -> Names.con_modpath cst
+    | IndRef ind -> Names.ind_modpath ind
+    | ConstructRef constr -> Names.constr_modpath constr
 
 let rec dp_of_mp modp =
   match modp with
-    | MPfile dp -> dp
-    | MPbound _ | MPself _ -> library_dp ()
-    | MPdot (mp,_) -> dp_of_mp mp
-
+    | Names.MPfile dp -> dp
+    | Names.MPbound _ | Names.MPself _ -> library_dp ()
+    | Names.MPdot (mp,_) -> dp_of_mp mp
+
+let rec split_mp mp = 
+  match mp with 
+    | Names.MPfile dp -> dp,  Names.empty_dirpath
+    | Names.MPdot (prfx, lbl) -> 
+	let mprec, dprec = split_mp prfx in 
+	  mprec, Names.make_dirpath (Names.id_of_string (Names.string_of_label lbl) :: (Names.repr_dirpath dprec))
+    | Names.MPself msid -> let (_, id, dp) = Names.repr_msid msid in  library_dp(), Names.make_dirpath [Names.id_of_string id]
+    | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in  library_dp(), Names.make_dirpath [Names.id_of_string id]
+
+let split_modpath mp =
+  let rec aux = function
+    | Names.MPfile dp -> dp, []
+    | Names.MPbound mbid -> 
+	library_dp (), [Names.id_of_mbid mbid]
+    | Names.MPself msid -> library_dp (), [Names.id_of_msid msid]
+    | Names.MPdot (mp,l) -> let (mp', lab) = aux mp in
+			      (mp', Names.id_of_label l :: lab)
+  in 
+  let (mp, l) = aux mp in
+    mp, l
+			
 let library_part ref =
   match ref with 
     | VarRef id -> library_dp ()
@@ -798,12 +821,12 @@ let pop_con con =
   Names.make_con mp (dirpath_prefix dir) l
 
 let con_defined_in_sec kn = 
-  let _,dir,_ = repr_con kn in
-  dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
+  let _,dir,_ = Names.repr_con kn in
+  dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
 
 let defined_in_sec kn = 
-  let _,dir,_ = repr_kn kn in
-  dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
+  let _,dir,_ = Names.repr_kn kn in
+  dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
 
 let discharge_global = function
   | ConstRef kn when con_defined_in_sec kn ->
diff --git a/library/lib.mli b/library/lib.mli
index 03498f5d99..80ce26fc6a 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -8,39 +8,31 @@
 
 (*i $Id$ i*)
 
-(*i*)
-open Util
-open Names
-open Libnames
-open Libobject
-open Summary
-open Mod_subst
-(*i*)
 
 (*s This module provides a general mechanism to keep a trace of all operations
    and to backtrack (undo) those operations. It provides also the section
    mechanism (at a low level; discharge is not known at this step). *)
 
 type node = 
-  | Leaf of obj
-  | CompilingLibrary of object_prefix
-  | OpenedModule of bool option * object_prefix * Summary.frozen
+  | Leaf of Libobject.obj
+  | CompilingLibrary of Libnames.object_prefix
+  | OpenedModule of bool option * Libnames.object_prefix * Summary.frozen
   | ClosedModule  of library_segment
-  | OpenedModtype of object_prefix * Summary.frozen
+  | OpenedModtype of Libnames.object_prefix * Summary.frozen
   | ClosedModtype of library_segment
-  | OpenedSection of object_prefix * Summary.frozen
+  | OpenedSection of Libnames.object_prefix * Summary.frozen
   | ClosedSection of library_segment
   | FrozenState of Summary.frozen
 
-and library_segment = (object_name * node) list
+and library_segment = (Libnames.object_name * node) list
 
-type lib_objects = (identifier * obj) list
+type lib_objects = (Names.identifier * Libobject.obj) list
 
 (*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 open_objects : int -> Libnames.object_prefix -> lib_objects -> unit
+val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit
+val subst_objects : Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects
 
 (* [classify_segment seg] verifies that there are no OpenedThings,
    clears ClosedSections and FrozenStates and divides Leafs according
@@ -48,23 +40,23 @@ val subst_objects : object_prefix -> substitution -> lib_objects -> lib_objects
    [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
+  library_segment -> lib_objects * lib_objects * Libobject.obj list
 
 (* [segment_of_objects prefix objs] forms a list of Leafs *)
 val segment_of_objects :
-  object_prefix -> lib_objects -> library_segment
+  Libnames.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). *)
 
-val add_leaf : identifier -> obj -> object_name
-val add_absolutely_named_leaf : object_name -> obj -> unit
-val add_anonymous_leaf : obj -> unit
+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]
    for each of them *)
-val add_leaves : identifier -> obj list -> object_name
+val add_leaves : Names.identifier -> Libobject.obj list -> Libnames.object_name
 
 val add_frozen_state : unit -> unit
 
@@ -81,19 +73,20 @@ val reset_label : int -> unit
   starting from a given section path. If not given, the entire segment
   is returned. *)
 
-val contents_after : object_name option -> library_segment
+val contents_after : Libnames.object_name option -> library_segment
 
 (*s Functions relative to current path *)
 
 (* User-side names *)
-val cwd : unit -> dir_path
-val make_path : identifier -> section_path
-val path_of_include : unit -> section_path
+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
 
 (* Kernel-side names *)
-val current_prefix : unit -> module_path * dir_path
-val make_kn : identifier -> kernel_name
-val make_con : identifier -> constant
+val current_prefix : unit -> Names.module_path * Names.dir_path
+val make_kn : Names.identifier -> Names.kernel_name
+val make_con : Names.identifier -> Names.constant
 
 (* Are we inside an opened section *)
 val sections_are_opened : unit -> bool
@@ -102,53 +95,55 @@ val sections_depth : unit -> int
 (* Are we inside an opened module type *)
 val is_modtype : unit -> bool
 val is_module : unit -> bool
-val current_mod_id : unit -> module_ident
+val current_mod_id : unit -> Names.module_ident
 
 (* Returns the most recent OpenedThing node *)
-val what_is_opened : unit -> object_name * node
+val what_is_opened : unit -> Libnames.object_name * node
 
 
 (*s Modules and module types *)
 
 val start_module : 
-  bool option -> module_ident -> module_path -> Summary.frozen -> object_prefix
-val end_module : module_ident 
-  -> object_name * object_prefix * Summary.frozen * library_segment
+  bool option -> Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix
+val end_module : Names.module_ident 
+  -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment
 
 val start_modtype : 
-  module_ident -> module_path -> Summary.frozen -> object_prefix
-val end_modtype : module_ident 
-  -> object_name * object_prefix * Summary.frozen * library_segment
+  Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix
+val end_modtype : Names.module_ident 
+  -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment
 (* [Lib.add_frozen_state] must be called after each of the above functions *)
 
 (*s Compilation units *)
 
-val start_compilation : dir_path -> module_path -> unit
-val end_compilation : dir_path -> object_prefix * library_segment
+val start_compilation : Names.dir_path -> Names.module_path -> unit
+val end_compilation : Names.dir_path -> Libnames.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
+val library_dp : unit -> Names.dir_path
 
 (* Extract the library part of a name even if in a section *)
-val dp_of_mp : module_path -> dir_path
-val library_part :  global_reference -> dir_path
-val remove_section_part : global_reference -> dir_path
+val dp_of_mp : Names.module_path -> Names.dir_path
+val split_mp : Names.module_path -> Names.dir_path * Names.dir_path
+val split_modpath : Names.module_path -> Names.dir_path * Names.identifier list
+val library_part :  Libnames.global_reference -> Names.dir_path
+val remove_section_part : Libnames.global_reference -> Names.dir_path
 
 (*s Sections *)
 
-val open_section : identifier -> unit
-val close_section : identifier -> unit
+val open_section : Names.identifier -> unit
+val close_section : Names.identifier -> unit
 
 (*s Backtracking (undo). *)
 
-val reset_to : object_name -> unit
-val reset_name : identifier located -> unit
-val remove_name : identifier located -> unit
-val reset_mod : identifier located -> unit
-val reset_to_state : object_name -> unit
+val reset_to : Libnames.object_name -> unit
+val reset_name : Names.identifier Util.located -> unit
+val remove_name : Names.identifier Util.located -> unit
+val reset_mod : Names.identifier Util.located -> unit
+val reset_to_state : Libnames.object_name -> unit
 
-val has_top_frozen_state : unit -> object_name option
+val has_top_frozen_state : unit -> Libnames.object_name option
 
 (* [back n] resets to the place corresponding to the $n$-th call of 
    [mark_end_of_command] (counting backwards) *)
@@ -168,28 +163,28 @@ val reset_initial : unit -> unit
 
 
 (* XML output hooks *)
-val set_xml_open_section : (identifier -> unit) -> unit
-val set_xml_close_section : (identifier -> unit) -> unit
+val set_xml_open_section : (Names.identifier -> unit) -> unit
+val set_xml_close_section : (Names.identifier -> unit) -> unit
 
 
 (*s Section management for discharge *)
 
-val section_segment_of_constant : constant -> Sign.named_context
-val section_segment_of_mutual_inductive: mutual_inductive -> Sign.named_context
+val section_segment_of_constant : Names.constant -> Sign.named_context
+val section_segment_of_mutual_inductive: Names.mutual_inductive -> Sign.named_context
 
-val section_instance : global_reference -> identifier array
+val section_instance : Libnames.global_reference -> Names.identifier array
 
-val add_section_variable : identifier -> bool -> Term.types option -> unit
-val add_section_constant : constant -> Sign.named_context -> unit
-val add_section_kn : kernel_name -> Sign.named_context -> unit
+val add_section_variable : Names.identifier -> bool -> Term.types option -> unit
+val add_section_constant : Names.constant -> Sign.named_context -> unit
+val add_section_kn : Names.kernel_name -> Sign.named_context -> unit
 val replacement_context : unit ->
-  (identifier array Cmap.t * identifier array KNmap.t)
+  (Names.identifier array Names.Cmap.t * Names.identifier array Names.KNmap.t)
 
 (*s Discharge: decrease the section level if in the current section *)
 
-val discharge_kn :  kernel_name -> kernel_name
-val discharge_con : constant -> constant
-val discharge_global : global_reference -> global_reference
-val discharge_inductive : inductive -> inductive
+val discharge_kn :  Names.kernel_name -> Names.kernel_name
+val discharge_con : Names.constant -> Names.constant
+val discharge_global : Libnames.global_reference -> Libnames.global_reference
+val discharge_inductive : Names.inductive -> Names.inductive
 
 
diff --git a/library/library.ml b/library/library.ml
index 2f74fe92b9..272f01f7d7 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -18,7 +18,6 @@ open Safe_typing
 open Libobject
 open Lib
 open Nametab
-open Declaremods
 
 (*************************************************************************)
 (*s Load path. Mapping from physical to logical paths etc.*)
@@ -113,7 +112,7 @@ type compilation_unit_name = dir_path
 type library_disk = { 
   md_name : compilation_unit_name;
   md_compiled : compiled_library;
-  md_objects : library_objects;
+  md_objects : Declaremods.library_objects;
   md_deps : (compilation_unit_name * Digest.t) list;
   md_imports : compilation_unit_name list }
 
@@ -123,7 +122,7 @@ type library_disk = {
 type library_t = {
   library_name : compilation_unit_name;
   library_compiled : compiled_library;
-  library_objects : library_objects;
+  library_objects : Declaremods.library_objects;
   library_deps : (compilation_unit_name * Digest.t) list;
   library_imports : compilation_unit_name list;
   library_digest : Digest.t }
@@ -540,19 +539,16 @@ let require_library qidl export =
   let modrefl = List.map try_locate_qualified_library qidl in
   let needed = List.rev (List.fold_left rec_intern_library [] modrefl) in
   let modrefl = List.map fst modrefl in
-    if Lib.is_modtype () || Lib.is_module () then begin
-      add_anonymous_leaf (in_require (needed,modrefl,None));
-      Option.iter (fun exp ->
-	List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl)
-	export
-    end
+    if Lib.is_modtype () || Lib.is_module () then 
+      begin
+	add_anonymous_leaf (in_require (needed,modrefl,None));
+	Option.iter (fun exp ->
+	  List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl)
+	  export
+      end
     else
       add_anonymous_leaf (in_require (needed,modrefl,export));
-  if !Flags.dump then List.iter2 (fun (loc, _) dp -> 
-    Flags.dump_string (Printf.sprintf "R%d %s <> <> %s\n" 
-		    (fst (unloc loc)) (string_of_dirpath dp) "lib"))
-    qidl modrefl;
-  if !Flags.xml_export then List.iter !xml_require modrefl;
+    if !Flags.xml_export then List.iter !xml_require modrefl;
   add_frozen_state ()
 
 let require_library_from_file idopt file export =
@@ -573,18 +569,18 @@ let require_library_from_file idopt file export =
 let import_module export (loc,qid) =
   try
     match Nametab.locate_module qid with
-	MPfile dir -> 
+      | MPfile dir -> 
 	  if Lib.is_modtype () || Lib.is_module () || not export then
 	    add_anonymous_leaf (in_import (dir, export))
 	  else
 	    add_anonymous_leaf (in_require ([],[dir], Some export))
       | mp ->
-	  import_module export mp
+	  Declaremods.import_module export mp
   with
       Not_found ->
 	user_err_loc
-        (loc,"import_library",
-	 str ((string_of_qualid qid)^" is not a module"))
+          (loc,"import_library",
+	  str ((string_of_qualid qid)^" is not a module"))
   
 (************************************************************************)
 (*s Initializing the compilation of a library. *)