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

23 files changed, 491 insertions, 471 deletions

diff --git a/Makefile.common b/Makefile.common
index f31b60a58..c0584b29c 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -172,7 +172,7 @@ PRETYPING:=\
 
 INTERP:=\
   parsing/lexer.cmo interp/topconstr.cmo interp/ppextend.cmo \
-  interp/notation.cmo \
+  interp/notation.cmo interp/dumpglob.cmo \
   interp/genarg.cmo interp/syntax_def.cmo interp/reserve.cmo \
   library/impargs.cmo interp/implicit_quantifiers.cmo interp/constrintern.cmo \
   interp/modintern.cmo interp/constrextern.cmo interp/coqlib.cmo \
@@ -509,7 +509,7 @@ PRINTERSCMO:=\
   pretyping/unification.cmo pretyping/cases.cmo \
   pretyping/pretyping.cmo pretyping/clenv.cmo pretyping/pattern.cmo \
   parsing/lexer.cmo interp/ppextend.cmo interp/genarg.cmo \
-  interp/topconstr.cmo interp/notation.cmo interp/reserve.cmo		\
+  interp/topconstr.cmo interp/notation.cmo  interp/dumpglob.cmo interp/reserve.cmo		\
   library/impargs.cmo interp/constrextern.cmo \
   interp/syntax_def.cmo interp/implicit_quantifiers.cmo  interp/constrintern.cmo \
   proofs/proof_trees.cmo proofs/logic.cmo proofs/refiner.cmo \
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 5ac428f6c..71aa7e99e 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -107,7 +107,8 @@ let declare_assumption env isevars idl is_coe k bl c nl =
 	(str "Cannot declare an assumption while in proof editing mode.")
 
 let dump_definition (loc, id) s =
-  Flags.dump_string (Printf.sprintf "%s %d %s\n" s (fst (unloc loc)) (string_of_id id))
+  Dumpglob.dump_string (Printf.sprintf "%s %d %s\n" s (fst (unloc loc)) 
+			   (string_of_id id))
 
 let dump_constraint ty ((loc, n), _, _) =
   match n with
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index aa16bd4bb..26cb416ac 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -165,7 +165,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
 	    try 
 	      let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
 	      let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
-		Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
+		Dumpglob.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
 		c :: props, rest'
 	    with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
 	  ([], props) k.cl_props
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1ddcac276..54abacaf6 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -124,150 +124,6 @@ let error_inductive_parameter_not_implicit loc =
     "the 'return' clauses; they must be replaced by '_' in the 'in' clauses."))
 
 (**********************************************************************)
-(* Dump of globalization (to be used by coqdoc)                       *)
-let token_number = ref 0
-let last_pos = ref 0
-
-type coqdoc_state = Lexer.location_table * int * int
-
-let coqdoc_freeze () =
-  let lt = Lexer.location_table() in
-  let state = (lt,!token_number,!last_pos) in
-    token_number := 0;
-    last_pos := 0;
-    state
-
-let coqdoc_unfreeze (lt,tn,lp) =
-  Lexer.restore_location_table lt;
-  token_number := tn;
-  last_pos := lp
-
-open Decl_kinds
-
-let type_of_logical_kind = function
-  | IsDefinition def -> 
-      (match def with
-      | Definition -> "def"
-      | Coercion -> "coe"
-      | SubClass -> "subclass"
-      | CanonicalStructure -> "canonstruc"
-      | Example -> "ex"
-      | Fixpoint -> "def"
-      | CoFixpoint -> "def"
-      | Scheme -> "scheme"
-      | StructureComponent -> "proj"
-      | IdentityCoercion -> "coe"
-      | Instance -> "inst"
-      | Method -> "meth")
-  | IsAssumption a ->
-      (match a with
-      | Definitional -> "defax"
-      | Logical -> "prfax"
-      | Conjectural -> "prfax")
-  | IsProof th ->
-      (match th with
-      | Theorem
-      | Lemma
-      | Fact
-      | Remark
-      | Property
-      | Proposition
-      | Corollary -> "thm")
-
-let type_of_global_ref gr =
-  if Typeclasses.is_class gr then
-    "class"
-  else
-    match gr with
-    | ConstRef cst -> 
-	type_of_logical_kind (Decls.constant_kind cst)
-    | VarRef v ->
-	"var" ^ type_of_logical_kind (Decls.variable_kind v)
-    | IndRef ind ->
-	let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
-	  if mib.Declarations.mind_record then
-	    if mib.Declarations.mind_finite then "rec"
-	    else "corec"
-	  else if mib.Declarations.mind_finite then "ind"
-	  else "coind"
-    | ConstructRef _ -> "constr"
-
-let remove_sections dir =
-  if is_dirpath_prefix_of dir (Lib.cwd ()) then
-    (* Not yet (fully) discharged *)
-    extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())
-  else
-    (* Theorem/Lemma outside its outer section of definition *)
-    dir
-
-let dump_reference loc filepath modpath ident ty =
-  dump_string (Printf.sprintf "R%d %s %s %s %s\n" 
-		  (fst (unloc loc)) filepath modpath ident ty)
-
-let add_glob_gen loc sp lib_dp ty =
-  let mod_dp,id = repr_path sp in
-  let mod_dp = remove_sections mod_dp in
-  let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in
-  let filepath = string_of_dirpath lib_dp in
-  let modpath = string_of_dirpath mod_dp_trunc in
-  let ident = string_of_id id in
-    dump_reference loc filepath modpath ident ty
-
-let add_glob loc ref = 
-  let sp = Nametab.sp_of_global ref in
-  let lib_dp = Lib.library_part ref in
-  let ty = type_of_global_ref ref in
-    add_glob_gen loc sp lib_dp ty
-      
-let add_glob loc ref =
-  if !Flags.dump && loc <> dummy_loc then add_glob loc ref
-
-let mp_of_kn kn = 
-  let mp,sec,l = repr_kn kn in 
-    MPdot (mp,l) 
-
-let add_glob_kn loc kn =
-  let sp = Nametab.sp_of_syntactic_definition kn in
-  let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
-    add_glob_gen loc sp lib_dp "syndef"
-
-let add_glob_kn loc ref =
-  if !Flags.dump && loc <> dummy_loc then add_glob_kn loc ref
-
-let add_local loc id = ()
-(*   let mod_dp,id = repr_path sp in *)
-(*   let mod_dp = remove_sections mod_dp in *)
-(*   let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in *)
-(*   let filepath = string_of_dirpath lib_dp in *)
-(*   let modpath = string_of_dirpath mod_dp_trunc in *)
-(*   let ident = string_of_id id in *)
-(*     dump_string (Printf.sprintf "R%d %s %s %s %s\n"  *)
-(* 		    (fst (unloc loc)) filepath modpath ident ty) *)
-
-let dump_binding loc id = ()
-      
-let loc_of_notation f loc args ntn =
-  if args=[] or ntn.[0] <> '_' then fst (unloc loc)
-  else snd (unloc (f (List.hd args)))
-
-let ntn_loc = loc_of_notation constr_loc
-let patntn_loc = loc_of_notation cases_pattern_expr_loc
-
-let dump_notation_location pos ((path,df),sc) =
-  let rec next growing =
-    let loc = Lexer.location_function !token_number in
-    let (bp,_) = unloc loc in
-      if growing then if bp >= pos then loc else (incr token_number;next true)
-      else if bp = pos then loc
-      else if bp > pos then (decr token_number;next false)
-      else (incr token_number;next true) in
-  let loc = next (pos >= !last_pos) in
-    last_pos := pos;
-    let path = string_of_dirpath path in
-    let _sc = match sc with Some sc -> " "^sc | None -> "" in
-      dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (unloc loc)) path df)
-
-(**********************************************************************)
 (* Contracting "{ _ }" in notations *)
 
 let rec wildcards ntn n =
