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, 53 insertions, 79 deletions

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 2fb2cb81c..c6cf8a751 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -1,30 +1,27 @@
-(************************************************************************)
-(*  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 Names
 open Univ
 open Term
 open Cemitcodes
 open Sign
 open Mod_subst
-(*i*)
 
-(* This module defines the internal representation of global
+(** This module defines the internal representation of global
    declarations. This includes global constants/axioms, mutual
    inductive definitions, modules and module types *)
 
 type engagement = ImpredicativeSet
 
-(**********************************************************************)
-(*s Representation of constants (Definition/Axiom)                    *)
+(** {6 Representation of constants (Definition/Axiom) } *)
 
 type polymorphic_arity = {
   poly_param_levels : universe option list;
@@ -41,7 +38,7 @@ val from_val : constr -> constr_substituted
 val force : constr_substituted -> constr
 
 type constant_body = {
-    const_hyps : section_context; (* New: younger hyp at top *)
+    const_hyps : section_context; (** New: younger hyp at top *)
     const_body : constr_substituted option;
     const_type : constant_type;
     const_body_code : to_patch_substituted;
@@ -52,8 +49,7 @@ type constant_body = {
 
 val subst_const_body : substitution -> constant_body -> constant_body
 
-(**********************************************************************)
-(*s Representation of mutual inductive types in the kernel            *)
+(** {6 Representation of mutual inductive types in the kernel } *)
 
 type recarg =
   | Norec
@@ -72,12 +68,12 @@ val recarg_length : wf_paths -> int -> int
 
 val subst_wf_paths : substitution -> wf_paths -> wf_paths
 
-(*
-\begin{verbatim}
+(**
+{% \begin{verbatim} %}
    Inductive I1 (params) : U1 := c11 : T11 | ... | c1p1 : T1p1
    ...
    with      In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn
-\end{verbatim}
+{% \end{verbatim} %}
 *)
 
 type monomorphic_inductive_arity = {
@@ -90,94 +86,72 @@ type inductive_arity =
 | Polymorphic of polymorphic_arity
 
 type one_inductive_body = {
+(** {8 Primitive datas } *)
 
-(* Primitive datas *)
+    mind_typename : identifier; (** Name of the type: [Ii] *)
 
- (* Name of the type: [Ii] *)
-    mind_typename : identifier;
+    mind_arity_ctxt : rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *)
 
- (* Arity context of [Ii] with parameters: [forall params, Ui] *)
-    mind_arity_ctxt : rel_context;
+    mind_arity : inductive_arity; (** Arity sort and original user arity if monomorphic *)
 
- (* Arity sort and original user arity if monomorphic *)
-    mind_arity : inductive_arity;
+    mind_consnames : identifier array; (** Names of the constructors: [cij] *)
 
- (* Names of the constructors: [cij] *)
-    mind_consnames : identifier array;
-
- (* Types of the constructors with parameters: [forall params, Tij],
-    where the Ik are replaced by de Bruijn index in the context
-    I1:forall params, U1 ..  In:forall params, Un *)
     mind_user_lc : types array;
+ (** Types of the constructors with parameters:  [forall params, Tij],
+     where the Ik are replaced by de Bruijn index in the
+     context I1:forall params, U1 ..  In:forall params, Un *)
 
-(* Derived datas *)
+(** {8 Derived datas } *)
 
- (* Number of expected real arguments of the type (no let, no params) *)
-    mind_nrealargs : int;
+    mind_nrealargs : int; (** Number of expected real arguments of the type (no let, no params) *)
 
- (* Length of realargs context (with let, no params) *)
-    mind_nrealargs_ctxt : int;
+    mind_nrealargs_ctxt : int; (** Length of realargs context (with let, no params) *)
 
- (* List of allowed elimination sorts *)
-    mind_kelim : sorts_family list;
+    mind_kelim : sorts_family list; (** List of allowed elimination sorts *)
 
- (* Head normalized constructor types so that their conclusion is atomic *)
-    mind_nf_lc : types array;
+    mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion is atomic *)
 
- (* Length of the signature of the constructors (with let, w/o params)
-    (not to be used in the kernel!) *)
     mind_consnrealdecls : int array;
+ (** Length of the signature of the constructors (with let, w/o params)
+    (not used in the kernel) *)
 
- (* Signature of recursive arguments in the constructors *)
-    mind_recargs : wf_paths;
+    mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *)
 
-(* Datas for bytecode compilation *)
+(** {8 Datas for bytecode compilation } *)
 
- (* number of constant constructor *)
-    mind_nb_constant : int;
+    mind_nb_constant : int; (** number of constant constructor *)
 
- (* number of no constant constructor *)
-    mind_nb_args : int;
+    mind_nb_args : int; (** number of no constant constructor *)
 
     mind_reloc_tbl :  Cbytecodes.reloc_table;
   }
 
 type mutual_inductive_body = {
 
-  (* The component of the mutual inductive block *)
-    mind_packets : one_inductive_body array;
+    mind_packets : one_inductive_body array;  (** The component of the mutual inductive block *)
 
-  (* Whether the inductive type has been declared as a record *)
-    mind_record : bool;
+    mind_record : bool;  (** Whether the inductive type has been declared as a record *)
 
-  (* Whether the type is inductive or coinductive *)
-    mind_finite : bool;
+    mind_finite : bool;  (** Whether the type is inductive or coinductive *)
 
-  (* Number of types in the block *)
-    mind_ntypes : int;
+    mind_ntypes : int;  (** Number of types in the block *)
 
-  (* Section hypotheses on which the block depends *)
-    mind_hyps : section_context;
+    mind_hyps : section_context;  (** Section hypotheses on which the block depends *)
 
-  (* Number of expected parameters *)
-    mind_nparams : int;
+    mind_nparams : int;  (** Number of expected parameters *)
 
-  (* Number of recursively uniform (i.e. ordinary) parameters *)
-    mind_nparams_rec : int;
+    mind_nparams_rec : int;  (** Number of recursively uniform (i.e. ordinary) parameters *)
 
-  (* The context of parameters (includes let-in declaration) *)
-    mind_params_ctxt : rel_context;
+    mind_params_ctxt : rel_context;  (** The context of parameters (includes let-in declaration) *)
 
-  (* Universes constraints enforced by the inductive declaration *)
-    mind_constraints : constraints;
+    mind_constraints : constraints;  (** Universes constraints enforced by the inductive declaration *)
 
   }
 
 val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body
 
-(**********************************************************************)
-(*s Modules: signature component specifications, module types, and
-  module declarations *)
+(** {6 Modules: signature component specifications, module types, and
+  module declarations } *)
 
 type structure_field_body =
   | SFBconst of constant_body
@@ -199,29 +173,29 @@ and with_declaration_body =
   | With_definition_body of  identifier list * constant_body
 
 and module_body =
-    {  (*absolute path of the module*)
+    {  (** absolute path of the module *)
       mod_mp : module_path;
-      (* Implementation *)
+      (** Implementation *)
       mod_expr : struct_expr_body option; 
-      (* Signature *)
+      (** Signature *)
       mod_type : struct_expr_body;
-      (* algebraic structure expression is kept 
+      (** algebraic structure expression is kept 
 	 if it's relevant for extraction  *)
       mod_type_alg : struct_expr_body option; 
-      (* set of all constraint in the module  *)
+      (** set of all constraint in the module  *)
       mod_constraints : constraints;
-      (* quotiented set of equivalent constant and inductive name  *)
+      (** quotiented set of equivalent constant and inductive name  *)
       mod_delta : delta_resolver;
       mod_retroknowledge : Retroknowledge.action list}
       
 and module_type_body =
     { 
-      (*Path of the module type*)
+      (** Path of the module type *)
       typ_mp : module_path;
       typ_expr : struct_expr_body;
-      (* algebraic structure expression is kept 
+      (** algebraic structure expression is kept 
 	 if it's relevant for extraction  *)
       typ_expr_alg : struct_expr_body option ;
       typ_constraints : constraints;
-      (* quotiented set of equivalent constant and inductive name  *)
+      (** quotiented set of equivalent constant and inductive name  *)
       typ_delta :delta_resolver}