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 | |
| 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')
| -rw-r--r-- | plugins/decl_mode/decl_mode.ml | 6 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 4 |
2 files changed, 5 insertions, 5 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 diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index e47776bd7d..6b5cb7492b 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -121,7 +121,7 @@ let start_proof_tac gls= tcl_change_info info gls let go_to_proof_mode () = - Pfedit.by (Proofview.V82.tactic start_proof_tac); + ignore (Pfedit.by (Proofview.V82.tactic start_proof_tac)); let p = Proof_global.give_me_the_proof () in Decl_mode.focus p @@ -1461,7 +1461,7 @@ let do_instr raw_instr pts = let glob_instr = intern_proof_instr ist raw_instr in let instr = interp_proof_instr (get_its_info gl) sigma env glob_instr in - Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)) + ignore (Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp))) else () end; postprocess pts raw_instr.instr; (* spiwack: this should restore a compatible semantics with |