@@ -394,9 +250,9 @@ let rec subst_aconstr_in_rawconstr loc interp subst (renaming,(ids,_,scopes)) =
 let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args =
   let ntn,args = contract_notation ntn args in
   let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
-  if !dump then dump_notation_location (ntn_loc loc args ntn) df;
-  let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
-  subst_aconstr_in_rawconstr loc intern subst ([],env) c
+    if !Flags.dump then Dumpglob.dump_notation_location (Dumpglob.ntn_loc loc args ntn) df;
+    let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
+      subst_aconstr_in_rawconstr loc intern subst ([],env) c
 
 let set_type_scope (ids,tmp_scope,scopes) =
   (ids,Some Notation.type_scope,scopes)
@@ -476,10 +332,10 @@ let check_no_explicitation l =
 let intern_qualid loc qid intern env args =
   try match Nametab.extended_locate qid with
   | TrueGlobal ref ->
-      add_glob loc ref;
+      Dumpglob.add_glob loc ref;
       RRef (loc, ref), args
   | SyntacticDef sp ->
-      add_glob_kn loc sp;
+      Dumpglob.add_glob_kn loc sp;
       let (ids,c) = Syntax_def.search_syntactic_definition loc sp in
       let nids = List.length ids in
       if List.length args < nids then error_not_enough_arguments loc;
@@ -709,7 +565,7 @@ let find_constructor ref f aliases pats scopes =
 	    let v = Environ.constant_value (Global.env()) cst in
 	    unf (global_of_constr v)
         | ConstructRef cstr -> 
-	    add_glob loc r; 
+	    Dumpglob.add_glob loc r; 
 	    cstr, [], pats
         | _ -> raise Not_found
       in unf r
@@ -760,7 +616,7 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
   | CPatNotation (loc, ntn, args) ->
       let ntn,args = contract_pat_notation ntn args in
       let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
-      if !dump then dump_notation_location (patntn_loc loc args ntn) df;
+      if !Flags.dump then Dumpglob.dump_notation_location (Dumpglob.patntn_loc loc args ntn) df;
       let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in
       let ids'',pl = subst_cases_pattern loc (alias_of aliases) intern_pat subst scopes 
 	c
@@ -769,7 +625,7 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
       let a = alias_of aliases in
       let (c,df) = Notation.interp_prim_token_cases_pattern loc p a 
 	(tmp_scope,scopes) in
-      if !dump then dump_notation_location (fst (unloc loc)) df;
+      if !Flags.dump then Dumpglob.dump_notation_location (fst (unloc loc)) df;
       (ids,[subst,c])
   | CPatDelimiters (loc, key, e) ->
       intern_pat (find_delimiters_scope loc key::scopes) aliases None e
@@ -829,7 +685,7 @@ let push_loc_name_env lvar (ids,tmpsc,scopes as env) loc = function
   | Anonymous -> env 
   | Name id -> 
       check_hidden_implicit_parameters id lvar;
-      dump_binding loc id;
+      Dumpglob.dump_binding loc id;
       (Idset.add id ids,tmpsc,scopes)
 
 let intern_typeclass_binders intern_type lvar env bl =
@@ -1029,7 +885,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
         intern_notation intern env loc ntn args
     | CPrim (loc, p) ->
 	let c,df = Notation.interp_prim_token loc p (tmp_scope,scopes) in
