diff options
| author | aspiwack | 2013-11-02 15:35:11 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-02 15:35:11 +0000 |
| commit | 80f2f9462205193885f054338ab28bfcd17de965 (patch) | |
| tree | b6c9e46cbc54080ec260282558abe9e8fc609723 /proofs/proof.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.mli')
| -rw-r--r-- | proofs/proof.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index fa6007061b..66aee03138 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -128,7 +128,9 @@ val no_focused_goal : proof -> bool (*** Tactics ***) -val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> proof +(* the returned boolean signal whether an unsafe tactic has been + used. In which case it is [false]. *) +val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> proof*bool val emit_side_effects : Declareops.side_effects -> proof -> proof |