diff options
Diffstat (limited to 'proofs/proof_global.mli')
| -rw-r--r-- | proofs/proof_global.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 9b5015e0c..867010fb0 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -79,9 +79,12 @@ exception NoSuchProof val get_open_goals : unit -> int -(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is - no current proof. *) +(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is + no current proof. + The return boolean is set to [false] if an unsafe tactic has been used. *) val with_current_proof : + (unit Proofview.tactic -> Proof.proof -> Proof.proof*bool) -> bool +val simple_with_current_proof : (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit (** Sets the tactic to be used when a tactic line is closed with [...] *) |