-	if !dump then dump_notation_location (fst (unloc loc)) df;
+	if !Flags.dump then Dumpglob.dump_notation_location (fst (unloc loc)) df;
 	c
     | CDelimiters (loc, key, e) ->
 	intern (ids,None,find_delimiters_scope loc key::scopes) e
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index d3b8da8f9..27a46daf1 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -144,10 +144,3 @@ val interp_aconstr : implicits_env -> identifier list -> constr_expr ->
 
 (* Globalization leak for Grammar *)
 val for_grammar : ('a -> 'b) -> 'a -> 'b
-
-(* Coqdoc utility functions *)
-type coqdoc_state
-val coqdoc_freeze : unit -> coqdoc_state
-val coqdoc_unfreeze : coqdoc_state -> unit
-
-val add_glob : Util.loc -> global_reference -> unit
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
new file mode 100644
index 000000000..8cc6371f5
--- /dev/null
+++ b/interp/dumpglob.ml
@@ -0,0 +1,220 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+
+let rec drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: drop_last tl
+
+(* Dump of globalization (to be used by coqdoc) *)
+
+let glob_file = ref Pervasives.stdout
+
+let open_glob_file f =
+  glob_file := Pervasives.open_out(f ^ ".glob")
+  
+let close_glob_file () =
+  Pervasives.close_out !glob_file
+
+let dump_string s = 
+  Pervasives.output_string !glob_file s
+
+
+
+(**********************************************************************)
+(* Dump of globalization (to be used by coqdoc)                       *)
+let token_number = ref 0
+let last_pos = ref 0
+
+type coqdoc_state = Lexer.location_table * int * int
+
+let coqdoc_freeze () =
+  let lt = Lexer.location_table() in
+  let state = (lt,!token_number,!last_pos) in
+    token_number := 0;
+    last_pos := 0;
+    state
+
+let coqdoc_unfreeze (lt,tn,lp) =
+  Lexer.restore_location_table lt;
+  token_number := tn;
+  last_pos := lp
+
+open Decl_kinds
+
+let type_of_logical_kind = function
+  | IsDefinition def -> 
+      (match def with
+      | Definition -> "def"
+      | Coercion -> "coe"
+      | SubClass -> "subclass"
+      | CanonicalStructure -> "canonstruc"
+      | Example -> "ex"
+      | Fixpoint -> "def"
+      | CoFixpoint -> "def"
+      | Scheme -> "scheme"
+      | StructureComponent -> "proj"
+      | IdentityCoercion -> "coe"
+      | Instance -> "inst"
+      | Method -> "meth")
+  | IsAssumption a ->
+      (match a with
+      | Definitional -> "defax"
+      | Logical -> "prfax"
+      | Conjectural -> "prfax")
+  | IsProof th ->
+      (match th with
+      | Theorem
+      | Lemma
+      | Fact
+      | Remark
+      | Property
+      | Proposition
+      | Corollary -> "thm")
+
+let type_of_global_ref gr =
+  if Typeclasses.is_class gr then
+    "class"
+  else
+    match gr with
+    | Libnames.ConstRef cst -> 
+	type_of_logical_kind (Decls.constant_kind cst)
+    | Libnames.VarRef v ->
+	"var" ^ type_of_logical_kind (Decls.variable_kind v)
+    | Libnames.IndRef ind ->
+	let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
+	  if mib.Declarations.mind_record then
+	    if mib.Declarations.mind_finite then "rec"
+	    else "corec"
+	  else if mib.Declarations.mind_finite then "ind"
+	  else "coind"
+    | Libnames.ConstructRef _ -> "constr"
+
+let remove_sections dir =
+  if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then
+    (* Not yet (fully) discharged *)
+    Libnames.extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())
+  else
+    (* Theorem/Lemma outside its outer section of definition *)
+    dir
+
+let dump_ref loc filepath modpath ident ty =
+  dump_string (Printf.sprintf "R%d %s %s %s %s\n" 
+		  (fst (Util.unloc loc)) filepath modpath ident ty)
+
+let add_glob_gen loc sp lib_dp ty =
+  let mod_dp,id = Libnames.repr_path sp in
+  let mod_dp = remove_sections mod_dp in
+  let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp mod_dp in
+  let filepath = Names.string_of_dirpath lib_dp in
+  let modpath = Names.string_of_dirpath mod_dp_trunc in
+  let ident = Names.string_of_id id in
+    dump_ref loc filepath modpath ident ty
+
+let add_glob loc ref = 
+  let sp = Nametab.sp_of_global ref in
+  let lib_dp = Lib.library_part ref in
+  let ty = type_of_global_ref ref in
+    add_glob_gen loc sp lib_dp ty
+      
+let add_glob loc ref =
+  if !Flags.dump && loc <> Util.dummy_loc then add_glob loc ref
+
+let mp_of_kn kn = 
+  let mp,sec,l = Names.repr_kn kn in 
+    Names.MPdot (mp,l) 
+
+let add_glob_kn loc kn =
+  let sp = Nametab.sp_of_syntactic_definition kn in
+  let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
+    add_glob_gen loc sp lib_dp "syndef"
+
+let add_glob_kn loc ref =
+  if !Flags.dump && loc <> Util.dummy_loc then add_glob_kn loc ref
+
+let add_local loc id = ()
+(*   let mod_dp,id = repr_path sp in *)
+(*   let mod_dp = remove_sections mod_dp in *)
+(*   let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in *)
+(*   let filepath = string_of_dirpath lib_dp in *)
+(*   let modpath = string_of_dirpath mod_dp_trunc in *)
+(*   let ident = string_of_id id in *)
+(*     dump_string (Printf.sprintf "R%d %s %s %s %s\n"  *)
+(* 		    (fst (unloc loc)) filepath modpath ident ty) *)
+
+let dump_binding loc id = ()
+      
+(* BEGIN obsolete *)
+
+let dump_modref qid = Pp.warning ("Dumpglob.modref: not yet implemented")
+  
+let dump_def loc ref = 
+  let curr_mp, _ = Lib.current_prefix() in
+  let lib_dp, curr_dp = Lib.split_mp curr_mp in
+  let mod_dp_trunc =  Libnames.drop_dirpath_prefix lib_dp curr_dp in
+
+  let fullname = Libnames.string_of_qualid (Libnames.make_qualid mod_dp_trunc ref) in
+  let filepath = Names.string_of_dirpath lib_dp in
+    dump_string (Printf.sprintf "D%d %s %s\n" (fst (Util.unloc loc)) filepath fullname)
+
+(* END obsolete *)
+
+let dump_definition (loc, id) sec s =
+  dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (Util.unloc loc)) 
+			(Names.string_of_dirpath (Lib.current_dirpath sec)) (Names.string_of_id id))
+    
+let dump_reference loc modpath ident ty =
+  dump_string (Printf.sprintf "R%d %s %s %s %s\n" 
+		  (fst (Util.unloc loc)) (Names.string_of_dirpath (Lib.library_dp ())) modpath ident ty)
+
+let dump_constraint ((loc, n), _, _) sec ty =
+  match n with
+    | Names.Name id -> dump_definition (loc, id) sec ty
+    | Names.Anonymous -> ()
+
+let dump_modref loc mp ty =
+  if !Flags.dump then
+    let (dp, l) = Lib.split_modpath mp in
+    let fp = Names.string_of_dirpath dp in
+    let mp = Names.string_of_dirpath (Names.make_dirpath (drop_last l)) in
+      dump_string (Printf.sprintf "R%d %s %s %s %s\n" 
+			    (fst (Util.unloc loc)) fp mp "<>" ty)
+
+let dump_moddef loc mp ty =
+  if !Flags.dump then
+    let (dp, l) = Lib.split_modpath mp in
+    let mp = Names.string_of_dirpath (Names.make_dirpath l) in
+      dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (Util.unloc loc)) "<>" mp)
+
+let dump_libref loc dp ty =
+  if !Flags.dump then
+    dump_string (Printf.sprintf "R%d %s <> <> %s\n" 
+			     (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
+
+let loc_of_notation f loc args ntn =
+  if args=[] or ntn.[0] <> '_' then fst (Util.unloc loc)
+  else snd (Util.unloc (f (List.hd args)))
+
+let ntn_loc = loc_of_notation Topconstr.constr_loc
+let patntn_loc = loc_of_notation Topconstr.cases_pattern_expr_loc
+
+let dump_notation_location pos ((path,df),sc) =
+  let rec next growing =
+    let loc = Lexer.location_function !token_number in
+    let (bp,_) = Util.unloc loc in
+      if growing then if bp >= pos then loc else (incr token_number; next true)
+      else if bp = pos then loc
+      else if bp > pos then (decr token_number;next false)
+      else (incr token_number;next true) in
+  let loc = next (pos >= !last_pos) in
+    last_pos := pos;
+    let path = Names.string_of_dirpath path in
+    let _sc = match sc with Some sc -> " "^sc | None -> "" in
+      dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (Util.unloc loc)) path df)
+
+
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 0af11bad9..3482dd3a0 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -61,34 +61,6 @@ let lookup_qualid (modtype:bool) qid =
 *)
 
 
