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, 23 insertions, 23 deletions

diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 74a0d7d8e..954890d89 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -1,23 +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 Nametab
 open Term
 open Libnames
 open Libobject
 open Library
-(*i*)
 
-(*s A structure S is a non recursive inductive type with a single
+(** {6 Sect } *)
+(** A structure S is a non recursive inductive type with a single
    constructor (the name of which defaults to Build_S) *)
 
 type struc_typ = {
@@ -29,34 +28,35 @@ type struc_typ = {
 val declare_structure :
   inductive * constructor * (name * bool) list * constant option list -> unit
 
-(* [lookup_structure isp] returns the struc_typ associated to the
+(** [lookup_structure isp] returns the struc_typ associated to the
    inductive path [isp] if it corresponds to a structure, otherwise
    it fails with [Not_found] *)
 val lookup_structure : inductive -> struc_typ
 
-(* [lookup_projections isp] returns the projections associated to the
+(** [lookup_projections isp] returns the projections associated to the
    inductive path [isp] if it corresponds to a structure, otherwise
    it fails with [Not_found] *)
 val lookup_projections : inductive -> constant option list
 
-(* raise [Not_found] if not a projection *)
+(** raise [Not_found] if not a projection *)
 val find_projection_nparams : global_reference -> int
 
-(* raise [Not_found] if not a projection *)
+(** raise [Not_found] if not a projection *)
 val find_projection : global_reference -> struc_typ
 
-(* we keep an index (dnet) of record's arguments + fields
+(** we keep an index (dnet) of record's arguments + fields
    (=methods). Here is how to declare them: *)
 val declare_method :
   global_reference -> Evd.evar -> Evd.evar_map -> unit
-  (* and here is how to search for methods matched by a given term: *)
+  (** and here is how to search for methods matched by a given term: *)
 val methods_matching : constr ->
   ((global_reference*Evd.evar*Evd.evar_map) *
      (constr*existential_key)*Termops.subst) list
 
-(*s A canonical structure declares "canonical" conversion hints between *)
-(*  the effective components of a structure and the projections of the  *)
-(*  structure *)
+(** {6 Sect } *)
+(** A canonical structure declares "canonical" conversion hints between 
+    the effective components of a structure and the projections of the  
+    structure *)
 
 type cs_pattern =
     Const_cs of global_reference
@@ -66,11 +66,11 @@ type cs_pattern =
 
 type obj_typ = {
   o_DEF : constr;
-  o_INJ : int;      (* position of trivial argument *)
-  o_TABS : constr list;    (* ordered *)
-  o_TPARAMS : constr list; (* ordered *)
+  o_INJ : int;      (** position of trivial argument *)
+  o_TABS : constr list;    (** ordered *)
+  o_TPARAMS : constr list; (** ordered *)
   o_NPARAMS : int;
-  o_TCOMPS : constr list } (* ordered *)
+  o_TCOMPS : constr list } (** ordered *)
 
 val cs_pattern_of_constr : constr -> cs_pattern * int * constr list