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

diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index a948d1647..53925955e 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -1,19 +1,19 @@
-(************************************************************************)
-(*  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 [Mod_subst] *)
+(** {6 [Mod_subst] } *)
 
 open Names
 open Term
 
-(* A delta_resolver maps name (constant, inductive, module_path) 
+(** A delta_resolver maps name (constant, inductive, module_path) 
    to canonical name  *)
 type delta_resolver
 
@@ -35,30 +35,30 @@ val add_mp_delta_resolver : module_path -> module_path -> delta_resolver
 
 val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver
 
-(* Apply the substitution on the domain of the resolver  *)
+(** Apply the substitution on the domain of the resolver  *)
 val subst_dom_delta_resolver : substitution -> delta_resolver -> delta_resolver
 
-(* Apply the substitution on the codomain of the resolver  *)
+(** Apply the substitution on the codomain of the resolver  *)
 val subst_codom_delta_resolver : substitution -> delta_resolver -> delta_resolver
 
 val subst_dom_codom_delta_resolver : 
   substitution -> delta_resolver -> delta_resolver
 
-(* *_of_delta return the associated name of arg2 in arg1   *)
+(** *_of_delta return the associated name of arg2 in arg1   *)
 val constant_of_delta : delta_resolver -> constant -> constant
 
 val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive
 
 val delta_of_mp : delta_resolver -> module_path -> module_path
 
-(* Extract the set of inlined constant in the resolver *)
+(** Extract the set of inlined constant in the resolver *)
 val inline_of_delta : delta_resolver -> kernel_name list
 
-(* remove_mp is used for the computation of a resolver induced by Include P *)
+(** remove_mp is used for the computation of a resolver induced by Include P *)
 val remove_mp_delta_resolver : delta_resolver -> module_path -> delta_resolver
 
 
-(* mem tests *)
+(** mem tests *)
 val mp_in_delta : module_path -> delta_resolver -> bool
 
 val con_in_delta : constant -> delta_resolver -> bool
@@ -69,20 +69,20 @@ val mind_in_delta : mutual_inductive -> delta_resolver -> bool
 
 val empty_subst : substitution
 
-(* add_* add [arg2/arg1]{arg3} to the substitution with no 
+(** add_* add [arg2/arg1]\{arg3\} to the substitution with no 
    sequential composition  *)
 val add_mbid :
   mod_bound_id -> module_path -> delta_resolver  -> substitution -> substitution
 val add_mp :
   module_path -> module_path -> delta_resolver -> substitution -> substitution
 
-(* map_* create a new substitution [arg2/arg1]{arg3} *)
+(** map_* create a new substitution [arg2/arg1]\{arg3\} *)
 val map_mbid :
   mod_bound_id -> module_path -> delta_resolver -> substitution
 val map_mp :
   module_path -> module_path -> delta_resolver -> substitution
 
-(* sequential composition:
+(** sequential composition:
    [substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)]
 *)
 val join : substitution -> substitution -> substitution
@@ -97,9 +97,9 @@ val debug_string_of_subst : substitution -> string
 val debug_pr_subst : substitution -> Pp.std_ppcmds
 val debug_string_of_delta : delta_resolver -> string
 val debug_pr_delta : delta_resolver -> Pp.std_ppcmds
-(*i*)
+(**/**)
 
-(* [subst_mp sub mp] guarantees that whenever the result of the
+(** [subst_mp sub mp] guarantees that whenever the result of the
    substitution is structutally equal [mp], it is equal by pointers
    as well [==] *)
 
@@ -115,7 +115,7 @@ val subst_kn :
 val subst_con :
   substitution -> constant -> constant * constr
 
-(* Here the semantics is completely unclear.
+(** Here the semantics is completely unclear.
    What does "Hint Unfold t" means when "t" is a parameter?
    Does the user mean "Unfold X.t" or does she mean "Unfold y"
    where X.t is later on instantiated with y? I choose the first
@@ -123,14 +123,14 @@ val subst_con :
 val subst_evaluable_reference :
   substitution -> evaluable_global_reference -> evaluable_global_reference
 
-(* [replace_mp_in_con mp mp' con] replaces [mp] with [mp'] in [con] *)
+(** [replace_mp_in_con mp mp' con] replaces [mp] with [mp'] in [con] *)
 val replace_mp_in_kn : module_path -> module_path -> kernel_name -> kernel_name
 
-(* [subst_mps sub c] performs the substitution [sub] on all kernel
+(** [subst_mps sub c] performs the substitution [sub] on all kernel
    names appearing in [c] *)
 val subst_mps : substitution -> constr -> constr
 
-(* [occur_*id id sub] returns true iff [id] occurs in [sub]
+(** [occur_*id id sub] returns true iff [id] occurs in [sub]
    on either side *)
 
 val occur_mbid : mod_bound_id -> substitution -> bool