-let split_modpath mp =
-  let rec aux = function
-    | MPfile dp -> dp, []
-    | MPbound mbid -> 
-	Lib.library_dp (), [id_of_mbid mbid]
-    | MPself msid -> Lib.library_dp (), [id_of_msid msid]
-    | MPdot (mp,l) -> let (mp', lab) = aux mp in
-			(mp', id_of_label l :: lab)
-  in 
-  let (mp, l) = aux mp in
-    mp, l
-			
-let dump_moddef loc mp ty =
-  if !Flags.dump then
-    let (dp, l) = split_modpath mp in
-    let mp = string_of_dirpath (make_dirpath l) in
-      Flags.dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (unloc loc)) "<>" mp)
-
-let rec drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: drop_last tl
-
-let dump_modref loc mp ty =
-  if !Flags.dump then
-    let (dp, l) = split_modpath mp in
-    let fp = string_of_dirpath dp in
-    let mp = string_of_dirpath (make_dirpath (drop_last l)) in
-      Flags.dump_string (Printf.sprintf "R%d %s %s %s %s\n" 
-			    (fst (unloc loc)) fp mp "<>" ty)
-
 (* Search for the head of [qid] in [binders]. 
    If found, returns the module_path/kernel_name created from the dirpath
    and the basename. Searches Nametab otherwise.
@@ -96,14 +68,14 @@ let dump_modref loc mp ty =
 let lookup_module (loc,qid) =
   try
     let mp = Nametab.locate_module qid in
-      dump_modref loc mp "modtype"; mp
+      Dumpglob.dump_modref loc mp "modtype"; mp
   with
     | Not_found -> Modops.error_not_a_module_loc loc (string_of_qualid qid)
 	
 let lookup_modtype (loc,qid) =
   try
     let mp = Nametab.locate_modtype qid in
-      dump_modref loc mp "mod"; mp
+      Dumpglob.dump_modref loc mp "mod"; mp
   with
     | Not_found -> 
 	Modops.error_not_a_modtype_loc loc (string_of_qualid qid)
diff --git a/interp/modintern.mli b/interp/modintern.mli
index c14b6481e..1f27e3c18 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -26,6 +26,3 @@ val interp_modtype : env -> module_type_ast -> module_struct_entry
 val interp_modexpr : env -> module_ast -> module_struct_entry
 
 val lookup_module : qualid located -> module_path
-
-val dump_moddef : loc -> module_path -> string -> unit
-val dump_modref : loc -> module_path -> string -> unit
diff --git a/kernel/names.ml b/kernel/names.ml
index 975390cb9..3d80ad23e 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -86,6 +86,7 @@ type label = string
 
 type mod_self_id = uniq_ident
 let make_msid = make_uid
+let repr_msid (n, id, dp) = (n, id, dp)
 let debug_string_of_msid = debug_string_of_uid
 let refresh_msid (_,s,dir) = make_uid dir s
 let string_of_msid = string_of_uid
@@ -94,6 +95,7 @@ let label_of_msid (_,s,_) = s
 
 type mod_bound_id = uniq_ident
 let make_mbid = make_uid
+let repr_mbid (n, id, dp) = (n, id, dp)
 let debug_string_of_mbid = debug_string_of_uid
 let string_of_mbid = string_of_uid
 let id_of_mbid (_,s,_) = s
@@ -116,7 +118,7 @@ type module_path =
   | MPdot of module_path * label
 
 let rec string_of_mp = function
-  | MPfile sl -> string_of_dirpath sl
+  | MPfile sl -> "MPfile (" ^ string_of_dirpath sl ^ ")"
   | MPbound uid -> string_of_uid uid
   | MPself uid -> string_of_uid uid
   | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
diff --git a/kernel/names.mli b/kernel/names.mli
index b19f93e2d..177768cf4 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -48,6 +48,7 @@ type mod_self_id
 (* The first argument is a file name - to prevent conflict between 
    different files *)
 val make_msid : dir_path -> string -> mod_self_id
+val repr_msid : mod_self_id -> int * string * dir_path
 val id_of_msid : mod_self_id -> identifier
 val label_of_msid : mod_self_id -> label
 val refresh_msid : mod_self_id -> mod_self_id
@@ -58,6 +59,7 @@ val string_of_msid : mod_self_id -> string
 type mod_bound_id
 
 val make_mbid : dir_path -> string -> mod_bound_id
+val repr_mbid : mod_bound_id -> int * string * dir_path
 val id_of_mbid : mod_bound_id -> identifier
 val label_of_mbid : mod_bound_id -> label
 val debug_string_of_mbid : mod_bound_id -> string
@@ -82,7 +84,6 @@ type module_path =
   | MPdot of module_path * label
 (*i  | MPapply of module_path * module_path    in the future (maybe) i*)
 
-
 val string_of_mp : module_path -> string
 
 module MPset : Set.S with type elt = module_path
diff --git a/lib/flags.ml b/lib/flags.ml
index 68e287f69..f2ab87b4b 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -86,23 +86,6 @@ let is_unsafe s = Stringset.mem s !unsafe_set
 
 let noglob = ref false
 let dump = ref false
-let dump_file = ref ""
-let dump_into_file f = dump := true; dump_file := f
-
-let dump_buffer = Buffer.create 8192
-
-let dump_string = Buffer.add_string dump_buffer
-
-let dump_it () = 
-  if !dump then begin
-    let mode = [Open_wronly; Open_creat] in
-    let c = open_out_gen mode 0o666 !dump_file in
-    output_string c (Buffer.contents dump_buffer);
-    Buffer.clear dump_buffer;
-    close_out c
-  end
-
-let _ = at_exit dump_it
 
 (* Flags.for the virtual machine *)
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 08f9a279d..4cab30381 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -61,9 +61,6 @@ val is_unsafe : string -> bool
 
 val noglob : bool ref
 val dump : bool ref
-val dump_into_file : string -> unit
-val dump_string : string -> unit
-val dump_it : unit -> unit
 
 (* Options for the virtual machine *)
 
diff --git a/library/lib.ml b/library/lib.ml
index 5e22c4d22..bb0ad74ca 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 03498f5d9..80ce26fc6 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 2f74fe92b..272f01f7d 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. *)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index a4933a896..0d5d27538 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -441,7 +441,7 @@ let add_hints local dbnames0 h =
             (str "Cannot coerce" ++ spc () ++ pr_global gr ++ spc () ++
              str "to an evaluable reference")
         in
