Enhancements to coqdoc, better globalization of sections and modules.

Minor fix in Morphisms which prevented working with higher-order
morphisms and PER relations.


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

14 files changed, 206 insertions, 93 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b867bfd69..ac4639b43 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -161,9 +161,9 @@ let type_of_logical_kind = function
       | Method -> "meth")
   | IsAssumption a ->
       (match a with
-      | Definitional -> "def"
-      | Logical -> "prf"
-      | Conjectural -> "prf")
+      | Definitional -> "defax"
+      | Logical -> "prfax"
+      | Conjectural -> "prfax")
   | IsProof th ->
       (match th with
       | Theorem
@@ -200,6 +200,10 @@ let remove_sections dir =
     (* 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
@@ -207,8 +211,7 @@ let add_glob_gen loc sp lib_dp ty =
   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)
+    dump_reference loc filepath modpath ident ty
 
 let add_glob loc ref = 
   let sp = Nametab.sp_of_global ref in
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 68978080b..cd55ec74d 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -60,19 +60,51 @@ 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 fp = string_of_dirpath dp 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.
 *)
 let lookup_module (loc,qid) =
   try
-    Nametab.locate_module qid
+    let mp = Nametab.locate_module qid in
+      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
-    Nametab.locate_modtype qid
+    let mp = Nametab.locate_modtype qid in
+      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 1f27e3c18..c14b6481e 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -26,3 +26,6 @@ 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/library/declaremods.ml b/library/declaremods.ml
index 0bb74f74a..bb6d947c5 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -663,7 +663,7 @@ let start_module interp_modtype export id args res_o =
     openmod_info:=(mbids,res_entry_o,sub_body_o);
   let prefix = Lib.start_module export id mp fs in
   Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
-  Lib.add_frozen_state ()
+  Lib.add_frozen_state (); mp
 
 
 let end_module id =
@@ -717,7 +717,8 @@ let end_module id =
     if mp_of_kn (snd newoname) <> mp then 
       anomaly "Kernel and Library names do not match";
 
-    Lib.add_frozen_state () (* to prevent recaching *)
+    Lib.add_frozen_state () (* to prevent recaching *);
+    mp
 
 
 
@@ -819,7 +820,7 @@ let start_modtype interp_modtype id args =
   openmodtype_info := mbids;
   let prefix = Lib.start_modtype id mp fs in
   Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix);
-  Lib.add_frozen_state ()
+  Lib.add_frozen_state (); mp
 
 
 let end_modtype id =
@@ -843,14 +844,15 @@ let end_modtype id =
     anomaly
       "Kernel and Library names do not match";
 
-  Lib.add_frozen_state ()(* to prevent recaching *)
+  Lib.add_frozen_state ()(* to prevent recaching *);
+  ln
 
 
 let declare_modtype interp_modtype id args mty = 
   let fs = Summary.freeze_summaries () in
 
   try
-  let _ = Global.start_modtype id in
+  let mmp = Global.start_modtype id in
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
 
   let base_mty = interp_modtype (Global.env()) mty in
@@ -865,7 +867,8 @@ let declare_modtype interp_modtype id args mty =
   (* and declare the module type as a whole *)
   Summary.unfreeze_summaries fs;
     
-  ignore (add_leaf id (in_modtype (Some entry, substobjs)))
+  ignore (add_leaf id (in_modtype (Some entry, substobjs)));
+  mmp
   with e ->
     (* Something wrong: undo the whole process *)
     Summary.unfreeze_summaries fs; raise e
@@ -1017,7 +1020,7 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
   let fs = Summary.freeze_summaries () in
 
   try
-  let _ = Global.start_module id in
+  let mmp = Global.start_module id in
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
 
   let mty_entry_o, mty_sub_o = match mty_o with
@@ -1073,7 +1076,8 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
 		    | _ -> None in
 	   ignore (add_leaf
 		     id
-		     (in_module_alias (Some (entry, mty_sub_o), substobjs, substituted)))
+		     (in_module_alias (Some (entry, mty_sub_o), substobjs, substituted)));
+	   mmp
       | _ ->
 	  let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
 	  let (sub,mbids,msid,objs) = substobjs in
