Fix setoid_rewrite documentation examples.

Debug handling of identifiers in coqdoc (should work with modules and
sections) and add missing macros.
Move theories/Program to THEORIESVO to put the files in the standard
library documentation.


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

14 files changed, 138 insertions, 85 deletions

diff --git a/COMPATIBILITY b/COMPATIBILITY
index 7ddc33d47f..1595445293 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -22,7 +22,8 @@ Tactics
 - Add Relation and Add Morphism on polymorphic relations should now be
   declared with Add Parametric Relation and Add Parametric Morphism.
 
-- Some bug fixes may lead to incompatibilities.
+- Some bug fixes may lead to incompatibilities (see CHANGES for a detailed
+  account).
 
 Libraries
 
diff --git a/Makefile.build b/Makefile.build
index 8a6bf2df4e..f2385dc443 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -892,7 +892,7 @@ else
 endif
 %.ml4.d: $(D_DEPEND_BEFORE_SRC) %.ml4
 	$(SHOW)'CAMLP4DEPS $<'
-	$(HIDE)( echo -n '$*.cmo $*.cmx $*.ml4.ml.d $*.ml4-preprocessed: $(SEP)' && $(CAMLP4DEPS) "$<" ) > "$@" \
+	$(HIDE)( /bin/echo -n '$*.cmo $*.cmx $*.ml4.ml.d $*.ml4-preprocessed: $(SEP)' && $(CAMLP4DEPS) "$<" ) > "$@" \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
 %.ml4.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml4 $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILES:.ml4=.ml) %.ml4.d
diff --git a/Makefile.common b/Makefile.common
index b90cdbc0f0..42197c98d6 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -735,11 +735,16 @@ CLASSESVO:=$(addprefix theories/Classes/, \
  Morphisms_Relations.vo	Functions.vo 	Equivalence.vo  SetoidTactics.vo  \
  SetoidClass.vo 	SetoidAxioms.vo EquivDec.vo 	SetoidDec.vo )
 
+PROGRAMVO:=$(addprefix theories/Program/, \
+ Tactics.vo 	Equality.vo 	Subset.vo	Utils.vo 	\
+ Wf.vo 		Basics.vo	FunctionalExtensionality.vo 	\
+ Combinators.vo	Syntax.vo 	Program.vo )
+
 THEORIESVO:=\
   $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \
   $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) \
   $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO)  $(SORTINGVO) $(QARITHVO) \
-  $(NUMBERSVO) $(UNICODEVO) $(CLASSESVO)
+  $(NUMBERSVO) $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO)
 
 THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(ARITHVO)
 
@@ -799,17 +804,12 @@ CCVO:=
 DPVO:=$(addprefix contrib/dp/, \
  Dp.vo )
 
-SUBTACVO:=$(addprefix theories/Program/, \
- Tactics.vo 	Equality.vo 	Subset.vo	Utils.vo 	\
- Wf.vo 		Basics.vo	FunctionalExtensionality.vo 	\
- Combinators.vo	Syntax.vo 	Program.vo )
-
 RTAUTOVO:=$(addprefix contrib/rtauto/, \
  Bintree.vo	Rtauto.vo )
 
 CONTRIBVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
 	    $(XMLVO) $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) \
-	    $(SUBTACVO) $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO)
+	    $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO)
 
 ALLVO:= $(INITVO) $(THEORIESVO) $(CONTRIBVO)
 VFILES:= $(ALLVO:.vo=.v)
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index d2b6d11516..ba847562e5 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -623,10 +623,13 @@ Reset Initial.
 Require Import Setoid.
 \end{coq_eval}
 \begin{coq_example}
-Instance {A : Type} => all_iff_morphism : 
+Instance all_iff_morphism (A : Type) :
   Morphism (pointwise_relation iff ==> iff) (@all A).
 Proof. simpl_relation. 
 \end{coq_example}
+\begin{coq_eval}
+Admitted.
+\end{coq_eval}
 
 One then has to show that if two predicates are equivalent at every
 point, their universal quantifications are equivalent. Once we have