-	  if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr;
+	  if !Flags.dump then Dumpglob.add_glob (loc_of_reference r) gr;
 	 (gr,r') in
       add_unfolds (List.map f lhints) local dbnames
   | HintsConstructors lqid ->
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index ab23f2210..e4d464236 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -238,7 +238,9 @@ let firstchar =
 let identchar = 
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' 
      '\'' '0'-'9']
-let ident = firstchar identchar*
+let id = firstchar identchar*
+let pfx_id = (id '.')*
+let ident = id | pfx_id id
 
 let begin_hide = "(*" space* "begin" space+ "hide" space* "*)"
 let end_hide = "(*" space* "end" space+ "hide" space* "*)"
@@ -405,10 +407,11 @@ and module_refs = parse
       { module_refs lexbuf }
   | ident  
       { let id =  lexeme lexbuf in
-	  (try
-	      add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id
-	    with
-		Not_found -> ()
+	  (Printf.eprintf "DEBUG: id = %s\n" id; 
+	   try
+	     add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id
+	   with
+	       Not_found -> ()
 	  ); 
 	module_refs lexbuf }
   | eof    
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 0522bbac0..a75b7196d 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -417,17 +417,14 @@ module Html = struct
   let stop_verbatim () = printf "</pre>\n"
 
   let module_ref m s = 
-    printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
-    (*i
     match find_module m with
-    | Local ->
-	printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
-    | Coqlib when !externals ->
-	let m = Filename.concat !coqlib m in
-	printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
-    | Coqlib | Unknown ->
-	raw_ident s
-    i*)
+      | Local ->
+	  printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
+      | Coqlib when !externals ->
+	  let m = Filename.concat !coqlib m in
+	    printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
+      | Coqlib | Unknown ->
+	  raw_ident s
 
   let ident_ref m fid s = 
     match find_module m with
@@ -446,6 +443,7 @@ module Html = struct
       printf "</span>"
     end else 
       begin
+	Printf.eprintf "DEBUG: looking for (%s, %d)\n" !current_module loc;
 	try
 	  (match Index.find !current_module loc with
 	     | Def (fullid,_) -> 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index d78aabbf9..b2fa915b6 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -639,7 +639,7 @@ and notation_bol = parse
 
 and notation = parse
   | nl { Output.line_break(); notation_bol lexbuf }
-  | '"' { Output.char '"'; false }
+  | '"' { Output.char '"'}
   | token
       { let s = lexeme lexbuf in
 	  Output.symbol s; notation lexbuf }
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 30fee26a0..d07051b71 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -447,7 +447,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
 		  try 
 		    let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
 		    let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
-		      Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
+		      Dumpglob.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
 		      c :: props, rest'
 		  with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
 		([], props) k.cl_props
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 02044b2cf..83a4703a2 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -108,15 +108,11 @@ let add_compile verbose s =
   compile_list := (verbose,s) :: !compile_list
 let compile_files () =
   let init_state = States.freeze() in
-  let coqdoc_init_state = Constrintern.coqdoc_freeze () in
+  let coqdoc_init_state = Dumpglob.coqdoc_freeze () in
     List.iter
       (fun (v,f) ->
 	 States.unfreeze init_state;
-	 Constrintern.coqdoc_unfreeze coqdoc_init_state;
-	 if !Flags.noglob then
-	   Flags.dump := false
-	 else
-	   Flags.dump_into_file (f^".glob");
+	 Dumpglob.coqdoc_unfreeze coqdoc_init_state;
 	 if Flags.do_translate () then
 	   with_option translate_file (Vernac.compile v) f
 	 else
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index c0ec55228..d3c556147 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -126,7 +126,7 @@ let rec vernac_com interpfun (loc,com) =
         let cl = !Pp.comments in
         (* end translator state *)
         (* coqdoc state *)
-        let cds = Constrintern.coqdoc_freeze() in
+        let cds = Dumpglob.coqdoc_freeze() in
           if !Flags.translate_file then 
 	    begin
               let _,f = find_file_in_path (Library.get_load_paths ())
@@ -141,13 +141,13 @@ let rec vernac_com interpfun (loc,com) =
               chan_translate := ch;
               Lexer.restore_com_state cs;
               Pp.comments := cl;
-              Constrintern.coqdoc_unfreeze cds
+              Dumpglob.coqdoc_unfreeze cds
 	    with e -> 
 	      if !Flags.translate_file then close_out !chan_translate;
               chan_translate := ch;
               Lexer.restore_com_state cs;
               Pp.comments := cl;
-              Constrintern.coqdoc_unfreeze cds;
+              Dumpglob.coqdoc_unfreeze cds;
 	      raise e
 	  end
 	      
@@ -228,14 +228,15 @@ let compile verbosely f =
   let ldir,long_f_dot_v = Library.start_library f in
   let dumpstate = !Flags.dump in
     if not !Flags.noglob then
-      (Flags.dump_into_file (f ^ ".glob");
-       Flags.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"));
+      (Flags.dump := true; 
+       Dumpglob.open_glob_file f;
+       Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"));
     if !Flags.xml_export then !xml_start_library ();
     let _ = load_vernac verbosely long_f_dot_v in
      if Pfedit.get_all_proof_names () <> [] then
 	(message "Error: There are pending proofs"; exit 1);
       if !Flags.xml_export then !xml_end_library ();
-      if !Flags.dump then Flags.dump_it ();
+      if !Flags.dump then Dumpglob.close_glob_file ();
       Flags.dump := dumpstate;
       Library.save_library_to ldir (long_f_dot_v ^ "o")
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 2cea826a7..d1003bd83 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -275,7 +275,7 @@ let print_located_module r =
 
 let global_with_alias r =
   let gr = global_with_alias r in
-    if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr;
+    if !Flags.dump then Dumpglob.add_glob (loc_of_reference r) gr;
     gr
 
 (**********)
@@ -305,49 +305,31 @@ let start_proof_and_print k l hook =
   print_subgoals ();
   if !pcoq <> None then (Option.get !pcoq).start_proof ()
 
-let current_dirpath sec =
-  drop_dirpath_prefix (Lib.library_dp ()) 
-    (if sec then Lib.cwd () 
-      else extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()))
-    
-let dump_definition (loc, id) sec s =
-  Flags.dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (unloc loc)) 
-			(string_of_dirpath (current_dirpath sec)) (string_of_id id))
-    
-let dump_reference loc modpath ident ty =
-  dump_string (Printf.sprintf "R%d %s %s %s %s\n" 
-		  (fst (unloc loc)) (string_of_dirpath (Lib.library_dp ())) modpath ident ty)
-
-let dump_constraint ((loc, n), _, _) sec ty =
-  match n with
-    | Name id -> dump_definition (loc, id) sec ty
-    | Anonymous -> ()
-
-let vernac_definition (local,_,_ as k) (_,id as lid) def hook =
-  if !Flags.dump then dump_definition lid false "def";
-  match def with
-  | ProveBody (bl,t) ->   (* local binders, typ *)
-      if Lib.is_modtype () then
-	errorlabstrm "Vernacentries.VernacDefinition"
-	  (str "Proof editing mode not supported in module types")
-      else
-	let hook _ _ = () in
-	start_proof_and_print (local,DefinitionBody Definition)
-                             [Some lid,(bl,t)] hook
-  | DefineBody (bl,red_option,c,typ_opt) ->
-      let red_option = match red_option with
-        | None -> None
-        | Some r -> 
-	    let (evc,env)= Command.get_current_context () in
-	    Some (interp_redexp env evc r) in
-      declare_definition id k bl red_option c typ_opt hook
-
+let vernac_definition (local,_,_ as k) (loc,id as lid) def hook =
+  if !Flags.dump then Dumpglob.dump_definition lid false "def";
+  (match def with
+    | ProveBody (bl,t) ->   (* local binders, typ *)
+ 	if Lib.is_modtype () then
+ 	  errorlabstrm "Vernacentries.VernacDefinition"
+ 	    (str "Proof editing mode not supported in module types")
+ 	else
+ 	  let hook _ _ = () in
+ 	    start_proof_and_print (local,DefinitionBody Definition) 
+	      [Some lid, (bl,t)] hook
+    | DefineBody (bl,red_option,c,typ_opt) ->
+ 	let red_option = match red_option with
+          | None -> None
+          | Some r -> 
+ 	      let (evc,env)= Command.get_current_context () in
+ 		Some (interp_redexp env evc r) in
+ 	  declare_definition id k bl red_option c typ_opt hook)
+ 	      
 let vernac_start_proof kind l lettop hook =
   if !Flags.dump then
     List.iter (fun (id, _) -> 
       match id with
-      | Some lid -> dump_definition lid false "prf"
-      | None -> ()) l;
+	| Some lid -> Dumpglob.dump_definition lid false "prf"
+	| None -> ()) l;
   if not(refining ()) then
     if lettop then
       errorlabstrm "Vernacentries.StartProof"
@@ -381,28 +363,28 @@ let vernac_exact_proof c =
   	
 let vernac_assumption kind l nl=
   let global = fst kind = Global in
-  List.iter (fun (is_coe,(idl,c)) -> 
-    if !dump then
-      List.iter (fun lid -> 
-	if global then dump_definition lid false "ax" 
-	else dump_definition lid true "var") idl;
-    declare_assumption idl is_coe kind [] c false false nl) l
-
+    List.iter (fun (is_coe,(idl,c)) -> 
+      if !dump then
+	List.iter (fun lid -> 
+	  if global then Dumpglob.dump_definition lid false "ax" 
+	  else Dumpglob.dump_definition lid true "var") idl;
+      declare_assumption idl is_coe kind [] c false false nl) l
+      
 let vernac_inductive f indl = 
   if !dump then
     List.iter (fun ((lid, _, _, cstrs), _) ->
-      dump_definition lid false"ind";
+      Dumpglob.dump_definition lid false"ind";
       List.iter (fun (_, (lid, _)) ->
-	dump_definition lid false "constr") cstrs)
+	Dumpglob.dump_definition lid false "constr") cstrs)
       indl;
   build_mutual indl f
 
 let vernac_fixpoint l b = 
