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, 22 insertions, 21 deletions

diff --git a/kernel/sign.mli b/kernel/sign.mli
index b3e7ace55..5cadb125f 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -1,19 +1,17 @@
-(************************************************************************)
-(*  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 Term
-(*i*)
 
-(*s Signatures of ordered named declarations *)
+(** {6 Signatures of ordered named declarations } *)
 
 type named_context = named_declaration list
 type section_context = named_context
@@ -24,39 +22,42 @@ val vars_of_named_context : named_context -> identifier list
 
 val lookup_named : identifier -> named_context -> named_declaration
 
-(* number of declarations *)
+(** number of declarations *)
 val named_context_length : named_context -> int
 
-(*s Recurrence on [named_context]: older declarations processed first *)
+(** {6 Recurrence on [named_context]: older declarations processed first } *)
 val fold_named_context :
   (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a
-(* newer declarations first *)
+
+(** newer declarations first *)
 val fold_named_context_reverse :
   ('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a
 
-(*s Section-related auxiliary functions *)
+(** {6 Section-related auxiliary functions } *)
 val instance_from_named_context : named_context -> constr array
 
-(*s Signatures of ordered optionally named variables, intended to be
+(** {6 Sect } *)
+(** Signatures of ordered optionally named variables, intended to be
    accessed by de Bruijn indices *)
 
 val push_named_to_rel_context : named_context -> rel_context -> rel_context
 
-(*s Recurrence on [rel_context]: older declarations processed first *)
+(** {6 Recurrence on [rel_context]: older declarations processed first } *)
 val fold_rel_context :
   (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
-(* newer declarations first *)
+
+(** newer declarations first *)
 val fold_rel_context_reverse :
   ('a -> rel_declaration -> 'a) -> init:'a -> rel_context -> 'a
 
-(*s Map function of [rel_context] *)
+(** {6 Map function of [rel_context] } *)
 val map_rel_context : (constr -> constr) -> rel_context -> rel_context
 
-(*s Map function of [named_context] *)
+(** {6 Map function of [named_context] } *)
 val map_named_context : (constr -> constr) -> named_context -> named_context
 
-(*s Map function of [rel_context] *)
+(** {6 Map function of [rel_context] } *)
 val iter_rel_context : (constr -> unit) -> rel_context -> unit
 
-(*s Map function of [named_context] *)
+(** {6 Map function of [named_context] } *)
 val iter_named_context : (constr -> unit) -> named_context -> unit