diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:35:11 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:35:11 +0000 |
| commit | 80f2f9462205193885f054338ab28bfcd17de965 (patch) | |
| tree | b6c9e46cbc54080ec260282558abe9e8fc609723 /proofs/proof_global.mli | |
| parent | d45d2232e9dae87162a841a21cc708769259a184 (diff) | |
The tactic [admit] exits with the "unsafe" status.
It is highlighted in yellow in Coqide.
The unsafe status is tracked throughout the execution of tactics such that
nested calls to admit are caught.
Many function (mainly those building constr with tactics such as typeclass
related stuff, and Function, and a few other like eauto's use of Hint Extern)
drop the unsafe status. This is unfortunate, but a lot of refactoring would
be in order.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16977 85f007b7-540e-0410-9357-904b9bb8a0f7
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 [...] *) |