-  List.iter (fun ((lid, _, _, _, _), _) -> dump_definition lid false "def") l;
+  List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
   build_recursive l b
 
 let vernac_cofixpoint l b =
-  List.iter (fun ((lid, _, _, _), _) -> dump_definition lid false "def") l;
+  List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
   build_corecursive l b
 
 let vernac_scheme = build_scheme
@@ -413,9 +395,11 @@ let vernac_combined_scheme = build_combined_scheme
 (* Modules            *)
 
 let vernac_import export refl =
-  let import ref = Library.import_module export (qualid_of_reference ref) in
-  List.iter import refl;
-  Lib.add_frozen_state ()
+  let import ref = 
+    Library.import_module export (qualid_of_reference ref)
+  in
+    List.iter import refl;
+    Lib.add_frozen_state ()
 
 let vernac_declare_module export (loc, id) binders_ast mty_ast_o = 
   (* We check the state of the system (in section, in module type)
@@ -433,9 +417,9 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast_o =
     Modintern.interp_modtype Modintern.interp_modexpr
     id binders_ast (Some mty_ast_o) None
   in 
-  Modintern.dump_moddef loc mp "mod";
-  if_verbose message ("Module "^ string_of_id id ^" is declared");
-  Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+    Dumpglob.dump_moddef loc mp "mod";
+    if_verbose message ("Module "^ string_of_id id ^" is declared");
+    Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
 
 let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = 
   (* We check the state of the system (in section, in module type)
@@ -453,7 +437,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
        let mp = Declaremods.start_module Modintern.interp_modtype export
 	 id binders_ast mty_ast_o 
        in
-	 Modintern.dump_moddef loc mp "mod";
+	 Dumpglob.dump_moddef loc mp "mod";
 	 if_verbose message 
 	   ("Interactive Module "^ string_of_id id ^" started") ;
          List.iter
@@ -473,7 +457,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
 	  Modintern.interp_modtype Modintern.interp_modexpr
 	  id binders_ast mty_ast_o mexpr_ast_o 
        in
-	 Modintern.dump_moddef loc mp "mod";
+	 Dumpglob.dump_moddef loc mp "mod";
 	 if_verbose message 
 	   ("Module "^ string_of_id id ^" is defined");
          Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)])