@@ -653,12 +656,13 @@ Inductive list_equiv {A:Type} (eqA : relation A) : relation (list A) :=
   forall l l', list_equiv eqA l l' -> list_equiv eqA (x :: l) (y :: l').
 \end{coq_eval}
 \begin{coq_example*}
-Instance [ Equivalence A eqA, Equivalence B eqB ] => 
+Instance map_morphism [ Equivalence A eqA, Equivalence B eqB ] :
   Morphism ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) 
      (@map A B).
 \end{coq_example*}
 
-where \texttt{list\_equiv} implements an equivalence on lists.
+where \texttt{list\_equiv} implements an equivalence on lists
+parameterized by an equivalence on the elements.
 
 Note that when one does rewriting with a lemma under a binder
 using \texttt{setoid\_rewrite}, the application of the lemma may capture
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index c86338175e..48dbb3f01c 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -438,12 +438,16 @@ through the <tt>Require Import</tt> command.</p>
     Support for dependently-typed programming.
   </dt>
   <dd> 
+    theories/Program/Basics.v
     theories/Program/Wf.v
+    theories/Program/Subset.v
     theories/Program/Equality.v
     theories/Program/Tactics.v
     theories/Program/Utils.v
+    theories/Program/Syntax.v
     theories/Program/Program.v
     theories/Program/FunctionalExtensionality.v
