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.ml | |
| 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.ml')
| -rw-r--r-- | proofs/proof.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 89f3638a1..3a00d76f0 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -252,8 +252,8 @@ let initial_goals p = Proofview.initial_goals p.proofview let run_tactic env tac pr = let sp = pr.proofview in - let (_,tacticced_proofview) = Proofview.apply env tac sp in - { pr with proofview = tacticced_proofview } + let (_,tacticced_proofview,status) = Proofview.apply env tac sp in + { pr with proofview = tacticced_proofview },status let emit_side_effects eff pr = {pr with proofview = Proofview.emit_side_effects eff pr.proofview} |