@@ -481,9 +465,9 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
 
 let vernac_end_module export (loc,id) =
   let mp = Declaremods.end_module id in
-  Modintern.dump_modref loc mp "mod";
-  if_verbose message ("Module "^ string_of_id id ^" is defined") ;
-  Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+    Dumpglob.dump_modref loc mp "mod";
+    if_verbose message ("Module "^ string_of_id id ^" is defined") ;
+    Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
 
 
 let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
@@ -499,7 +483,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
            (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast
              ([],[]) in
        let mp = Declaremods.start_modtype Modintern.interp_modtype id binders_ast in
-        Modintern.dump_moddef loc mp "modtype";
+        Dumpglob.dump_moddef loc mp "modtype";
 	if_verbose message 
 	  ("Interactive Module Type "^ string_of_id id ^" started");
         List.iter
@@ -509,25 +493,25 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
          ) argsexport
 	  
     | Some base_mty ->
-       let binders_ast = List.map
-        (fun (export,idl,ty) ->
-          if export <> None then
-           error ("Arguments of a functor definition can be imported only if" ^
-                  " the definition is interactive. Remove the \"Export\" " ^
-                  "and \"Import\" keywords from every functor argument.")
-          else (idl,ty)) binders_ast in
-       let mp = Declaremods.declare_modtype Modintern.interp_modtype 
+	let binders_ast = List.map
+          (fun (export,idl,ty) ->
+            if export <> None then
+              error ("Arguments of a functor definition can be imported only if" ^
+			" the definition is interactive. Remove the \"Export\" " ^
+			"and \"Import\" keywords from every functor argument.")
+            else (idl,ty)) binders_ast in
+	let mp = Declaremods.declare_modtype Modintern.interp_modtype 
 	  id binders_ast base_mty in
