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, 31 insertions, 32 deletions

diff --git a/toplevel/command.mli b/toplevel/command.mli
index 48fc5a8eb..904a1a034 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -1,14 +1,13 @@
-(************************************************************************)
-(*  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 Term
@@ -21,19 +20,19 @@ open Decl_kinds
 open Redexpr
 open Constrintern
 open Pfedit
-(*i*)
 
-(*s This file is about the interpretation of raw commands into typed
+(** {6 Sect } *)
+(** This file is about the interpretation of raw commands into typed
     ones and top-level declaration of the main Gallina objects *)
 
-(* Hooks for Pcoq *)
+(** Hooks for Pcoq *)
 
 val set_declare_definition_hook : (definition_entry -> unit) -> unit
 val get_declare_definition_hook : unit -> (definition_entry -> unit)
 val set_declare_assumptions_hook : (types -> unit) -> unit
 
-(*************************************************************************)
-(* Definitions/Let *)
+(************************************************************************
+   Definitions/Let *)
 
 val interp_definition :
   boxed_flag -> local_binder list -> red_expr option -> constr_expr ->
@@ -42,24 +41,24 @@ val interp_definition :
 val declare_definition : identifier -> locality * definition_object_kind ->
   definition_entry -> manual_implicits -> declaration_hook -> unit
 
-(*************************************************************************)
-(* Parameters/Assumptions *)
+(************************************************************************
+   Parameters/Assumptions *)
 
 val interp_assumption :
   local_binder list -> constr_expr -> types * manual_implicits
 
 val declare_assumption : coercion_flag -> assumption_kind -> types ->
   manual_implicits ->
-  bool (* implicit *) -> bool (* inline *) -> variable located -> unit
+  bool (** implicit *) -> bool (* inline *) -> variable located -> unit
 
 val declare_assumptions : variable located list ->
   coercion_flag -> assumption_kind -> types -> manual_implicits ->
   bool -> bool -> unit
 
-(*************************************************************************)
-(* Inductive and coinductive types *)
+(************************************************************************
+   Inductive and coinductive types *)
 
-(* Extracting the semantical components out of the raw syntax of mutual
+(** Extracting the semantical components out of the raw syntax of mutual
    inductive declarations *)
 
 type structured_one_inductive_expr = {
@@ -75,30 +74,30 @@ val extract_mutual_inductive_declaration_components :
   (one_inductive_expr * decl_notation list) list ->
     structured_inductive_expr * (*coercions:*) qualid list * decl_notation list
 
-(* Typing mutual inductive definitions *)
+(** Typing mutual inductive definitions *)
 
 type one_inductive_impls =
-  Impargs.manual_explicitation list (* for inds *)*
-  Impargs.manual_explicitation list list (* for constrs *)
+  Impargs.manual_explicitation list (** for inds *)*
+  Impargs.manual_explicitation list list (** for constrs *)
 
 val interp_mutual_inductive :
   structured_inductive_expr -> decl_notation list -> bool ->
     mutual_inductive_entry * one_inductive_impls list
 
-(* Registering a mutual inductive definition together with its
+(** Registering a mutual inductive definition together with its
    associated schemes *)
 
 val declare_mutual_inductive_with_eliminations :
   bool -> mutual_inductive_entry -> one_inductive_impls list ->
   mutual_inductive
 
-(* Entry points for the vernacular commands Inductive and CoInductive *)
+(** Entry points for the vernacular commands Inductive and CoInductive *)
 
 val do_mutual_inductive :
   (one_inductive_expr * decl_notation list) list -> bool -> unit
 
-(*************************************************************************)
-(* Fixpoints and cofixpoints *)
+(************************************************************************
+   Fixpoints and cofixpoints *)
 
 type structured_fixpoint_expr = {
   fix_name : identifier;
@@ -107,19 +106,19 @@ type structured_fixpoint_expr = {
   fix_type : constr_expr
 }
 
-(* Extracting the semantical components out of the raw syntax of
+(** Extracting the semantical components out of the raw syntax of
    (co)fixpoints declarations *)
 
 val extract_fixpoint_components :
   (fixpoint_expr * decl_notation list) list ->
     structured_fixpoint_expr list * decl_notation list *
-    (* possible structural arg: *) lident option list
+    (** possible structural arg: *) lident option list
 
 val extract_cofixpoint_components :
   (cofixpoint_expr * decl_notation list) list ->
     structured_fixpoint_expr list * decl_notation list
 
-(* Typing global fixpoints and cofixpoint_expr *)
+(** Typing global fixpoints and cofixpoint_expr *)
 
 type recursive_preentry =
   identifier list * constr option list * types list
@@ -132,7 +131,7 @@ val interp_cofixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
     recursive_preentry * (int * manual_implicits) list
 
-(* Registering fixpoints and cofixpoints in the environment *)
+(** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
   bool -> recursive_preentry * (int * manual_implicits) list -> 
@@ -142,7 +141,7 @@ val declare_cofixpoint :
   bool -> recursive_preentry * (int * manual_implicits) list ->
     decl_notation list -> unit
 
-(* Entry points for the vernacular commands Fixpoint and CoFixpoint *)
+(** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint :
   (fixpoint_expr * decl_notation list) list -> bool -> unit
@@ -150,7 +149,7 @@ val do_fixpoint :
 val do_cofixpoint :
   (cofixpoint_expr * decl_notation list) list -> bool -> unit
 
-(* Utils *)
+(** Utils *)
 
 val check_mutuality : Environ.env -> bool -> (identifier * types) list -> unit