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, 27 insertions, 28 deletions

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 8fe8eb11f..7f2b08844 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -1,24 +1,22 @@
-(************************************************************************)
-(*  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 Declarations
 open Environ
-(*i*)
 
-(*s Extracting an inductive type from a construction *)
+(** {6 Extracting an inductive type from a construction } *)
 
-(* [find_m*type env sigma c] coerce [c] to an recursive type (I args).
+(** [find_m*type env sigma c] coerce [c] to an recursive type (I args).
    [find_rectype], [find_inductive] and [find_coinductive]
    respectively accepts any recursive type, only an inductive type and
    only a coinductive type.
@@ -30,31 +28,32 @@ val find_coinductive : env -> types -> inductive * constr list
 
 type mind_specif = mutual_inductive_body * one_inductive_body
 
-(*s Fetching information in the environment about an inductive type.
+(** {6 Sect } *)
+(** Fetching information in the environment about an inductive type.
     Raises [Not_found] if the inductive type is not found. *)
 val lookup_mind_specif : env -> inductive -> mind_specif
 
-(*s Functions to build standard types related to inductive *)
+(** {6 Functions to build standard types related to inductive } *)
 val ind_subst : mutual_inductive -> mutual_inductive_body -> constr list
 
 val type_of_inductive : env -> mind_specif -> types
 
 val elim_sorts : mind_specif -> sorts_family list
 
-(* Return type as quoted by the user *)
+(** Return type as quoted by the user *)
 val type_of_constructor : constructor -> mind_specif -> types
 
-(* Return constructor types in normal form *)
+(** Return constructor types in normal form *)
 val arities_of_constructors : inductive -> mind_specif -> types array
 
-(* Return constructor types in user form *)
+(** Return constructor types in user form *)
 val type_of_constructors : inductive -> mind_specif -> types array
 
-(* Transforms inductive specification into types (in nf) *)
+(** Transforms inductive specification into types (in nf) *)
 val arities_of_specif : mutual_inductive -> mind_specif -> types array
 
 
-(* [type_case_branches env (I,args) (p:A) c] computes useful types
+(** [type_case_branches env (I,args) (p:A) c] computes useful types
    about the following Cases expression:
       <p>Cases (c :: (I args)) of b1..bn end
    It computes the type of every branch (pattern variables are
@@ -69,20 +68,20 @@ val build_branches_type :
   inductive -> mutual_inductive_body * one_inductive_body ->
     constr list -> constr -> types array
 
-(* Return the arity of an inductive type *)
+(** Return the arity of an inductive type *)
 val mind_arity : one_inductive_body -> rel_context * sorts_family
 
 val inductive_sort_family : one_inductive_body -> sorts_family
 
-(* Check a [case_info] actually correspond to a Case expression on the
+(** Check a [case_info] actually correspond to a Case expression on the
    given inductive type. *)
 val check_case_info : env -> inductive -> case_info -> unit
 
-(*s Guard conditions for fix and cofix-points. *)
+(** {6 Guard conditions for fix and cofix-points. } *)
 val check_fix : env -> fixpoint -> unit
 val check_cofix : env -> cofixpoint -> unit
 
-(*s Support for sort-polymorphic inductive types *)
+(** {6 Support for sort-polymorphic inductive types } *)
 
 val type_of_inductive_knowing_parameters :
   env -> one_inductive_body -> types array -> types
@@ -92,8 +91,8 @@ val max_inductive_sort : sorts array -> universe
 val instantiate_universes : env -> rel_context ->
     polymorphic_arity -> types array -> rel_context * sorts
 
-(***************************************************************)
-(* Debug *)
+(**************************************************************
+   Debug *)
 
 type size = Large | Strict
 type subterm_spec =
@@ -102,13 +101,13 @@ type subterm_spec =
   | Not_subterm
 type guard_env =
   { env     : env;
-    (* dB of last fixpoint *)
+    (** dB of last fixpoint *)
     rel_min : int;
-    (* inductive of recarg of each fixpoint *)
+    (** inductive of recarg of each fixpoint *)
     inds    : inductive array;
-    (* the recarg information of inductive family *)
+    (** the recarg information of inductive family *)
     recvec  : wf_paths array;
-    (* dB of variables denoting subterms *)
+    (** dB of variables denoting subterms *)
     genv    : subterm_spec Lazy.t list;
   }