@@ -1082,7 +1086,8 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
 	  let substituted = subst_substobjs dir mp substobjs in
 	    ignore (add_leaf
 		      id
-		      (in_module (Some (entry, mty_sub_o), substobjs, substituted)))
+		      (in_module (Some (entry, mty_sub_o), substobjs, substituted)));
+	    mmp
 	      
   with e -> 
     (* Something wrong: undo the whole process *)
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 717fddf79..1f7f6ada0 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -40,25 +40,25 @@ val declare_module :
   (env -> 'modtype -> module_struct_entry) -> (env -> 'modexpr -> module_struct_entry) ->
   identifier -> 
   (identifier located list * 'modtype) list -> ('modtype * bool) option -> 
-  'modexpr option -> unit
+  'modexpr option -> module_path
  
 val start_module : (env -> 'modtype -> module_struct_entry) -> 
   bool option -> identifier -> (identifier located list * 'modtype) list ->
-   ('modtype * bool) option -> unit
+   ('modtype * bool) option -> module_path
 
-val end_module : identifier -> unit
+val end_module : identifier -> module_path
 
 
 
 (*s Module types *)
 
 val declare_modtype : (env -> 'modtype -> module_struct_entry) -> 
-  identifier -> (identifier located list * 'modtype) list -> 'modtype -> unit
+  identifier -> (identifier located list * 'modtype) list -> 'modtype -> module_path
 
 val start_modtype : (env -> 'modtype -> module_struct_entry) -> 
-  identifier -> (identifier located list * 'modtype) list -> unit
+  identifier -> (identifier located list * 'modtype) list -> module_path
 
-val end_modtype : identifier -> unit
+val end_modtype : identifier -> module_path
 
 
 (*s Objects of a module. They come in two lists: the substitutive ones
diff --git a/library/library.ml b/library/library.ml
index e53c0cd1a..c014865fe 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -536,6 +536,10 @@ let require_library qidl 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;
   add_frozen_state ()
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index e9424ed0c..e41bebea1 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -432,16 +432,17 @@ let add_hints local dbnames0 h =
       add_trivials env sigma (List.map f lhints) local dbnames
   | HintsUnfold lhints ->
       let f r =
-	let r = Syntax_def.global_with_alias r in
-        let r' = match r with
+	let gr = Syntax_def.global_with_alias r in
+        let r' = match gr with
          | ConstRef c -> EvalConstRef c
          | VarRef c -> EvalVarRef c
          | _ -> 
            errorlabstrm "evalref_of_ref"
-            (str "Cannot coerce" ++ spc () ++ pr_global r ++ spc () ++
+            (str "Cannot coerce" ++ spc () ++ pr_global gr ++ spc () ++
              str "to an evaluable reference")
         in
-	 (r,r') in
+	  if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr;
+	 (gr,r') in
       add_unfolds (List.map f lhints) local dbnames
   | HintsConstructors lqid ->
       let add_one qid =
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index cd38f318c..6885d0b29 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -336,7 +336,7 @@ Proof. firstorder. Qed.
 
 (** [R] is Reflexive, hence we can build the needed proof. *)
 
-Lemma Reflexive_partial_app_morphism [ Morphism (A -> B) (R ==> R') m, Reflexive A R ] (x : A) :
+Lemma Reflexive_partial_app_morphism [ Morphism (A -> B) (R ==> R') m, MorphismProxy A R x ] :
    Morphism R' (m x).
 Proof. simpl_relation. Qed.
 
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index d22398166..c5a8f3d30 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -131,7 +131,7 @@ Implicit Arguments setoid_morphism [[!sa]].
 Existing Instance setoid_morphism.
 
 Program Definition setoid_partial_app_morphism [ sa : Setoid A ] (x : A) : Morphism (equiv ++> iff) (equiv x) :=
-  Reflexive_partial_app_morphism x.
+  Reflexive_partial_app_morphism.
 
 Existing Instance setoid_partial_app_morphism.
 
@@ -148,7 +148,7 @@ Ltac obligations_tactic ::= morphism_tac.
    using [iff_impl_id_morphism] if the proof is in [Prop] and
    [eq_arrow_id_morphism] if it is in Type. *)
 
-Program Instance iff_impl_id_morphism : Morphism (iff ++> impl) id.
+Program Instance iff_impl_id_morphism : Morphism (iff ++> impl) Basics.id.
 
 (* Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. *)
 
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index ca3e08f7f..ca454d852 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -44,6 +44,13 @@
 % macro for typesetting constant identifiers
 \newcommand{\coqdoccst}[1]{\textsf{#1}}
 
+% macro for typesetting module identifiers
+\newcommand{\coqdocmod}[1]{\textsc{\textsf{#1}}}
+
+% macro for typesetting module constant identifiers (e.g. Parameters in
+% module types)
+\newcommand{\coqdocax}[1]{\textsl{\textsf{#1}}}
+
 % macro for typesetting inductive type identifiers
 \newcommand{\coqdocind}[1]{\textbf{\textsf{#1}}}
 
@@ -62,13 +69,15 @@
 \newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{}
 }
 
-\usepackage{hyperref}
-\hypersetup{colorlinks=true,linkcolor=black}
+\usepackage[pdftex]{hyperref}
+\hypersetup{raiselinks=true,colorlinks=true,linkcolor=black}
+\usepackage[all]{hypcap}
+\usepackage{xr}
 %\usepackage{color}
 %\usepackage{multind}
 %\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{\index{coq}{#1@#2|hyperpage}#3}}
 
-\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{#3}}
+\newcommand{\coqdef}[3]{\phantomsection\hypertarget{coq:#1}{#3}}
 \newcommand{\coqref}[2]{\hyperlink{coq:#1}{#2}}
 
 \newcommand{\coqdocvar}[1]{{\textit{#1}}}
@@ -82,7 +91,6 @@
 %\newcommand{\coqvariable}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}}
 %\newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}}
 \newcommand{\coqvariable}[2]{\coqdocid{#2}}
-\newcommand{\coqaxiom}[2]{\coqdocid{#2}}
 
 \newcommand{\coqinductive}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
 \newcommand{\coqinductiveref}[2]{\coqref{#1}{\coqdocind{#2}}}
@@ -113,6 +121,25 @@
 
 \newcommand{\coqnotationref}[2]{\coqref{#1}{\coqdockw{#2}}}
 
+\newcommand{\coqsection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqsectionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+%\newcommand{\coqlibrary}[2]{\chapter{Library \coqdoccst{#2}}\label{coq:#1}}
+  
+%\newcommand{\coqlibraryref}[2]{\ref{coq:#1}}
+
+\newcommand{\coqlibrary}[2]{\cleardoublepage\phantomsection
+  \hypertarget{coq:#1}{\chapter{Library \coqdoccst{#2}}}}
+  
+\newcommand{\coqlibraryref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+\newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocax{#2}}}
+\newcommand{\coqaxiomref}[2]{\coqref{#1}{\coqdocax{#2}}}
+
+\newcommand{\coqmodule}[2]{\coqdef{#1}{#2}{\coqdocmod{#2}}}
+\newcommand{\coqmoduleref}[2]{\coqref{#1}{\coqdocmod{#2}}}
+
+
 %HEVEA\newcommand{\lnot}{\coqwkw{not}}
 %HEVEA\newcommand{\lor}{\coqwkw{or}}
 %HEVEA\newcommand{\land}{\&}
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index ec04017c4..9831ca3cb 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -29,6 +29,7 @@ type entry_type =
   | TacticDefinition
   | Abbreviation
   | Notation
+  | Section
 
 val type_name : entry_type -> string
 
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index 1fa7c2498..ab23f2210 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -36,6 +36,7 @@ type entry_type =
   | TacticDefinition
   | Abbreviation
   | Notation
+  | Section
 
 type index_entry = 
   | Def of string * entry_type
@@ -50,7 +51,13 @@ let table = Hashtbl.create 97
   (** [table] is used to store references and definitions *)
 
 let full_ident sp id =
-  if sp <> "<>" then sp ^ "." ^ id else id
+  if sp <> "<>" then 
+    if id <> "<>" then 
+      sp ^ "." ^ id 
+    else sp 
+  else if id <> "<>" 
+  then id 
+  else ""
     
 let add_def loc ty sp id = 
   Hashtbl.add table (!current_library, loc) (Def (full_ident sp id, ty))
@@ -195,7 +202,8 @@ let type_name = function
   | TacticDefinition -> "tactic"
   | Abbreviation -> "abbreviation"
   | Notation -> "notation"
-      
+  | Section -> "section"
+
 let all_entries () =
   let gl = ref [] in
   let add_g s m t = gl := (s,(m,t)) :: !gl in
@@ -421,14 +429,15 @@ and module_refs = parse
     | "meth" -> Method
     | "inst" -> Instance
     | "var" -> Variable
-    | "ax" -> Axiom
+    | "defax" | "prfax" | "ax" -> Axiom
     | "syndef" -> Abbreviation
     | "not" -> Notation
+    | "lib" -> Library
+    | "mod" | "modtype" -> Module
+    | "tac" -> TacticDefinition
+    | "sec" -> Section
     | s -> raise (Invalid_argument ("type_of_string:" ^ s))
-(*   | Library *)
-(*   | Module *)
-(*   | TacticDefinition *)
-
+	
   let read_glob f = 
     let c = open_in f in
     let cur_mod = ref "" in
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 5b68e94cc..009e4dd11 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -36,17 +36,17 @@ let is_keyword =
       "CoInductive"; "Defined"; "Definition"; "End"; "Eval"; "Example"; 
       "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
       "Hypothesis"; "Hypotheses"; 
-      "Resolve"; "Unfold"; "Immediate"; "Implicit"; "Import"; "Inductive"; 
+      "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive"; 
       "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; 
       "Module"; "Module Type"; "Declare Module"; "Include";
       "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed";
       "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
-      "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
+      "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
       "Set"; "Unset"; "Variable"; "Variables"; 
       "Notation"; "Reserved Notation"; "Tactic Notation";
-      "Delimit"; "Bind"; "Open"; "Scope";
-      "Boxed"; "Unboxed";
-      "Arguments"; 
+      "Delimit"; "Bind"; "Open"; "Scope"; 
+      "Boxed"; "Unboxed"; "Inline";
+      "Arguments"; "Add"; "Strict";
       "Typeclasses"; "Instance"; "Class"; "Instantiation";
       (* Program *)
       "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
@@ -65,7 +65,8 @@ let is_tactic =
       "cut"; "assumption"; "exact"; "split"; "try"; "discriminate";
       "simpl"; "unfold"; "red"; "compute"; "at"; "in"; "by";
       "reflexivity"; "symmetry"; "transitivity";
-      "replace"; "setoid_replace"; "inversion"; "pattern";
+      "replace"; "setoid_replace"; "inversion"; "inversion_clear";
+      "pattern"; "intuition"; "congruence";
       "trivial"; "exact"; "tauto"; "firstorder"; "ring";
       "clapply"; "program_simpl"; "eapply"; "auto"; "eauto" ]
 
@@ -190,7 +191,9 @@ module Latex = struct
 
   let start_module () = 
     if not !short then begin
-      printf "\\coqdocmodule{"; 
+      printf "\\coqlibrary{"; 
+      label_ident !current_module; 
+      printf "}{";
       raw_ident !current_module; 
       printf "}\n\n"
     end
@@ -231,13 +234,14 @@ module Latex = struct
 	raw_ident s
     i*)
 
-  let ident_ref m fid typ s = 
+  let ident_ref m fid typ s =
+    let id = if fid <> "" then (m ^ "." ^ fid) else m in
     match find_module m with
       | Local ->
-	  printf "\\coq%sref{" (type_name typ); label_ident (m ^ "." ^ fid); printf "}{"; raw_ident s; printf "}"
+	  printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
       | Coqlib when !externals ->
 	  let _m = Filename.concat !coqlib m in
-	    printf "\\coq%sref{" (type_name typ); label_ident (m ^ "." ^ fid); printf "}{"; raw_ident s; printf "}"
+	    printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
       | Coqlib | Unknown ->
 	  raw_ident s
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b63c59d93..2cea826a7 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -273,6 +273,11 @@ let print_located_module r =
 	str "No module is referred to by name ") ++ pr_qualid qid
   in msgnl msg  
 
+let global_with_alias r =
+  let gr = global_with_alias r in
+    if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr;
+    gr
+
 (**********)
 (* Syntax *)
 
@@ -309,6 +314,10 @@ 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
@@ -408,7 +417,7 @@ let vernac_import export refl =
   List.iter import refl;
   Lib.add_frozen_state ()
 
-let vernac_declare_module export id binders_ast mty_ast_o = 
+let vernac_declare_module export (loc, id) binders_ast mty_ast_o = 
   (* We check the state of the system (in section, in module type)
      and what module information is supplied *)
   if Lib.sections_are_opened () then
@@ -420,13 +429,15 @@ let vernac_declare_module export id binders_ast mty_ast_o =
        "Remove the \"Export\" and \"Import\" keywords from every functor " ^
        "argument.")
      else (idl,ty)) binders_ast in
-  Declaremods.declare_module 
+  let mp = Declaremods.declare_module 
     Modintern.interp_modtype Modintern.interp_modexpr
-     id binders_ast (Some mty_ast_o) None;
+    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
 
-let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o = 
+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)
      and what module information is supplied *)
   if Lib.sections_are_opened () then
@@ -439,15 +450,17 @@ let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o =
          (fun (export,idl,ty) (args,argsexport) ->
            (idl,ty)::args, (List.map (fun (_,i) -> export,i)idl)@argsexport) binders_ast
              ([],[]) in
-	Declaremods.start_module Modintern.interp_modtype export
-	  id binders_ast mty_ast_o;
-	if_verbose message 
-	  ("Interactive Module "^ string_of_id id ^" started") ;
-        List.iter
-         (fun (export,id) ->
-           Option.iter
-            (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
-         ) argsexport
+       let mp = Declaremods.start_module Modintern.interp_modtype export
+	 id binders_ast mty_ast_o 
+       in
+	 Modintern.dump_moddef loc mp "mod";
+	 if_verbose message 
+	   ("Interactive Module "^ string_of_id id ^" started") ;
+         List.iter
+           (fun (export,id) ->
+             Option.iter
+               (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+           ) argsexport
     | Some _ ->
        let binders_ast = List.map
         (fun (export,idl,ty) ->
@@ -456,21 +469,24 @@ let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o =
                   " the definition is interactive. Remove the \"Export\" and " ^
                   "\"Import\" keywords from every functor argument.")
           else (idl,ty)) binders_ast in
-	Declaremods.declare_module 
+       let mp =	Declaremods.declare_module 
 	  Modintern.interp_modtype Modintern.interp_modexpr
-	  id binders_ast mty_ast_o mexpr_ast_o;
-	if_verbose message 
-	  ("Module "^ string_of_id id ^" is defined");
-        Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)])
-         export
-
-let vernac_end_module export id =
-  Declaremods.end_module id;
+	  id binders_ast mty_ast_o mexpr_ast_o 
+       in
+	 Modintern.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)])
+           export
+
+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
 
 
-let vernac_declare_module_type id binders_ast mty_ast_o =
+let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
   if Lib.sections_are_opened () then
     error "Modules and Module Types are not allowed inside sections";
   
@@ -482,7 +498,8 @@ let vernac_declare_module_type id binders_ast mty_ast_o =
          (fun (export,idl,ty) (args,argsexport) ->
            (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast
              ([],[]) in
-	Declaremods.start_modtype Modintern.interp_modtype id binders_ast;
+       let mp = Declaremods.start_modtype Modintern.interp_modtype id binders_ast in
+        Modintern.dump_moddef loc mp "modtype";
 	if_verbose message 
 	  ("Interactive Module Type "^ string_of_id id ^" started");
         List.iter
@@ -499,14 +516,16 @@ let vernac_declare_module_type id binders_ast mty_ast_o =
                   " the definition is interactive. Remove the \"Export\" " ^
                   "and \"Import\" keywords from every functor argument.")
           else (idl,ty)) binders_ast in
-	Declaremods.declare_modtype Modintern.interp_modtype 
-	  id binders_ast base_mty;
+       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")
 
 
-let vernac_end_modtype id =
-  Declaremods.end_modtype id;
+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")
 
@@ -544,20 +563,25 @@ let vernac_record struc binders sort nameopt cfs =
 
   (* Sections *)
 
-let vernac_begin_section id =
+let vernac_begin_section (_, id as lid) =
   check_no_pending_proofs ();
+  if !Flags.dump then dump_definition lid true "sec";
   Lib.open_section id
 
-let vernac_end_section = Lib.close_section
+let vernac_end_section (loc, id) = 
+  if !Flags.dump then 
+    dump_reference loc 
+      (string_of_dirpath (current_dirpath true)) "<>" "sec";
+  Lib.close_section id
 
-let vernac_end_segment id =
+let vernac_end_segment lid =
   check_no_pending_proofs ();
   let o = try Lib.what_is_opened () with 
       Not_found -> error "There is nothing to end." in
     match o with
-      | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export id
-      | _,Lib.OpenedModtype _ -> vernac_end_modtype id
-      | _,Lib.OpenedSection _ -> vernac_end_section id
+      | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export lid
+      | _,Lib.OpenedModtype _ -> vernac_end_modtype lid
+      | _,Lib.OpenedSection _ -> vernac_end_section lid
       | _ -> anomaly "No more opened things"
 
 let vernac_require import _ qidl =
@@ -732,7 +756,7 @@ let vernac_hints = Auto.add_hints
 let vernac_syntactic_definition lid =
   dump_definition lid false "syndef";
   Command.syntax_definition (snd lid)
-
+  
 let vernac_declare_implicits local r = function
   | Some imps ->
       Impargs.declare_manual_implicits local (global_with_alias r) false
@@ -1263,18 +1287,18 @@ let interp c = match c with
   | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
 
   (* Modules *)
-  | VernacDeclareModule (export,(_,id),bl,mtyo) -> 
-      vernac_declare_module export id bl mtyo
-  | VernacDefineModule (export,(_,id),bl,mtyo,mexpro) -> 
-      vernac_define_module export id bl mtyo mexpro
-  | VernacDeclareModuleType ((_,id),bl,mtyo) -> 
-      vernac_declare_module_type id bl mtyo
+  | VernacDeclareModule (export,lid,bl,mtyo) -> 
+      vernac_declare_module export lid bl mtyo
+  | VernacDefineModule (export,lid,bl,mtyo,mexpro) -> 
+      vernac_define_module export lid bl mtyo mexpro
+  | VernacDeclareModuleType (lid,bl,mtyo) -> 
+      vernac_declare_module_type lid bl mtyo
   | VernacInclude (in_ast) ->
       vernac_include in_ast
   (* Gallina extensions *)
-  | VernacBeginSection (_,id) -> vernac_begin_section id
+  | VernacBeginSection lid -> vernac_begin_section lid
 
-  | VernacEndSegment (_,id) -> vernac_end_segment id
+  | VernacEndSegment lid -> vernac_end_segment lid
 
   | VernacRecord (_,id,bl,s,idopt,fs) -> vernac_record id bl s idopt fs
   | VernacRequire (export,spec,qidl) -> vernac_require export spec qidl