aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/pfedit.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 090edde5a5..4ca23e7116 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -99,8 +99,8 @@ val cook_proof : (Proof.proof -> unit) ->
val set_xml_cook_proof : (goal_kind * Proof.proof -> unit) -> unit
(** {6 ... } *)
-(** [get_pftreestate ()] returns the current focused pending proof or
- @raise NoCurrentProof *)
+(** [get_pftreestate ()] returns the current focused pending proof.
+ @raise NoCurrentProof if there is no pending proof. *)
val get_pftreestate : unit -> Proof.proof