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 /plugins/decl_mode/decl_mode.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 'plugins/decl_mode/decl_mode.ml')
| -rw-r--r-- | plugins/decl_mode/decl_mode.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index f3c5da2ad2..cbdcc96aa9 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -100,13 +100,13 @@ let proof_cond = Proof.no_cond proof_focus let focus p = let inf = get_stack p in - Proof_global.with_current_proof (fun _ -> Proof.focus proof_cond inf 1) + Proof_global.simple_with_current_proof (fun _ -> Proof.focus proof_cond inf 1) let unfocus () = - Proof_global.with_current_proof (fun _ p -> Proof.unfocus proof_focus p ()) + Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus proof_focus p ()) let maximal_unfocus () = - Proof_global.with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus) + Proof_global.simple_with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus) let get_top_stack pts = try |