-        Modintern.dump_moddef loc mp "modtype";
-	if_verbose message 
-	  ("Module Type "^ string_of_id id ^" is defined")
+          Dumpglob.dump_moddef loc mp "modtype";
+	  if_verbose message 
+	    ("Module Type "^ string_of_id id ^" is defined")
 
 
 let vernac_end_modtype (loc,id) =
   let mp = Declaremods.end_modtype id in
-  Modintern.dump_modref loc mp "modtype";
-  if_verbose message 
-    ("Module Type "^ string_of_id id ^" is defined")
+    Dumpglob.dump_modref loc mp "modtype";
+    if_verbose message 
+      ("Module Type "^ string_of_id id ^" is defined")
 
 let vernac_include = function
   | CIMTE mty_ast ->
@@ -544,7 +528,7 @@ let vernac_record struc binders sort nameopt cfs =
   let const = match nameopt with 
     | None -> add_prefix "Build_" (snd (snd struc))
     | Some (_,id as lid) ->
-	if !dump then dump_definition lid false "constr"; id in
+	if !dump then Dumpglob.dump_definition lid false "constr"; id in
   let sigma = Evd.empty in
   let env = Global.env() in
   let s = interp_constr sigma env sort in
@@ -553,11 +537,11 @@ let vernac_record struc binders sort nameopt cfs =
     | Sort s -> s
     | _ -> user_err_loc
         (constr_loc sort,"definition_structure", str "Sort expected") in
-    if !dump then (
-      dump_definition (snd struc) false "rec";
+    if !Flags.dump then (
+      Dumpglob.dump_definition (snd struc) false "rec";
       List.iter (fun (_, x) ->
 	match x with
-	| AssumExpr ((loc, Name id), _) -> dump_definition (loc,id) false "proj"
+	| AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
 	| _ -> ()) cfs);
     ignore(Record.definition_structure (struc,binders,cfs,const,s))
 
@@ -565,13 +549,13 @@ let vernac_record struc binders sort nameopt cfs =
 
 let vernac_begin_section (_, id as lid) =
   check_no_pending_proofs ();
-  if !Flags.dump then dump_definition lid true "sec";
+  if !Flags.dump then Dumpglob.dump_definition lid true "sec";
   Lib.open_section id
 
 let vernac_end_section (loc, id) = 
   if !Flags.dump then 
-    dump_reference loc 
-      (string_of_dirpath (current_dirpath true)) "<>" "sec";
+    Dumpglob.dump_reference loc 
+      (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec";
   Lib.close_section id
 
 let vernac_end_segment lid =
@@ -586,7 +570,9 @@ let vernac_end_segment lid =
 
 let vernac_require import _ qidl =
   let qidl = List.map qualid_of_reference qidl in
-  Library.require_library qidl import
+  let modrefl = List.map (fun (_, qid) -> let (_, dp, _) = (Library.locate_qualified_library qid) in dp) qidl in
+    List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl modrefl;
+    Library.require_library qidl import
 
 let vernac_canonical r =
   Recordops.declare_canonical_structure (global_with_alias r)
@@ -605,21 +591,21 @@ let vernac_identity_coercion stre id qids qidt =
 
 (* Type classes *)
 let vernac_class id par ar sup props =
-  if !dump then (
-    dump_definition id false "class";
-    List.iter (fun (lid, _, _) -> dump_definition lid false "meth") props);
+  if !Flags.dump then (
+      Dumpglob.dump_definition id false "class";
+      List.iter (fun (lid, _, _) -> Dumpglob.dump_definition lid false "meth") props);
   Classes.new_class id par ar sup props
  
 let vernac_instance glob sup inst props pri =
-  if !dump then dump_constraint inst false "inst";
+  if !Flags.dump then Dumpglob.dump_constraint inst false "inst";
   ignore(Classes.new_instance ~global:glob sup inst props pri)
 
 let vernac_context l =
-  if !dump then List.iter (fun x -> dump_constraint x true "var") l;
+  if !Flags.dump then List.iter (fun x -> Dumpglob.dump_constraint x true "var") l;
   Classes.context l
 
 let vernac_declare_instance id =
-  if !dump then dump_definition id false "inst";
+  if !Flags.dump then Dumpglob.dump_definition id false "inst";
   Classes.declare_instance false id
 
 (***********)
@@ -754,7 +740,7 @@ let vernac_declare_tactic_definition = Tacinterp.add_tacdef
 let vernac_hints = Auto.add_hints
 
 let vernac_syntactic_definition lid =
-  dump_definition lid false "syndef";
+  Dumpglob.dump_definition lid false "syndef";
   Command.syntax_definition (snd lid)
   
 let vernac_declare_implicits local r = function