Doc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@470 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 43 insertions, 43 deletions

diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index a5f4c11126..7f6747721e 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -19,7 +19,7 @@ open Tacmach
    or [Theorem]), and ``goal'' means a subgoal of the current focused
    proof *)
 
-(* [refining ()] tells if there is some proof in progress, even if a not
+(*s [refining ()] tells if there is some proof in progress, even if a not
    focused one *)
 
 val refining : unit -> bool
@@ -29,7 +29,7 @@ val refining : unit -> bool
 
 val check_no_pending_proofs : unit -> unit
 
-(* [abort_proof name] aborts proof of name [name] or failed if no proof
+(*s [abort_proof name] aborts proof of name [name] or failed if no proof
 has this name *)
 
 val abort_proof : string -> unit
@@ -43,7 +43,7 @@ val abort_current_proof : unit -> unit
 
 val abort_all_proofs : unit -> unit
 
-(* [undo n] undoes the effect of the last [n] tactics applied to the
+(*s [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 *)
 
@@ -58,12 +58,31 @@ val set_undo : int -> unit
 
 val reset_undo : unit -> unit
 
-(* [resume_last_proof ()] focus on the last unfocused proof or fails
+(*s [start_proof s str env t] starts a proof of name [s] and conclusion [t] *)
+
+val start_proof : string -> strength -> env -> constr -> unit
+
+(* [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
    if there is no suspended proofs *)
 
 val resume_last_proof : unit -> unit
 
-(* [get_pftreestate ()] returns the current focused pending proof or
+(* [resume_proof name] focuses on the proof of name [name] or
+   raises [UserError] if no proof has name [name] *)
+
+val resume_proof : string -> unit
+
+(* [suspend_proof ()] unfocuses the current focused proof or
+   failed with [UserError] if no proof is currently focused *)
+
+val suspend_proof : unit -> unit
+
+(*s [get_pftreestate ()] returns the current focused pending proof or
    raises [UserError "no focused proof"] *)
 
 val get_pftreestate : unit -> pftreestate
@@ -78,17 +97,7 @@ val get_goal_context : int -> evar_declarations * env
 
 val get_current_goal_context : unit -> evar_declarations * env
 
-(* [resume_proof name] focuses on the proof of name [name] or
-   raises [UserError] if no proof has name [name] *)
-
-val resume_proof : string -> unit
-
-(* [suspend_proof ()] unfocuses the current focused proof or
-   failed with [UserError] if no proof is currently focused *)
-
-val suspend_proof : unit -> unit
-
-(* [get_current_proof_name ()] return the name of the current focused
+(*s [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 -> string
@@ -97,16 +106,26 @@ val get_current_proof_name : unit -> string
 
 val get_all_proof_names : unit -> string list
 
-(* [restart_proof ()] restarts the current focused proof from the beginning
-   or fails if no proof is focused *)
+(*s [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 restart_proof : unit -> unit
+val solve_nth : int -> tactic -> unit
+
+(* [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 *)
 
-(* [start_proof s str env t] starts a proof of name [s] and conclusion [t] *)
+val by : tactic -> unit
 
-val start_proof : string -> strength -> env -> constr -> unit
+(* [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 *)
 
-(* [save_named b] saves the current completed proof under the name it
+val instantiate_nth_evar_com : int -> Coqast.t -> unit
+
+(*s [save_named b] saves the current completed proof under the name it
 was started; boolean [b] tells if the theorem is declared opaque; it
 fails if the proof is not completed *)
 
@@ -122,26 +141,7 @@ theorem under the name [name] and gives it the strength of a remark *)
 
 val save_anonymous_remark : bool -> string -> unit
 
-(* [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 : int -> tactic -> unit
-
-(* [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
-   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 -> Coqast.t -> unit
-
-(* To deal with subgoal focus *)
+(*s To deal with subgoal focus *)
 
 val make_focus : int -> unit
 val focus : unit -> int
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 98c6ab96fe..d2d2794f0c 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -57,7 +57,7 @@ val tclTHEN          : tactic -> tactic -> tactic
 val tclTHENLIST      : tactic list -> tactic
 
 (* [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
-   [(tac2 i)] to the i_th resulting subgoal (starting from 1) *)
+   [(tac2 i)] to the [i]$^{th}$ resulting subgoal (starting from 1) *)
 val tclTHEN_i        : tactic -> (int -> tactic) -> tactic
 
 (* [tclTHENL tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]