+    theories/Program/Combinators.v
   </dd>
 
 </dl>
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 283dc269d5..b867bfd69a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -191,31 +191,56 @@ let type_of_global_ref gr =
 	  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 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_string (Printf.sprintf "R%d %s %s %s %s\n" 
+		    (fst (unloc 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 mod_dp,id = repr_path sp in
-  let mod_dp_trunc =  drop_dirpath_prefix lib_dp mod_dp in
-  let filepath = string_of_dirpath lib_dp in
-  let fullname = string_of_qualid (make_qualid mod_dp_trunc id) in
   let ty = type_of_global_ref ref in
-    dump_string (Printf.sprintf "R%d %s %s %s\n" 
-		    (fst (unloc loc)) filepath fullname ty)
-
+    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 dp, id = repr_path sp in
-  let fullname = string_of_id id in
-  let filepath = string_of_dirpath dp in
-    dump_string (Printf.sprintf "R%d %s %s syndef\n" (fst (unloc loc)) filepath fullname)
+  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 =
@@ -473,7 +498,7 @@ let intern_applied_reference intern env lvar args = function
       let r,args2 = intern_qualid loc qid intern env args in
       find_appl_head_data lvar r, args2
   | Ident (loc, id) ->
-      try intern_var env lvar loc id,args
+      try intern_var env lvar loc id, args
       with Not_found -> 
       let qid = make_short_qualid id in
       try
diff --git a/library/lib.mli b/library/lib.mli
index f3fa9a4b37..03498f5d99 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -131,6 +131,7 @@ val end_compilation : dir_path -> object_prefix * library_segment
 val library_dp : unit -> 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
 
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index a5e560c891..6a61a16d45 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -21,19 +21,21 @@ Definition id {A} := fun x : A => x.
 
 (** Function composition. *)
 
-Definition compose {A B C} (g : B -> C) (f : A -> B) := fun x : A => g (f x).
+Definition compose {A B C} (g : B -> C) (f : A -> B) := 
+  fun x : A => g (f x).
 
 Hint Unfold compose.
 
-Notation " g ∘ f " := (compose g f)  (at level 40, left associativity) : program_scope.
+Notation " g ∘ f " := (compose g f)  
+  (at level 40, left associativity) : program_scope.
 
 Open Local Scope program_scope.
 
-(** [arrow A B] represents the non-dependent function space between [A] and [B]. *)
+(** The non-dependent function space between [A] and [B]. *)
 
 Definition arrow (A B : Type) := A -> B.
 
-(** [impl A B] represents the logical implication of [B] by [A]. *)
+(** Logical implication. *)
 
 Definition impl (A B : Prop) : Prop := A -> B.
 
@@ -45,7 +47,7 @@ Definition const {A B} (a : A) := fun _ : B => a.
 
 Definition flip {A B C} (f : A -> B -> C) x y := f y x.
 
-(** [apply f x] simply applies [f] to [x]. *)
+(** Application as a combinator. *)
 
 Definition apply {A B} (f : A -> B) (x : A) := f x.
 
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index d8cc333367..ca3e08f7fa 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -63,8 +63,8 @@
 }
 
 \usepackage{hyperref}
+\hypersetup{colorlinks=true,linkcolor=black}
 %\usepackage{color}
-%\hypersetup{colorlinks=true,linkcolor=black}
 %\usepackage{multind}
 %\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{\index{coq}{#1@#2|hyperpage}#3}}
 
@@ -79,7 +79,10 @@
 \newcommand{\coqdefinition}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
 \newcommand{\coqdefinitionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
 
-\newcommand{\coqvariable}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}}
+%\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}}}
@@ -108,6 +111,8 @@
 \newcommand{\coqprojection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
 \newcommand{\coqprojectionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
 
+\newcommand{\coqnotationref}[2]{\coqref{#1}{\coqdockw{#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 9f0c3d24a9..ec04017c44 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -60,6 +60,8 @@ type 'a index = {
   idx_entries : (char * (string * 'a) list) list;
   idx_size : int }
 
+val current_library : string ref
+
 val all_entries : unit -> 
       (coq_module * entry_type) index *
       (entry_type * coq_module index) list
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index fa619a9434..1fa7c2498b 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -44,16 +44,20 @@ type index_entry =
 
 let current_type = ref Library
 let current_library = ref ""
-  (** referes to the file being parsed *)
+  (** refers to the file being parsed *)
 
 let table = Hashtbl.create 97
   (** [table] is used to store references and definitions *)
 
-let add_def loc ty id = Hashtbl.add table (!current_library, loc) (Def (id, ty))
-
-let add_ref m loc m' id ty = 
-  Hashtbl.add table (m, loc) (Ref (m', id, ty))
+let full_ident sp id =
+  if sp <> "<>" then sp ^ "." ^ id else id
+    
+let add_def loc ty sp id = 
+  Hashtbl.add table (!current_library, loc) (Def (full_ident sp id, ty))
 
+let add_ref m loc m' sp id ty = 
+  Hashtbl.add table (m, loc) (Ref (m', full_ident sp id, ty))
+    
 let add_mod m loc m' id = Hashtbl.add table (m, loc) (Mod (m', id))
 
 let find m l = Hashtbl.find table (m, l)
@@ -288,7 +292,7 @@ and index_ident = parse
 	      | Lemma -> make_fullid id
 	      | _ -> id 
 	in 
-	  add_def (lexeme_start lexbuf) !current_type fullid }
+	  add_def (lexeme_start lexbuf) !current_type "" fullid }
   | eof    
       { () }
   | _      
@@ -300,7 +304,7 @@ and index_idents = parse
   | space+ | ','
       { index_idents lexbuf }
   | ident  
-      { add_def (lexeme_start lexbuf) !current_type (lexeme lexbuf);
+      { add_def (lexeme_start lexbuf) !current_type "" (lexeme lexbuf);
 	index_idents lexbuf }
   | eof    
       { () }
@@ -380,7 +384,7 @@ and module_ident = parse
       { () }
   | ident
       { let id = lexeme lexbuf in
-	  begin_module id; add_def (lexeme_start lexbuf) !current_type id }
+	  begin_module id; add_def (lexeme_start lexbuf) !current_type "" id }
   | eof
       { () }
   | _
@@ -439,13 +443,13 @@ and module_refs = parse
 		current_library := !cur_mod
 	    | 'R' ->
 		(try
-		    Scanf.sscanf s "R%d %s %s %s"
-		      (fun loc lib_dp full_id ty ->
-			add_ref !cur_mod loc lib_dp full_id (type_of_string ty))
+		    Scanf.sscanf s "R%d %s %s %s %s"
+		      (fun loc lib_dp sp id ty ->
+			add_ref !cur_mod loc lib_dp sp id (type_of_string ty))
 		  with _ -> ())
 	    | _ -> 
-		try Scanf.sscanf s "%s %d %s"
-		  (fun ty loc id -> add_def loc (type_of_string ty) id)
+		try Scanf.sscanf s "%s %d %s %s"
+		  (fun ty loc sp id -> add_def loc (type_of_string ty) sp id)
 		with Scanf.Scan_failure _ -> ()
 	end
       done; assert false
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 251fb23571..5b68e94cca 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -36,7 +36,7 @@ let is_keyword =
       "CoInductive"; "Defined"; "Definition"; "End"; "Eval"; "Example"; 
       "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
       "Hypothesis"; "Hypotheses"; 
-      "Immediate"; "Implicit"; "Import"; "Inductive"; 
+      "Resolve"; "Unfold"; "Immediate"; "Implicit"; "Import"; "Inductive"; 
       "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; 
       "Module"; "Module Type"; "Declare Module"; "Include";
       "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed";
@@ -46,18 +46,15 @@ let is_keyword =
       "Notation"; "Reserved Notation"; "Tactic Notation";
       "Delimit"; "Bind"; "Open"; "Scope";
       "Boxed"; "Unboxed";
-      "Arguments";
-      "Instance"; "Class"; "Instantiation";
+      "Arguments"; 
+      "Typeclasses"; "Instance"; "Class"; "Instantiation";
       (* Program *)
       "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
       "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
       "Program Instance";
-      (*i (* correctness *)
-      "array"; "assert"; "begin"; "do"; "done"; "else"; "end"; "if";
-      "in"; "invariant"; "let"; "of"; "ref"; "state"; "then"; "variant";
-      "while"; i*)
       (*i (* coq terms *) *)
-	"match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="
+	"match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; 
+	"if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"
        ]
 
 let is_tactic = 
@@ -65,9 +62,12 @@ let is_tactic =
     [ "intro"; "intros"; "apply"; "rewrite"; "setoid_rewrite";
       "destruct"; "induction"; "elim"; "dependent"; 
       "generalize"; "clear"; "rename"; "move"; "set"; "assert";
-      "cut"; "assumption"; "exact";
-      "unfold"; "red"; "compute"; "at"; "in"; "by";
-      "reflexivity"; "symmetry"; "transitivity" ]
+      "cut"; "assumption"; "exact"; "split"; "try"; "discriminate";
+      "simpl"; "unfold"; "red"; "compute"; "at"; "in"; "by";
+      "reflexivity"; "symmetry"; "transitivity";
+      "replace"; "setoid_replace"; "inversion"; "pattern";
+      "trivial"; "exact"; "tauto"; "firstorder"; "ring";
+      "clapply"; "program_simpl"; "eapply"; "auto"; "eauto" ]
 
 (*s Current Coq module *)
 
@@ -94,6 +94,7 @@ let remove_printing_token = Hashtbl.remove token_pp
 let _ = List.iter 
 	  (fun (s,l) -> Hashtbl.add token_pp s (Some l, None))
 	  [ "*" ,  "\\ensuremath{\\times}";
+	    "|", "\\ensuremath{|}";
 	    "->",  "\\ensuremath{\\rightarrow}";
 	    "->~",  "\\ensuremath{\\rightarrow\\lnot}";
 	    "->~~",  "\\ensuremath{\\rightarrow\\lnot\\lnot}";
@@ -246,8 +247,6 @@ module Latex = struct
   let ident s loc = 
     if is_keyword s then begin
       printf "\\coqdockw{"; raw_ident s; printf "}"
-    end else if is_tactic s then begin
-      printf "\\coqdoctac{"; raw_ident s; printf "}"
     end else begin
       begin
 	try
@@ -261,7 +260,9 @@ module Latex = struct
 	     | Mod _ ->
 		 printf "\\coqdocid{"; raw_ident s; printf "}")
 	with Not_found ->
-	  printf "\\coqdocvar{"; raw_ident s; printf "}"
+	  if is_tactic s then begin
+	    printf "\\coqdoctac{"; raw_ident s; printf "}"
+	  end else begin printf "\\coqdocvar{"; raw_ident s; printf "}" end
       end
     end
 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 2e0f46795a..a9ad92f4c7 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -661,6 +661,7 @@ and printing_token_body = parse
 
   let coq_file f m =
     reset ();
+    Index.current_library := m;
     Output.start_module ();
     let c = open_in f in
     let lb = from_channel c in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 30d993256f..b63c59d93f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -300,20 +300,22 @@ let start_proof_and_print k l hook =
   print_subgoals ();
   if !pcoq <> None then (Option.get !pcoq).start_proof ()
 
-let dump_definition (loc, id) s =
-  Flags.dump_string (Printf.sprintf "%s %d %s\n" s (fst (unloc loc)) (string_of_id id))
-
-let dump_variable (loc, id) s = ()
-(*   Flags.dump_string (Printf.sprintf "%s %d %s\n" s (fst (unloc loc)) *)
-(* 			(string_of_kn (Lib.make_kn id))) *)
-
-let dump_constraint ty ((loc, n), _, _) =
+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_constraint ((loc, n), _, _) sec ty =
   match n with
-    | Name id -> dump_definition (loc, id) ty
+    | 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 "def";
+  if !Flags.dump then dump_definition lid false "def";
   match def with
   | ProveBody (bl,t) ->   (* local binders, typ *)
       if Lib.is_modtype () then
@@ -335,7 +337,7 @@ let vernac_start_proof kind l lettop hook =
   if !Flags.dump then
     List.iter (fun (id, _) -> 
       match id with
-      | Some lid -> dump_definition lid "prf"
+      | Some lid -> dump_definition lid false "prf"
       | None -> ()) l;
   if not(refining ()) then
     if lettop then
@@ -372,25 +374,26 @@ 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 "ax" else
-	  dump_variable lid "var") idl;
+      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
 
 let vernac_inductive f indl = 
   if !dump then
     List.iter (fun ((lid, _, _, cstrs), _) ->
-      dump_definition lid "ind";
+      dump_definition lid false"ind";
       List.iter (fun (_, (lid, _)) ->
-	dump_definition lid "constr") cstrs)
+	dump_definition lid false "constr") cstrs)
       indl;
   build_mutual indl f
 
 let vernac_fixpoint l b = 
