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, 40 insertions, 48 deletions

diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 2533fc537..a97b85ed9 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.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
@@ -19,35 +18,32 @@ open Evarutil
 open Mod_subst
 open Rawterm
 open Unification
-(*i*)
 
-(***************************************************************)
-(* The Type of Constructions clausale environments. *)
+(** {6 The Type of Constructions clausale environments.} *)
 
-(* [env] is the typing context
- * [evd] is the mapping from metavar and evar numbers to their types
- *       and values.
- * [templval] is the template which we are trying to fill out.
- * [templtyp] is its type.
- *)
 type clausenv = {
-  env      : env;
-  evd      : evar_map;
-  templval : constr freelisted;
-  templtyp : constr freelisted }
-
-(* Substitution is not applied on templenv (because [subst_clenv] is
+  env      : env; (** the typing context *)
+  evd      : evar_map; (** the mapping from metavar and evar numbers to their 
+			   types and values *)
+  templval : constr freelisted; (** the template which we are trying to fill 
+				    out *)
+  templtyp : constr freelisted (** its type *)}
+
+(** Substitution is not applied on templenv (because [subst_clenv] is
    applied only on hints which typing env is overwritten by the
    goal env) *)
 val subst_clenv : substitution -> clausenv -> clausenv
 
-(* subject of clenv (instantiated) *)
+(** subject of clenv (instantiated) *)
 val clenv_value     : clausenv -> constr
-(* type of clenv (instantiated) *)
+
+(** type of clenv (instantiated) *)
 val clenv_type      : clausenv -> types
-(* substitute resolved metas *)
+
+(** substitute resolved metas *)
 val clenv_nf_meta   : clausenv -> constr -> constr
-(* type of a meta in clenv context *)
+
+(** type of a meta in clenv context *)
 val clenv_meta_type : clausenv -> metavariable -> types
 
 val mk_clenv_from : Goal.goal sigma -> constr * types -> clausenv
@@ -56,25 +52,23 @@ val mk_clenv_from_n :
 val mk_clenv_type_of : Goal.goal sigma -> constr -> clausenv
 val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv
 
-(***************************************************************)
-(* linking of clenvs *)
+(** {6 linking of clenvs } *)
 
 val connect_clenv : Goal.goal sigma -> clausenv -> clausenv
 val clenv_fchain :
   ?allow_K:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
 
-(***************************************************************)
-(* Unification with clenvs *)
+(** {6 Unification with clenvs } *)
 
-(* Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *)
+(** Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *)
 val clenv_unify :
   bool -> ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
 
-(* unifies the concl of the goal with the type of the clenv *)
+(** unifies the concl of the goal with the type of the clenv *)
 val clenv_unique_resolver :
   bool -> ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
 
-(* same as above ([allow_K=false]) but replaces remaining metas
+(** same as above ([allow_K=false]) but replaces remaining metas
    with fresh evars if [evars_flag] is [true] *)
 val evar_clenv_unique_resolver :
   bool -> ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
@@ -83,12 +77,11 @@ val clenv_dependent : bool -> clausenv -> metavariable list
 
 val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
 
-(***************************************************************)
-(* Bindings *)
+(** {6 Bindings } *)
 
 type arg_bindings = constr explicit_bindings
 
-(* bindings where the key is the position in the template of the
+(** bindings where the key is the position in the template of the
    clenv (dependent or not). Positions can be negative meaning to
    start from the rightmost argument of the template. *)
 val clenv_independent : clausenv -> metavariable list
@@ -96,23 +89,23 @@ val clenv_missing : clausenv -> metavariable list
 
 val clenv_constrain_last_binding : constr -> clausenv -> clausenv
 
-(* defines metas corresponding to the name of the bindings *)
+(** defines metas corresponding to the name of the bindings *)
 val clenv_match_args : arg_bindings -> clausenv -> clausenv
 
 val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
 
-(* start with a clenv to refine with a given term with bindings *)
+(** start with a clenv to refine with a given term with bindings *)
 
-(* the arity of the lemma is fixed *)
-(* the optional int tells how many prods of the lemma have to be used *)
-(* use all of them if None *)
+(** the arity of the lemma is fixed 
+   the optional int tells how many prods of the lemma have to be used 
+   use all of them if None *)
 val make_clenv_binding_apply :
   Goal.goal sigma -> int option -> constr * constr -> constr bindings ->
    clausenv
 val make_clenv_binding :
   Goal.goal sigma -> constr * constr -> constr bindings -> clausenv
 
-(* [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where
+(** [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where
    [lmetas] is a list of metas to be applied to a proof of [t] so that
    it produces the unification pattern [ccl]; [sigma'] is [sigma]
    extended with [lmetas]; if [n] is defined, it limits the size of
@@ -124,20 +117,19 @@ val make_clenv_binding :
 val clenv_environments :
  evar_map -> int option -> types -> evar_map * constr list * types
 
-(* [clenv_environments_evars env sigma n t] does the same but returns
+(** [clenv_environments_evars env sigma n t] does the same but returns
    a list of Evar's defined in [env] and extends [sigma] accordingly *)
 val clenv_environments_evars :
  env -> evar_map -> int option -> types -> evar_map * constr list * types
 
-(* [clenv_conv_leq env sigma t c n] looks for c1...cn s.t. [t <= c c1...cn] *)
+(** [clenv_conv_leq env sigma t c n] looks for c1...cn s.t. [t <= c c1...cn] *)
 val clenv_conv_leq :
  env -> evar_map -> types -> constr -> int -> constr list
 
-(* if the clause is a product, add an extra meta for this product *)
+(** if the clause is a product, add an extra meta for this product *)
 exception NotExtensibleClause
 val clenv_push_prod : clausenv -> clausenv
 
-(***************************************************************)
-(* Pretty-print *)
+(** {6 Pretty-print } *)
 val pr_clenv : clausenv -> Pp.std_ppcmds