From 80f2f9462205193885f054338ab28bfcd17de965 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:35:11 +0000
Subject: 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
---
 plugins/decl_mode/decl_mode.ml        | 6 +++---
 plugins/decl_mode/decl_proof_instr.ml | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins/decl_mode')

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
-- 
cgit v1.2.3