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

3 files changed, 45 insertions, 7 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