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

6 files changed, 20 insertions, 20 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
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 2da4b61478..8c2fdb7eb5 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -983,7 +983,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
     (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
     lemma_type
     (fun _ _ -> ());
-  Pfedit.by (Proofview.V82.tactic prove_replacement);
+  ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
   Lemmas.save_named false
 
 
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 0850d556cc..3d577b4401 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -297,7 +297,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
       (hook new_principle_type)
     ;
     (*       let _tim1 = System.get_time ()  in *)
-    Pfedit.by  (Proofview.V82.tactic (proof_tac (Array.map mkConst funs) mutr_nparams));
+    ignore (Pfedit.by  (Proofview.V82.tactic (proof_tac (Array.map mkConst funs) mutr_nparams)));
     (*       let _tim2 =  System.get_time ()  in *)
     (* 	begin *)
     (* 	  let dur1 = System.time_difference tim1 tim2 in *)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index ce25f7aaf0..36de855957 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1069,9 +1069,9 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	   (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
 	   (fst lemmas_types_infos.(i))
            (fun _ _ -> ());
-	 Pfedit.by
+	 ignore (Pfedit.by
 	   (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
-	      (proving_tac i)));
+	      (proving_tac i))));
 	 do_save ();
 	 let finfo = find_Function_infos f_as_constant in
 	 let lem_cst = destConst (Constrintern.global_reference lem_id) in
@@ -1120,9 +1120,9 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	   (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
 	   (fst lemmas_types_infos.(i))
            (fun _ _ -> ());
-	 Pfedit.by
+	 ignore (Pfedit.by
 	   (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
-	      (proving_tac i)));
+	      (proving_tac i))));
 	 do_save ();
 	 let finfo = find_Function_infos f_as_constant in
 	 let lem_cst = destConst (Constrintern.global_reference lem_id) in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 76095cb1c8..881d930fcc 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1319,10 +1319,10 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
     hook;
   if Indfun_common.is_strict_tcc  ()
   then
-    by (Proofview.V82.tactic (tclIDTAC))
+    ignore (by (Proofview.V82.tactic (tclIDTAC)))
   else 
     begin
-      by (Proofview.V82.tactic begin
+      ignore (by (Proofview.V82.tactic begin
 	fun g ->
 	  tclTHEN
 	    (decompose_and_tac)
@@ -1338,10 +1338,10 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 	 	     )
 	 	     using_lemmas)
 	       ) tclIDTAC)
-	    g end)
+	    g end))
     end;
   try
-    by (Proofview.V82.tactic tclIDTAC); (* raises UserError _ if the proof is complete *)
+    ignore (by (Proofview.V82.tactic tclIDTAC)); (* raises UserError _ if the proof is complete *)
   with UserError _ ->
     defined ()
 
@@ -1364,9 +1364,9 @@ let com_terminate
       (Global, Proof Lemma) (Environ.named_context_val env)
       (compute_terminate_type nb_args fonctional_ref) hook;
 
-    by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start));
-    by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
-    				   input_type relation rec_arg_num )))
+    ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start)));
+    ignore (by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
+    				   input_type relation rec_arg_num ))))
   in
   start_proof tclIDTAC tclIDTAC;
   try
@@ -1410,7 +1410,7 @@ let (com_eqn : int -> Id.t ->
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
     (start_proof eq_name (Global, Proof Lemma)
        (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
-     by
+     ignore (by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref
 	  (fun  x ->
 	     prove_eq (fun _ -> tclIDTAC)
@@ -1437,7 +1437,7 @@ let (com_eqn : int -> Id.t ->
 		ih = Id.of_string "______";
 	       }
 	  )
-       )); 
+       ))); 
      (* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
 (*      Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *)
      Flags.silently (fun () -> Lemmas.save_named opacity) () ;