Move from ocamlweb to ocamdoc to generate mli documentation

dev/ocamlweb-doc has been erased. I hope no one still use the
"new-parse" it generate.

In dev/,
make html will generate in dev/html/ "clickable version of mlis". (as
the caml standard library)
make coq.pdf will generate nearly the same awfull stuff that coq.ps was.
make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of
the given directory.

ocamldoc comment syntax is here :
http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html

The possibility to put graphs in pdf/html seems to be lost.

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

1 files changed, 25 insertions, 23 deletions

diff --git a/library/library.mli b/library/library.mli
index c6bd8fe0b..05b213350 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -1,21 +1,20 @@
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
+(***********************************************************************
+    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        
+  ***********************************************************************)
 
 (*i $Id$ i*)
 
-(*i*)
 open Util
 open Names
 open Libnames
 open Libobject
-(*i*)
 
-(*s This module provides functions to load, open and save
+(** {6 Sect } *)
+(** This module provides functions to load, open and save
   libraries. Libraries correspond to the subclass of modules that
   coincide with a file on disk (the ".vo" files). Libraries on the
   disk comes with checksums (obtained with the [Digest] module), which
@@ -23,43 +22,46 @@ open Libobject
   written at various dates.
 *)
 
-(*s Require = load in the environment + open (if the optional boolean
+(** {6 Sect } *)
+(** Require = load in the environment + open (if the optional boolean
     is not [None]); mark also for export if the boolean is [Some true] *)
 val require_library : qualid located list -> bool option -> unit
 val require_library_from_dirpath : (dir_path * string) list -> bool option -> unit
 val require_library_from_file :
   identifier option -> System.physical_path -> bool option -> unit
 
-(*s Open a module (or a library); if the boolean is true then it's also
+(** {6 Sect } *)
+(** Open a module (or a library); if the boolean is true then it's also
    an export otherwise just a simple import *)
 val import_module : bool -> qualid located -> unit
 
-(*s Start the compilation of a library *)
+(** {6 Start the compilation of a library } *)
 val start_library : string -> dir_path * string
 
-(*s End the compilation of a library and save it to a ".vo" file *)
+(** {6 End the compilation of a library and save it to a ".vo" file } *)
 val save_library_to : dir_path -> string -> unit
 
-(*s Interrogate the status of libraries *)
+(** {6 Interrogate the status of libraries } *)
 
-  (* - Tell if a library is loaded or opened *)
+  (** - Tell if a library is loaded or opened *)
 val library_is_loaded : dir_path -> bool
 val library_is_opened : dir_path -> bool
 
-  (* - Tell which libraries are loaded or imported *)
+  (** - Tell which libraries are loaded or imported *)
 val loaded_libraries : unit -> dir_path list
 val opened_libraries : unit -> dir_path list
 
-  (* - Return the full filename of a loaded library. *)
+  (** - Return the full filename of a loaded library. *)
 val library_full_filename : dir_path -> string
 
-  (* - Overwrite the filename of all libraries (used when restoring a state) *)
+  (** - Overwrite the filename of all libraries (used when restoring a state) *)
 val overwrite_library_filenames : string -> unit
 
-(*s Hook for the xml exportation of libraries *)
+(** {6 Hook for the xml exportation of libraries } *)
 val set_xml_require : (dir_path -> unit) -> unit
 
-(*s Global load paths: a load path is a physical path in the file
+(** {6 Sect } *)
+(** Global load paths: a load path is a physical path in the file
     system; to each load path is associated a Coq [dir_path] (the "logical"
     path of the physical path) *)
 
@@ -70,7 +72,7 @@ val remove_load_path : System.physical_path -> unit
 val find_logical_path : System.physical_path -> dir_path
 val is_in_load_paths : System.physical_path -> bool
 
-(*s Locate a library in the load paths *)
+(** {6 Locate a library in the load paths } *)
 exception LibUnmappedDir
 exception LibNotFound
 type library_location = LibLoaded | LibInPath
@@ -79,5 +81,5 @@ val locate_qualified_library :
   bool -> qualid -> library_location * dir_path * System.physical_path
 val try_locate_qualified_library : qualid located -> dir_path * string
 
-(*s Statistics: display the memory use of a library. *)
+(** {6 Statistics: display the memory use of a library. } *)
 val mem : dir_path -> Pp.std_ppcmds