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, 18 insertions, 15 deletions

diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index bf1d23241..bbb3d838e 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -1,15 +1,16 @@
-(************************************************************************)
-(*  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*)
 
-(*s Explicit substitutions of type ['a]. *)
-(*  - ESID(n)             = %n END   bounded identity
+(** {6 Sect } *)
+(** Explicit substitutions of type ['a]. 
+    - ESID(n)             = %n END   bounded identity
  *  - CONS([|t1..tn|],S)  = (S.t1...tn)    parallel substitution
  *       (beware of the order: indice 1 is substituted by tn)
  *  - SHIFT(n,S)          = (^n o S) terms in S are relocated with n vars
@@ -21,15 +22,16 @@ type 'a subs =
   | SHIFT of int * 'a subs
   | LIFT of int * 'a subs
 
-(* Derived constructors granting basic invariants *)
+(** Derived constructors granting basic invariants *)
 val subs_cons: 'a array * 'a subs -> 'a subs
 val subs_shft: int * 'a subs -> 'a subs
 val subs_lift: 'a subs -> 'a subs
 val subs_liftn: int -> 'a subs -> 'a subs
-(* [subs_shift_cons(k,s,[|t1..tn|])] builds (^k s).t1..tn *)
+
+(** [subs_shift_cons(k,s,[|t1..tn|])] builds (^k s).t1..tn *)
 val subs_shift_cons: int * 'a subs * 'a array -> 'a subs
 
-(* [expand_rel k subs] expands de Bruijn [k] in the explicit substitution
+(** [expand_rel k subs] expands de Bruijn [k] in the explicit substitution
  * [subs]. The result is either (Inl(lams,v)) when the variable is
  * substituted by value [v] under lams binders (i.e. v *has* to be
  * shifted by lams), or (Inr (k',p)) when the variable k is just relocated
@@ -38,17 +40,18 @@ val subs_shift_cons: int * 'a subs * 'a array -> 'a subs
  *)
 val expand_rel: int -> 'a subs -> (int * 'a, int * int option) Util.union
 
-(* Tests whether a substitution behaves like the identity *)
+(** Tests whether a substitution behaves like the identity *)
 val is_subs_id: 'a subs -> bool
 
-(* Composition of substitutions: [comp mk_clos s1 s2] computes a
+(** Composition of substitutions: [comp mk_clos s1 s2] computes a
  * substitution equivalent to applying s2 then s1. Argument
  * mk_clos is used when a closure has to be created, i.e. when
  * s1 is applied on an element of s2.
  *)
 val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs
 
-(*s Compact representation of explicit relocations. \\
+(** {6 Sect } *)
+(** Compact representation of explicit relocations. \\
    [ELSHFT(l,n)] == lift of [n], then apply [lift l].
    [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *)
 type lift =