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

diff --git a/kernel/vm.mli b/kernel/vm.mli
index 5ecc8d99c..ff76e7cd5 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -8,10 +8,11 @@ val set_drawinstr : unit -> unit
 
 val transp_values : unit -> bool
 val set_transp_values : bool -> unit
-(* le code machine *)
+
+(** le code machine *)
 type tcode
 
-(* Les valeurs ***********)
+(** Les valeurs ***********)
 
 type vprod
 type vfun
@@ -26,11 +27,11 @@ type atom =
   | Aiddef of id_key * values
   | Aind of inductive
 
-(* Les zippers *)
+(** Les zippers *)
 
 type zipper =
   | Zapp of arguments
-  | Zfix of vfix*arguments  (* Peut-etre vide *)
+  | Zfix of vfix*arguments  (** Peut-etre vide *)
   | Zswitch of vswitch
 
 type stack = zipper list
@@ -64,42 +65,42 @@ external val_of_annot_switch : annot_switch -> values = "%identity"
 (** Destructors *)
 val whd_val : values -> whd
 
-(* Arguments *)
+(** Arguments *)
 val nargs : arguments -> int
 val arg : arguments -> int -> values
 
-(* Product *)
+(** Product *)
 val dom : vprod -> values
 val codom : vprod -> vfun
 
-(* Function *)
+(** Function *)
 val body_of_vfun : int -> vfun -> values
 val decompose_vfun2  : int -> vfun -> vfun -> int * values * values
 
-(* Fix *)
+(** Fix *)
 val current_fix : vfix -> int
 val check_fix : vfix -> vfix -> bool
 val rec_args : vfix -> int array
 val reduce_fix : int -> vfix -> vfun array * values array
-                              (* bodies ,  types *)
+                              (** bodies ,  types *)
 
-(* CoFix *)
+(** CoFix *)
 val current_cofix : vcofix -> int
 val check_cofix : vcofix -> vcofix -> bool
 val reduce_cofix : int -> vcofix -> values array * values array
-                                      (* bodies , types *)
-(* Block *)
+                                      (** bodies , types 
+   Block *)
 val btag : vblock -> int
 val bsize : vblock -> int
 val bfield : vblock -> int -> values
 
-(* Switch *)
+(** Switch *)
 val check_switch : vswitch -> vswitch -> bool
 val case_info : vswitch -> case_info
 val type_of_switch : vswitch -> values
 val branch_of_switch : int -> vswitch -> (int * values) array
 
-(* Evaluation *)
+(** Evaluation *)
 val whd_stack : values -> stack -> whd
 val force_whd : values -> stack -> whd