-  List.iter (fun ((lid, _, _, _, _), _) -> dump_definition lid "def") l;
+  List.iter (fun ((lid, _, _, _, _), _) -> dump_definition lid false "def") l;
   build_recursive l b
 
 let vernac_cofixpoint l b =
-  List.iter (fun ((lid, _, _, _), _) -> dump_definition lid "def") l;
+  List.iter (fun ((lid, _, _, _), _) -> dump_definition lid false "def") l;
   build_corecursive l b
 
 let vernac_scheme = build_scheme
@@ -522,7 +525,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 "constr"; id in
+	if !dump then 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
@@ -532,10 +535,10 @@ let vernac_record struc binders sort nameopt cfs =
     | _ -> user_err_loc
         (constr_loc sort,"definition_structure", str "Sort expected") in
     if !dump then (
-      dump_definition (snd struc) "rec";
+      dump_definition (snd struc) false "rec";
       List.iter (fun (_, x) ->
 	match x with
-	| AssumExpr ((loc, Name id), _) -> dump_definition (loc,id) "proj"
+	| AssumExpr ((loc, Name id), _) -> dump_definition (loc,id) false "proj"
 	| _ -> ()) cfs);
     ignore(Record.definition_structure (struc,binders,cfs,const,s))
 
@@ -579,20 +582,20 @@ let vernac_identity_coercion stre id qids qidt =
 (* Type classes *)
 let vernac_class id par ar sup props =
   if !dump then (
-    dump_definition id "class";
-    List.iter (fun (lid, _, _) -> dump_definition lid "meth") props);
+    dump_definition id false "class";
+    List.iter (fun (lid, _, _) -> 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" inst;
+  if !dump then dump_constraint inst false "inst";
   ignore(Classes.new_instance ~global:glob sup inst props pri)
 
 let vernac_context l =
-  if !dump then List.iter (dump_constraint "var") l;
+  if !dump then List.iter (fun x -> dump_constraint x true "var") l;
   Classes.context l
 
 let vernac_declare_instance id =
-  if !dump then dump_definition id "inst";
+  if !dump then dump_definition id false "inst";
   Classes.declare_instance false id
 
 (***********)
@@ -727,7 +730,7 @@ let vernac_declare_tactic_definition = Tacinterp.add_tacdef
 let vernac_hints = Auto.add_hints
 
 let vernac_syntactic_definition lid =
-  dump_definition lid "syndef";
+  dump_definition lid false "syndef";
   Command.syntax_definition (snd lid)
 
 let vernac_declare_implicits local r = function