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 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/decl_mode/decl_mode.ml')

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