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, 45 insertions, 38 deletions

diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 9e24061d3..47b741f5d 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.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 Pp
 open Names
@@ -18,60 +17,62 @@ open Environ
 open Decl_kinds
 open Tacmach
 open Tacexpr
-(*i*)
 
-
-(*s Several proofs can be opened simultaneously but at most one is
+(** Several proofs can be opened simultaneously but at most one is
    focused at some time. The following functions work by side-effect
    on current set of open proofs. In this module, ``proofs'' means an
    open proof (something started by vernacular command [Goal], [Lemma]
    or [Theorem]), and ``goal'' means a subgoal of the current focused
    proof *)
 
-(*s [refining ()] tells if there is some proof in progress, even if a not
+(** {6 Sect } *)
+(** [refining ()] tells if there is some proof in progress, even if a not
    focused one *)
 
 val refining : unit -> bool
 
-(* [check_no_pending_proofs ()] fails if there is still some proof in
+(** [check_no_pending_proofs ()] fails if there is still some proof in
    progress *)
 
 val check_no_pending_proofs : unit -> unit
 
-(*s [delete_proof name] deletes proof of name [name] or fails if no proof
+(** {6 Sect } *)
+(** [delete_proof name] deletes proof of name [name] or fails if no proof
     has this name *)
 
 val delete_proof : identifier located -> unit
 
-(* [delete_current_proof ()] deletes current focused proof or fails if
+(** [delete_current_proof ()] deletes current focused proof or fails if
     no proof is focused *)
 
 val delete_current_proof : unit -> unit
 
-(* [delete_all_proofs ()] deletes all open proofs if any *)
+(** [delete_all_proofs ()] deletes all open proofs if any *)
 
 val delete_all_proofs : unit -> unit
 
-(*s [undo n] undoes the effect of the last [n] tactics applied to the
+(** {6 Sect } *)
+(** [undo n] undoes the effect of the last [n] tactics applied to the
     current proof; it fails if no proof is focused or if the ``undo''
     stack is exhausted *)
 
 val undo : int -> unit
 
-(* [undo_todepth n] resets the proof to its nth step (does [undo (d-n)] where d
+(** [undo_todepth n] resets the proof to its nth step (does [undo (d-n)] where d
    is the depth of the undo stack). *)
 val undo_todepth : int -> unit 
 
-(* Returns the depth of the current focused proof stack, this is used
+(** Returns the depth of the current focused proof stack, this is used
    to put informations in coq prompt (in emacs mode). *)
 val current_proof_depth: unit -> int
 
-(* [set_undo (Some n)] used to set the size of the ``undo'' stack. 
+(** [set_undo (Some n)] used to set the size of the ``undo'' stack. 
     These function now do nothing and will disapear. *)
 val set_undo : int option -> unit
 val get_undo : unit -> int option
 
-(*s [start_proof s str env t hook tac] starts a proof of name [s] and
+(** {6 Sect } *)
+(** [start_proof s str env t hook tac] starts a proof of name [s] and
     conclusion [t]; [hook] is optionally a function to be applied at
     proof end (e.g. to declare the built constructions as a coercion
     or a setoid morphism); init_tac is possibly a tactic to
@@ -85,27 +86,29 @@ val start_proof :
   ?init_tac:tactic -> ?compute_guard:lemma_possible_guards -> 
   declaration_hook -> unit
 
-(* [restart_proof ()] restarts the current focused proof from the beginning
+(** [restart_proof ()] restarts the current focused proof from the beginning
    or fails if no proof is focused *)
 
 val restart_proof : unit -> unit
 
-(*s [resume_last_proof ()] focus on the last unfocused proof or fails
+(** {6 Sect } *)
+(** [resume_last_proof ()] focus on the last unfocused proof or fails
    if there is no suspended proofs *)
 
 val resume_last_proof : unit -> unit
 
-(* [resume_proof name] focuses on the proof of name [name] or
+(** [resume_proof name] focuses on the proof of name [name] or
    raises [UserError] if no proof has name [name] *)
 
 val resume_proof : identifier located -> unit
 
-(* [suspend_proof ()] unfocuses the current focused proof or
+(** [suspend_proof ()] unfocuses the current focused proof or
    failed with [UserError] if no proof is currently focused *)
 
 val suspend_proof : unit -> unit
 
-(*s [cook_proof opacity] turns the current proof (assumed completed) into
+(** {6 Sect } *)
+(** [cook_proof opacity] turns the current proof (assumed completed) into
     a constant with its name, kind and possible hook (see [start_proof]);
     it fails if there is no current proof of if it is not completed;
     it also tells if the guardness condition has to be inferred. *)
@@ -115,63 +118,67 @@ val cook_proof : (Proof.proof -> unit) ->
     (Entries.definition_entry * lemma_possible_guards * goal_kind *
      declaration_hook)
 
-(* To export completed proofs to xml *)
+(** To export completed proofs to xml *)
 val set_xml_cook_proof : (goal_kind * Proof.proof -> unit) -> unit
 
-(*s [get_Proof.proof ()] returns the current focused pending proof or
+(** {6 Sect } *)
+(** [get_Proof.proof ()] returns the current focused pending proof or
    raises [UserError "no focused proof"] *)
 
 val get_pftreestate : unit -> Proof.proof
 
-(* [get_goal_context n] returns the context of the [n]th subgoal of
+(** [get_goal_context n] returns the context of the [n]th subgoal of
    the current focused proof or raises a [UserError] if there is no
    focused proof or if there is no more subgoals *)
 
 val get_goal_context : int -> Evd.evar_map * env
 
-(* [get_current_goal_context ()] works as [get_goal_context 1] *)
+(** [get_current_goal_context ()] works as [get_goal_context 1] *)
 
 val get_current_goal_context : unit -> Evd.evar_map * env
 
-(* [current_proof_statement] *)
+(** [current_proof_statement] *)
 
 val current_proof_statement :
   unit -> identifier * goal_kind * types * declaration_hook
 
-(*s [get_current_proof_name ()] return the name of the current focused
+(** {6 Sect } *)
+(** [get_current_proof_name ()] return the name of the current focused
     proof or failed if no proof is focused *)
 
 val get_current_proof_name : unit -> identifier
 
-(* [get_all_proof_names ()] returns the list of all pending proof names *)
+(** [get_all_proof_names ()] returns the list of all pending proof names *)
 
 val get_all_proof_names : unit -> identifier list
 
-(*s [set_end_tac tac] applies tactic [tac] to all subgoal generate
+(** {6 Sect } *)
+(** [set_end_tac tac] applies tactic [tac] to all subgoal generate
     by [solve_nth] *)
 
 val set_end_tac : tactic -> unit
 
-(*s [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the
+(** {6 Sect } *)
+(** [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the
    current focused proof or raises a UserError if no proof is focused or
    if there is no [n]th subgoal *)
 
 val solve_nth : ?with_end_tac:bool -> int -> tactic -> unit
 
-(* [by tac] applies tactic [tac] to the 1st subgoal of the current
+(** [by tac] applies tactic [tac] to the 1st subgoal of the current
    focused proof or raises a UserError if there is no focused proof or
    if there is no more subgoals *)
 
 val by : tactic -> unit
 
-(* [instantiate_nth_evar_com n c] instantiate the [n]th undefined
+(** [instantiate_nth_evar_com n c] instantiate the [n]th undefined
    existential variable of the current focused proof by [c] or raises a
    UserError if no proof is focused or if there is no such [n]th
    existential variable *)
 
 val instantiate_nth_evar_com : int -> Topconstr.constr_expr -> unit
 
-(* [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *)
+(** [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *)
 
 val build_constant_by_tactic : named_context_val -> types -> tactic ->
   Entries.definition_entry