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, 24 insertions, 15 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 0bb74f74a6..bb6d947c54 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 717fddf793..1f7f6ada0a 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 e53c0cd1a1..c014865fe5 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 ()