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, 21 insertions, 22 deletions

diff --git a/lib/pp.mli b/lib/pp.mli
index 66d9bfa674..6ddfa6fc9c 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -1,30 +1,28 @@
-(************************************************************************)
-(*  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 Pp_control
-(*i*)
 
-(* Modify pretty printing functions behavior for emacs ouput (special
+(** Modify pretty printing functions behavior for emacs ouput (special
    chars inserted at some places). This function should called once in
    module [Options], that's all. *)
 val make_pp_emacs:unit -> unit
 val make_pp_nonemacs:unit -> unit
 
-(* Pretty-printers. *)
+(** Pretty-printers. *)
 
 type ppcmd
 
 type std_ppcmds = ppcmd Stream.t
 
-(*s Formatting commands. *)
+(** {6 Formatting commands. } *)
 
 val str  : string -> std_ppcmds
 val stras : int * string -> std_ppcmds
@@ -40,11 +38,11 @@ val ismt : std_ppcmds -> bool
 val comment : int -> std_ppcmds
 val comments : ((int * int) * string) list ref
 
-(*s Concatenation. *)
+(** {6 Concatenation. } *)
 
 val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds
 
-(*s Derived commands. *)
+(** {6 Derived commands. } *)
 
 val spc : unit -> std_ppcmds
 val cut : unit -> std_ppcmds
@@ -59,7 +57,7 @@ val strbrk : string -> std_ppcmds
 
 val xmlescape : ppcmd -> ppcmd
 
-(*s Boxing commands. *)
+(** {6 Boxing commands. } *)
 
 val h : int -> std_ppcmds -> std_ppcmds
 val v : int -> std_ppcmds -> std_ppcmds
@@ -67,7 +65,7 @@ val hv : int -> std_ppcmds -> std_ppcmds
 val hov : int -> std_ppcmds -> std_ppcmds
 val t : std_ppcmds -> std_ppcmds
 
-(*s Opening and closing of boxes. *)
+(** {6 Opening and closing of boxes. } *)
 
 val hb : int -> std_ppcmds
 val vb : int -> std_ppcmds
@@ -77,7 +75,7 @@ val tb : unit -> std_ppcmds
 val close : unit -> std_ppcmds
 val tclose : unit -> std_ppcmds
 
-(*s Pretty-printing functions \emph{without flush}. *)
+(** {6 Pretty-printing functions {% \emph{%}without flush{% }%}. } *)
 
 val pp_with : Format.formatter -> std_ppcmds -> unit
 val ppnl_with : Format.formatter -> std_ppcmds -> unit
@@ -87,28 +85,29 @@ val pp_flush_with : Format.formatter -> unit -> unit
 
 val set_warning_function : (Format.formatter -> std_ppcmds -> unit) -> unit
 
-(*s Pretty-printing functions \emph{with flush}. *)
+(** {6 Pretty-printing functions {% \emph{%}with flush{% }%}. } *)
 
 val msg_with : Format.formatter -> std_ppcmds -> unit
 val msgnl_with : Format.formatter -> std_ppcmds -> unit
 
 
-(*s The following functions are instances of the previous ones on
+(** {6 Sect } *)
+(** The following functions are instances of the previous ones on
   [std_ft] and [err_ft]. *)
 
-(*s Pretty-printing functions \emph{without flush} on [stdout] and [stderr]. *)
+(** {6 Pretty-printing functions {% \emph{%}without flush{% }%} on [stdout] and [stderr]. } *)
 
 val pp : std_ppcmds -> unit
 val ppnl : std_ppcmds -> unit
 val pperr : std_ppcmds -> unit
 val pperrnl : std_ppcmds -> unit
-val message : string -> unit       (* = pPNL *)
+val message : string -> unit       (** = pPNL *)
 val warning : string -> unit
 val warn : std_ppcmds -> unit
 val pp_flush : unit -> unit
 val flush_all: unit -> unit
 
-(*s Pretty-printing functions \emph{with flush} on [stdout] and [stderr]. *)
+(** {6 Pretty-printing functions {% \emph{%}with flush{% }%} on [stdout] and [stderr]. } *)
 
 val msg : std_ppcmds -> unit
 val msgnl : std_ppcmds -> unit