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

25 files changed, 293 insertions, 145 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) () ; 
diff --git a/proofs/monads.ml b/proofs/monads.ml
index ba14408641..803715a450 100644
--- a/proofs/monads.ml
+++ b/proofs/monads.ml
@@ -22,6 +22,13 @@ module type State = sig
   val get : s t
 end
 
+module type Writer = sig
+  type m (* type of the messages *)
+  include S
+
+  val put : m -> unit t
+end
+
 module type IO = sig
   include S
 
@@ -133,6 +140,54 @@ end = struct
     T.return { result=s ; state=s }
 end
 
+module type Monoid = sig
+  type t
+
+  val zero : t
+  val ( * ) : t -> t -> t
+end
+
+module Writer (M:Monoid) (T:S) : sig
+  include Writer with type +'a t = private ('a*M.t) T.t and type m = M.t
+
+  val lift : 'a T.t -> 'a t
+  (* The coercion from private ['a t] in function form. *)
+  val run : 'a t -> ('a*m) T.t
+end = struct
+
+  type 'a t = ('a*M.t) T.t
+  type m = M.t
+
+  let run x = x
+
+  (*spiwack: convenience notation, waiting for ocaml 3.12 *)
+  let (>>=) = T.bind
+
+  let bind x k = 
+    x >>= fun (a,m) ->
+    k a >>= fun (r,m') ->
+    T.return (r,M.( * ) m m')
+
+  let seq x k =
+    x >>= fun ((),m) ->
+    k >>= fun (r,m') ->
+    T.return (r,M.( * ) m m')
+
+  let return x =
+    T.return (x,M.zero)
+
+  let ignore x =
+    x >>= fun (_,m) ->
+    T.return ((),m)
+
+  let lift x =
+    x >>= fun r ->
+    T.return (r,M.zero)
+
+  let put m =
+    T.return ((),m)
+end
+
 (* Double-continuation backtracking monads are reasonable folklore for
    "search" implementations (including Tac interactive prover's
    tactics). Yet it's quite hard to wrap your head around these.  I
@@ -301,6 +356,7 @@ module StateLogic(X:Type)(T:Logic) : sig
   val set : s -> unit t
   val get : s t
 
+  val lift : 'a T.t -> 'a t
   val run : 'a t -> s -> 'a result T.t
 end = struct
 
@@ -370,14 +426,71 @@ end = struct
     return a.result
 end
 
+(* [Writer(M)(T:Logic)] can be lifted to [Logic] by backtracking on state on [plus].*)
+module WriterLogic(M:Monoid)(T:Logic) : sig
+  (* spiwack: some duplication from interfaces as we need ocaml 3.12
+     to substitute inside signatures. *)
+  type m = M.t
+  include Logic with type +'a t = private ('a*m) T.t
 
+  val put : m -> unit t
 
+  val lift : 'a T.t -> 'a t
+  val run : 'a t -> ('a*m) T.t
+end = struct
+  module W = Writer(M)(T)
+  include W
 
+  let zero e = lift (T.zero e)
+  let plus x y =
+    (* spiwack: convenience notation, waiting for ocaml 3.12 *)
+    let (>>=) = bind in
+    let (>>) = seq in
+    lift begin
+      (T.plus (run x) (fun e -> run (y e))) 
+    end >>= fun (r,m) ->
+    put m >>
+    return r
 
+  let split x =
+    (* spiwack: convenience notation, waiting for ocaml 3.12 *)
+    let (>>=) = bind in
+    let (>>) = seq in
+    lift (T.split (run x)) >>= function
+      | Util.Inr _ as e -> return e
+      | Util.Inl ((a,m),y) ->
+          let y' e =
+            lift (y e) >>= fun (b,m) ->
+            put m >>
+            return b
+          in
+          put m >>
+          return (Util.Inl(a,y'))
 
 
+  (*** IO ***)
 
+  type 'a ref = 'a T.ref
+  let ref x = lift (T.ref x)
+  let (:=) r x = lift (T.(:=) r x)
+  let (!) r = lift (T.(!) r)
 
+  let raise e = lift (T.raise e)
+  let catch t h =
+    (* spiwack: convenience notation, waiting for ocaml 3.12 *)
+    let (>>=) = bind in
+    let (>>) = seq in
+    let h' e = run (h e) in
+    lift (T.catch (run t) h') >>= fun (a,m) ->
+    put m >>
+    return a
 
-
-
+  exception Timeout
+  let timeout n t =
+    (* spiwack: convenience notation, waiting for ocaml 3.12 *)
+    let (>>=) = bind in
+    let (>>) = seq in
+    lift (T.timeout n (run t)) >>= fun (a,m) ->
+    put m >>
+    return a
+end
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 55c46a3401..6c0ddfc11a 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -33,10 +33,10 @@ let start_proof (id : Id.t) str hyps c ?init_tac ?compute_guard hook =
   let goals = [ (Global.env_of_context hyps , c) ] in
   Proof_global.start_proof id str goals ?compute_guard hook;
   let env = Global.env () in
-  Proof_global.with_current_proof (fun _ p ->
+  ignore (Proof_global.with_current_proof (fun _ p ->
     match init_tac with
-    | None -> p
-    | Some tac -> Proof.run_tactic env tac p)
+    | None -> p,true
+    | Some tac -> Proof.run_tactic env tac p))
 
 let cook_this_proof hook p =
   match p with
@@ -105,7 +105,7 @@ let solve_nth ?with_end_tac gi tac pr =
 let by tac = Proof_global.with_current_proof (fun _ -> solve_nth 1 tac)
 
 let instantiate_nth_evar_com n com = 
-  Proof_global.with_current_proof (fun _ -> Proof.V82.instantiate_evar n com)
+  Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p)
 
 
 (**********************************************************************)
@@ -118,10 +118,10 @@ let next = let n = ref 0 in fun () -> incr n; !n
 let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac =
   start_proof id goal_kind sign typ (fun _ _ -> ());
   try
-    by tac;
+    let status = by tac in
     let _,(const,_,_,_) = cook_proof (fun _ -> ()) in
     delete_current_proof ();
-    const
+    const, status
   with reraise ->
     delete_current_proof ();
     raise reraise
@@ -134,11 +134,11 @@ let constr_of_def = function
 let build_by_tactic env typ tac =
   let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
-  let ce = build_constant_by_tactic id sign typ tac in
+  let ce,status = build_constant_by_tactic id sign typ tac in
   let ce = Term_typing.handle_side_effects env ce in
   let cb, se = Future.force ce.const_entry_body in
-  assert(Declareops.side_effects_is_empty se);
-  cb
+  assert(Declareops.side_effects_is_empty (Declareops.no_seff));
+  cb,status
 
 (**********************************************************************)
 (* Support for resolution of evars in tactic interpretation, including
@@ -155,7 +155,7 @@ let solve_by_implicit_tactic env sigma evk =
       when
 	Context.named_context_equal (Environ.named_context_of_val evi.evar_hyps)
 	(Environ.named_context env) ->
-      (try build_by_tactic env evi.evar_concl (Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []))
+      (try fst (build_by_tactic env evi.evar_concl (Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) [])))
        with e when Logic.catchable_exception e -> raise Exit)
   | _ -> raise Exit
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 3a0c25c46a..73f12db987 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -136,13 +136,14 @@ val get_used_variables : unit -> Context.section_context option
    if there is no [n]th subgoal *)
 
 val solve_nth : ?with_end_tac:unit Proofview.tactic -> int -> unit Proofview.tactic ->
-      Proof.proof -> Proof.proof
+      Proof.proof -> Proof.proof*bool
 
 (** [by tac] applies tactic [tac] to the 1st subgoal of the current
    focused proof or raises a UserError if there is no focused proof or
-   if there is no more subgoals *)
+   if there is no more subgoals.
+   Returns [false] if an unsafe tactic has been used. *)
 
-val by : unit Proofview.tactic -> unit
+val by : unit Proofview.tactic -> bool
 
 (** [instantiate_nth_evar_com n c] instantiate the [n]th undefined
    existential variable of the current focused proof by [c] or raises a
@@ -151,12 +152,14 @@ val by : unit Proofview.tactic -> unit
 
 val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
 
-(** [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *)
+(** [build_by_tactic typ tac] returns a term of type [typ] by calling
+    [tac]. The return boolean, if [false] indicates the use of an unsafe
+    tactic. *)
 
 val build_constant_by_tactic :
   Id.t -> named_context_val -> ?goal_kind:goal_kind ->
-    types -> unit Proofview.tactic -> Entries.definition_entry
-val build_by_tactic : env -> types -> unit Proofview.tactic -> constr
+    types -> unit Proofview.tactic -> Entries.definition_entry * bool
+val build_by_tactic : env -> types -> unit Proofview.tactic -> constr * bool
 
 (** Declare the default tactic to fill implicit arguments *)
 
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 89f3638a10..3a00d76f06 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -252,8 +252,8 @@ let initial_goals p = Proofview.initial_goals p.proofview
 
 let run_tactic env tac pr =
   let sp = pr.proofview in
-  let (_,tacticced_proofview) = Proofview.apply env tac sp in
-  { pr with proofview = tacticced_proofview }
+  let (_,tacticced_proofview,status) = Proofview.apply env tac sp in
+  { pr with proofview = tacticced_proofview },status
 
 let emit_side_effects eff pr =
   {pr with proofview = Proofview.emit_side_effects eff pr.proofview}
diff --git a/proofs/proof.mli b/proofs/proof.mli
index fa6007061b..66aee03138 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -128,7 +128,9 @@ val no_focused_goal : proof -> bool
 
 (*** Tactics ***)
 
-val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> proof
+(* the returned boolean signal whether an unsafe tactic has been
+   used. In which case it is [false]. *)
+val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> proof*bool
 
 val emit_side_effects : Declareops.side_effects -> proof -> proof
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 3f84f6500d..5e11cfdb2d 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -154,8 +154,12 @@ let with_current_proof f =
         match p.endline_tactic with
         | None -> Proofview.tclUNIT ()
         | Some tac -> !interp_tac tac in
-      let p = { p with proof = f et p.proof } in
-      pstates := p :: rest
+      let (newpr,status) = f et p.proof in
+      let p = { p with proof = newpr } in
+      pstates := p :: rest;
+      status
+let simple_with_current_proof f =
+  ignore (with_current_proof (fun t p -> f t p , true))
 
 (* Sets the tactic to be used when a tactic line is closed with [...] *)
 let set_endline_tactic tac =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 9b5015e0c3..867010fb05 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -79,9 +79,12 @@ exception NoSuchProof
 
 val get_open_goals : unit -> int
 
-(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is 
-   no current proof. *)
+(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is
+    no current proof.
+    The return boolean is set to [false] if an unsafe tactic has been used. *)
 val with_current_proof :
+  (unit Proofview.tactic -> Proof.proof -> Proof.proof*bool) -> bool
+val simple_with_current_proof :
   (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit
 
 (** Sets the tactic to be used when a tactic line is closed with [...] *)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 3f80da785c..a3791e7a42 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -190,81 +190,88 @@ let unfocus c sp =
    - backtrack on previous changes of the proofview *)
 (* spiwack: it seems lighter, for now, to deal with the environment here rather than in [Monads]. *)
 
-module LocalState = struct
+module ProofState = struct
   type t = proofview
 end
+module MessageType = struct
+  type t = bool (* [false] if an unsafe tactic has been used. *)
+
+  let zero = true
+  let ( * ) s1 s2 = s1 && s2
+end
 module Backtrack = Monads.Logic(Monads.IO)
-module Inner = Monads.StateLogic(LocalState)(Backtrack)
+module Message = Monads.WriterLogic(MessageType)(Backtrack)
+module Proof = Monads.StateLogic(ProofState)(Message)
 
-type +'a tactic = Environ.env -> 'a Inner.t
+type +'a tactic = Environ.env -> 'a Proof.t
 
 (* Applies a tactic to the current proofview. *)
 let apply env t sp =
-  let next = Monads.IO.run (Backtrack.run (Inner.run (t env) sp)) in
-  next.Inner.result , next.Inner.state
+  let (next,status) = Monads.IO.run (Backtrack.run (Message.run (Proof.run (t env) sp))) in
+  next.Proof.result , next.Proof.state , status
 
 (*** tacticals ***)
 
 
 (* Unit of the tactic monad *)
-let tclUNIT a _ = Inner.return a
+let tclUNIT a _ = Proof.return a
 
 (* Bind operation of the tactic monad *)
 let tclBIND t k env =
-  Inner.bind (t env) (fun a -> k a env)
+  Proof.bind (t env) (fun a -> k a env)
 
 (* Interpretes the ";" (semicolon) of Ltac.
    As a monadic operation, it's a specialized "bind"
    on unit-returning tactic (meaning "there is no value to bind") *)
 let tclTHEN t1 t2 env =
-  Inner.seq (t1 env) (t2 env)
+  Proof.seq (t1 env) (t2 env)
 
 (* [tclIGNORE t] has the same operational content as [t],
    but drops the value at the end. *)
-let tclIGNORE tac env = Inner.ignore (tac env)
+let tclIGNORE tac env = Proof.ignore (tac env)
 
 (* [tclOR t1 t2 = t1] as long as [t1] succeeds. Whenever the successes
    of [t1] have been depleted and it failed with [e], then it behaves
    as [t2 e].  No interleaving at this point. *)
 let tclOR t1 t2 env =
-  Inner.plus (t1 env) (fun e -> t2 e env)
+  Proof.plus (t1 env) (fun e -> t2 e env)
 
 (* [tclZERO e] always fails with error message [e]*)
-let tclZERO e _ = Inner.zero e
+let tclZERO e _ = Proof.zero e
 
 (* [tclORELSE t1 t2] behaves like [t1] if [t1] succeeds at least once
    or [t2] if [t1] fails. *)
 let tclORELSE t1 t2 env =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
-  let (>>=) = Inner.bind in
-  Inner.split (t1 env) >>= function
+  let (>>=) = Proof.bind in
+  Proof.split (t1 env) >>= function
     | Util.Inr e -> t2 e env
-    | Util.Inl (a,t1') -> Inner.plus (Inner.return a) t1'
+    | Util.Inl (a,t1') -> Proof.plus (Proof.return a) t1'
 
 (* [tclIFCATCH a s f] is a generalisation of [tclORELSE]: if [a]
    succeeds at least once then it behaves as [tclBIND a s] otherwise, if [a]
    fails with [e], then it behaves as [f e]. *)
 let tclIFCATCH a s f env =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
-  let (>>=) = Inner.bind in
-  Inner.split (a env) >>= function
+  let (>>=) = Proof.bind in
+  Proof.split (a env) >>= function
     | Util.Inr e -> f e env
-    | Util.Inl (x,a') -> Inner.plus (s x env) (fun e -> (a' e) >>= fun x' -> (s x' env))
+    | Util.Inl (x,a') -> Proof.plus (s x env) (fun e -> (a' e) >>= fun x' -> (s x' env))
 
 (* Focuses a tactic at a range of subgoals, found by their indices. *)
 (* arnaud: bug if 0 goals ! *)
 let tclFOCUS i j t env =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
-  let (>>=) = Inner.bind in
-  let (>>) = Inner.seq in
-  Inner.get >>= fun initial ->
+  let (>>=) = Proof.bind in
+  let (>>) = Proof.seq in
+  Proof.get >>= fun initial ->
   try
     let (focused,context) = focus i j initial in
-    Inner.set focused >>
+    Proof.set focused >>
     t (env) >>= fun result ->
-    Inner.get >>= fun next ->
-    Inner.set (unfocus context next) >>
-    Inner.return result
+    Proof.get >>= fun next ->
+    Proof.set (unfocus context next) >>
+    Proof.return result
   with e ->
     (* spiwack: a priori the only possible exceptions are that of focus,
        of course I haven't made them algebraic yet. *)
@@ -294,24 +301,24 @@ end
 
 let rec tclDISPATCHGEN null join tacs env =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
-  let (>>=) = Inner.bind in
-  let (>>) = Inner.seq in
-  Inner.get >>= fun initial ->
+  let (>>=) = Proof.bind in
+  let (>>) = Proof.seq in
+  Proof.get >>= fun initial ->
   match tacs,initial.comb with
   | [], [] -> tclUNIT null env
   | t::tacs , first::goals ->
       begin match Goal.advance initial.solution first with
-      | None -> Inner.return null (* If [first] has been solved by side effect: do nothing. *)
+      | None -> Proof.return null (* If [first] has been solved by side effect: do nothing. *)
       | Some first ->
-          Inner.set {initial with comb=[first]} >>
+          Proof.set {initial with comb=[first]} >>
           t env
       end >>= fun y ->
-      Inner.get >>= fun step ->
-      Inner.set {step with comb=goals} >>
+      Proof.get >>= fun step ->
+      Proof.set {step with comb=goals} >>
       tclDISPATCHGEN null join tacs env >>= fun x ->
-      Inner.get >>= fun step' ->
-      Inner.set {step' with comb=step.comb@step'.comb} >>
-      Inner.return (join y x)
+      Proof.get >>= fun step' ->
+      Proof.set {step' with comb=step.comb@step'.comb} >>
+      Proof.return (join y x)
   | _ , _ -> tclZERO SizeMismatch env
 
 let unitK () () = ()
@@ -338,8 +345,8 @@ let extend_to_list =
     startxs@(copy (n-ne-ns) rx endxs)
 let tclEXTEND tacs1 rtac tacs2 env =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
-  let (>>=) = Inner.bind in
-  Inner.get >>= fun step ->
+  let (>>=) = Proof.bind in
+  Proof.get >>= fun step ->
   let tacs = extend_to_list tacs1 rtac tacs2 step.comb in
   tclDISPATCH tacs env
 
@@ -362,20 +369,20 @@ let sensitive_on_proofview s env step =
      comb = List.flatten combed_subgoals; }
   let tclSENSITIVE s env =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
-  let (>>=) = Inner.bind in
-  Inner.get >>= fun step ->
+  let (>>=) = Proof.bind in
+  Proof.get >>= fun step ->
   try
     let next = sensitive_on_proofview s env step in
-    Inner.set next
+    Proof.set next
   with e when Errors.noncritical e ->
     tclZERO e env
 
 let tclPROGRESS t env =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
-  let (>>=) = Inner.bind in
-  Inner.get >>= fun initial ->
+  let (>>=) = Proof.bind in
+  Proof.get >>= fun initial ->
   t env >>= fun res ->
-  Inner.get >>= fun final ->
+  Proof.get >>= fun final ->
   let test =
     Evd.progress_evar_map initial.solution final.solution &&
     not (Util.List.for_all2eq (fun i f -> Goal.equal initial.solution i final.solution f) initial.comb final.comb)
@@ -387,14 +394,17 @@ let tclPROGRESS t env =
 
 let tclEVARMAP _ =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
-  let (>>=) = Inner.bind in
-  Inner.get >>= fun initial ->
-  Inner.return (initial.solution)
+  let (>>=) = Proof.bind in
+  Proof.get >>= fun initial ->
+  Proof.return (initial.solution)
 
 let tclENV env =
-  Inner.return env
+  Proof.return env
+
+let tclTIMEOUT n t env = Proof.timeout n (t env)
 
-let tclTIMEOUT n t env = Inner.timeout n (t env)
+let mark_as_unsafe env =
+  Proof.lift (Message.put false)
 
 (*** Commands ***)
 
@@ -450,8 +460,8 @@ module V82 = struct
     (* spiwack: we ignore the dependencies between goals here, expectingly
        preserving the semantics of <= 8.2 tactics *)
     (* spiwack: convenience notations, waiting for ocaml 3.12 *)
-    let (>>=) = Inner.bind in
-    Inner.get >>= fun ps ->
+    let (>>=) = Proof.bind in
+    Proof.get >>= fun ps ->
     try
       let tac evd gl = 
         let glsigma  =
@@ -466,7 +476,7 @@ module V82 = struct
       in
       let (goalss,evd) = Goal.list_map tac initgoals initevd in
       let sgs = List.flatten goalss in
-      Inner.set { ps with solution=evd ; comb=sgs; }
+      Proof.set { ps with solution=evd ; comb=sgs; }
     with e when Errors.noncritical e ->
       tclZERO e env
 
@@ -516,9 +526,11 @@ module V82 = struct
 
   let of_tactic t gls =
     let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] ; initial = [] } in
-    let (_,final) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in
+    let (_,final,_) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in
     { Evd.sigma = final.solution ; it = final.comb }
 
+  let put_status b _env =
+    Proof.lift (Message.put b)
 end
 
 
@@ -528,17 +540,17 @@ module Goal = struct
 
   let lift s env =
     (* spiwack: convenience notations, waiting for ocaml 3.12 *)
-    let (>>=) = Inner.bind in
-    let (>>) = Inner.seq in
-    Inner.get >>= fun step ->
+    let (>>=) = Proof.bind in
+    let (>>) = Proof.seq in
+    Proof.get >>= fun step ->
     try
       let (res,sigma) =
         Goal.list_map begin fun sigma g ->
           Goal.eval s env sigma g
         end step.comb step.solution
       in
-      Inner.set { step with solution=sigma } >>
-        Inner.return res
+      Proof.set { step with solution=sigma } >>
+        Proof.return res
     with e when Errors.noncritical e ->
       tclZERO e env
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index d2db5be9a3..4536180e2e 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -118,7 +118,9 @@ val unfocus : focus_context -> proofview -> proofview
 type +'a tactic 
 
 (* Applies a tactic to the current proofview. *)
-val apply : Environ.env -> 'a tactic -> proofview -> 'a * proofview
+(* the return boolean signals the use of an unsafe tactic, in which
+   case it is [false]. *)
+val apply : Environ.env -> 'a tactic -> proofview -> 'a * proofview * bool
 
 (*** tacticals ***)
 
@@ -198,6 +200,9 @@ val tclENV : Environ.env tactic
       In case of timeout if fails with [tclZERO Timeout]. *)
 val tclTIMEOUT : int -> 'a tactic -> 'a tactic
 
+(** [mark_as_unsafe] signals that the current tactic is unsafe. *)
+val mark_as_unsafe : unit tactic
+
 val list_map : ('a -> 'b tactic) -> 'a list -> 'b list tactic
 
 (*** Commands ***)
@@ -260,6 +265,9 @@ module V82 : sig
      should be avoided as much as possible.  It should work as
      expected for a tactic obtained from {!V82.tactic} though. *)
   val of_tactic : 'a tactic -> tac
+
+  (* marks as unsafe if the argument is [false] *)
+  val put_status : bool -> unit tactic
 end
 
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a383b14528..9edf6302da 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -785,5 +785,5 @@ END;;
 VERNAC COMMAND EXTEND GrabEvars
 [ "Grab" "Existential" "Variables" ]
   => [ Vernacexpr.VtProofStep, Vernacexpr.VtLater ]
-  -> [ Proof_global.with_current_proof (fun _ p  -> Proof.V82.grab_evars p) ]
+  -> [ Proof_global.simple_with_current_proof (fun _ p  -> Proof.V82.grab_evars p) ]
 END
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index f889f9cb2c..846bba1d46 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -146,21 +146,20 @@ TACTIC EXTEND setoid_rewrite
       [ Proofview.V82.tactic (cl_rewrite_clause c o (occurrences_of occ) (Some id))]
 END
 
-let cl_rewrite_clause_newtac_tac c o occ cl gl =
-  cl_rewrite_clause_newtac' c o occ cl;
-  tclIDTAC gl
+let cl_rewrite_clause_newtac_tac c o occ cl =
+  cl_rewrite_clause_newtac' c o occ cl
 
 TACTIC EXTEND GenRew
 | [ "rew" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ) ] ->
-    [ Proofview.V82.tactic (cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id)) ]
+    [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id) ]
 | [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id) ] ->
-    [ Proofview.V82.tactic (cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id)) ]
+    [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id) ]
 | [ "rew" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] ->
-    [ Proofview.V82.tactic (cl_rewrite_clause_newtac_tac c o AllOccurrences (Some id)) ]
+    [ cl_rewrite_clause_newtac_tac c o AllOccurrences (Some id) ]
 | [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] ->
-    [ Proofview.V82.tactic (cl_rewrite_clause_newtac_tac c o (occurrences_of occ) None) ]
+    [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) None ]
 | [ "rew" orient(o) glob_constr_with_bindings(c) ] ->
-    [ Proofview.V82.tactic (cl_rewrite_clause_newtac_tac c o AllOccurrences None) ]
+    [ cl_rewrite_clause_newtac_tac c o AllOccurrences None ]
 END
 
 VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 06b067fcf4..04819830e5 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -198,8 +198,8 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   *)
   let pf = Proof.start [invEnv,invGoal] in
   let pf =
-    Proof.run_tactic env (
-      Tacticals.New.tclTHEN intro (Tacticals.New.onLastHypId inv_op)) pf
+    fst (Proof.run_tactic env (
+      Tacticals.New.tclTHEN intro (Tacticals.New.onLastHypId inv_op)) pf)
   in
   let pfterm = List.hd (Proof.partial_proof pf) in
   let global_named_context = Global.named_context () in
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 30fe8d4aef..66b2c64b0f 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -361,7 +361,7 @@ let solve_remaining_by by env prf =
     let evd' = 
       List.fold_right (fun mv evd ->
         let ty = Clenv.clenv_nf_meta env (meta_type evd mv) in
-	let c = Pfedit.build_by_tactic env.env ty (Tacticals.New.tclCOMPLETE tac) in
+	let c,_ = Pfedit.build_by_tactic env.env ty (Tacticals.New.tclCOMPLETE tac) in
 	  meta_assign mv (c, (Conv,TypeNotProcessed)) evd)
       indep env.evd
     in { env with evd = evd' }, prf
@@ -1342,9 +1342,8 @@ let cl_rewrite_clause_new_strat ?abs strat clause =
    newfail 0 (str"setoid rewrite failed: " ++ s))
 
 let cl_rewrite_clause_newtac' l left2right occs clause =
-  Proof_global.with_current_proof (fun _ -> Proof.run_tactic (Global.env ())
-    (Proofview.tclFOCUS 1 1 
-       (cl_rewrite_clause_new_strat (rewrite_with rewrite_unif_flags l left2right occs) clause)))
+  Proofview.tclFOCUS 1 1 
+       (cl_rewrite_clause_new_strat (rewrite_with rewrite_unif_flags l left2right occs) clause)
 
 let cl_rewrite_clause_strat strat clause =
   tclTHEN (tactic_init_setoid ())
@@ -1641,7 +1640,7 @@ let add_morphism_infer glob m n =
 				   glob (ConstRef cst));
 		  declare_projection n instance_id (ConstRef cst)
 		| _ -> assert false);
-	    Pfedit.by (Tacinterp.interp tac)) ()
+	    ignore (Pfedit.by (Tacinterp.interp tac))) ()
 
 let add_morphism glob binders m s n =
   init_setoid ();
diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli
index 637bab5a6a..63166c64a5 100644
--- a/tactics/rewrite.mli
+++ b/tactics/rewrite.mli
@@ -43,7 +43,7 @@ val cl_rewrite_clause :
 
 val cl_rewrite_clause_newtac' :
   interp_sign * (glob_constr_and_expr * glob_constr_and_expr bindings) ->
-  bool -> Locus.occurrences -> Id.t option -> unit
+  bool -> Locus.occurrences -> Id.t option -> unit Proofview.tactic
 
 val is_applied_rewrite_relation :
   env -> evar_map -> Context.rel_context -> constr -> types option
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5b1ae69e33..4026b42587 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3740,7 +3740,8 @@ let abstract_subproof id tac gl =
     try flush_and_check_evars (project gl) concl
     with Uninstantiated_evar _ ->
       error "\"abstract\" cannot handle existentials." in
-  let const = Pfedit.build_constant_by_tactic id secsign concl
+  (* spiwack: the [abstract] tacticals loses the "unsafe status" information *)
+  let (const,_) = Pfedit.build_constant_by_tactic id secsign concl
     (Tacticals.New.tclCOMPLETE (Tacticals.New.tclTHEN (Tacticals.New.tclDO (List.length sign) intro) tac)) in
   let cd = Entries.DefinitionEntry const in
   let decl = (cd, IsProof Lemma) in
@@ -3764,9 +3765,9 @@ let tclABSTRACT name_op tac gl =
 
 
 let admit_as_an_axiom =
-  (* spiwack: admit temporarily won't report an unsafe status *)
   Proofview.tclUNIT () >= fun () -> (* delay for Coqlib.build_coq_proof_admitted *)
-  simplest_case (Coqlib.build_coq_proof_admitted ())
+  simplest_case (Coqlib.build_coq_proof_admitted ()) <*>
+  Proofview.mark_as_unsafe
 
 let unify ?(state=full_transparent_state) x y gl =
   try
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index f35a346335..50d0130445 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -626,8 +626,8 @@ let make_bl_scheme mind =
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in
-  [|Pfedit.build_by_tactic (Global.env()) bl_goal
-    (compute_bl_tact (!bl_scheme_kind_aux()) ind lnamesparrec nparrec)|],
+  [|fst (Pfedit.build_by_tactic (Global.env()) bl_goal
+    (compute_bl_tact (!bl_scheme_kind_aux()) ind lnamesparrec nparrec))|],
   eff
 
 let bl_scheme_kind = declare_mutual_scheme_object "_dec_bl" make_bl_scheme
@@ -741,8 +741,8 @@ let make_lb_scheme mind =
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in
-  [|Pfedit.build_by_tactic (Global.env()) lb_goal
-    (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)|],
+  [|fst (Pfedit.build_by_tactic (Global.env()) lb_goal
+    (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec))|],
   eff
 
 let lb_scheme_kind = declare_mutual_scheme_object "_dec_lb" make_lb_scheme
@@ -903,9 +903,9 @@ let make_eq_decidability mind =
   let nparrec = mib.mind_nparams_rec in
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
-  [|Pfedit.build_by_tactic (Global.env())
+  [|fst (Pfedit.build_by_tactic (Global.env())
     (compute_dec_goal ind lnamesparrec nparrec)
-    (compute_dec_tact ind lnamesparrec nparrec)|], Declareops.no_seff
+    (compute_dec_tact ind lnamesparrec nparrec))|], Declareops.no_seff
 
 let eq_dec_scheme_kind =
   declare_mutual_scheme_object "_eq_dec" make_eq_decidability
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 121f8f4e1a..728baadb41 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -298,11 +298,12 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 	       (fun () ->
 		Lemmas.start_proof id kind termtype
 		(fun _ -> instance_hook k pri global imps ?hook);
+                 (* spiwack: I don't know what to do with the status here. *)
 		if not (Option.is_empty term) then 
-		  Pfedit.by (!refine_ref (evm, Option.get term))
+		  ignore (Pfedit.by (!refine_ref (evm, Option.get term)))
 		else if Flags.is_auto_intros () then
-		  Pfedit.by (Tacticals.New.tclDO len Tactics.intro);
-		(match tac with Some tac -> Pfedit.by tac | None -> ())) ();
+		  ignore (Pfedit.by (Tacticals.New.tclDO len Tactics.intro));
+		(match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) ();
 	       id)
 	end)
 	
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 13e12b7e15..3eb61ccdf3 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -761,7 +761,8 @@ let rec string_of_list sep f = function
 (* Solve an obligation using tactics, return the corresponding proof term *)
 let solve_by_tac evi t =
   let id = Id.of_string "H" in
-  let entry = Pfedit.build_constant_by_tactic 
+  (* spiwack: the status is dropped *)
+  let (entry,_) = Pfedit.build_constant_by_tactic 
     id ~goal_kind evi.evar_hyps evi.evar_concl (Tacticals.New.tclCOMPLETE t) in
   let env = Global.env () in
   let entry = Term_typing.handle_side_effects env entry in
@@ -814,7 +815,7 @@ let rec solve_obligation prg num tac =
 		  | _ -> ());
 	    trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
 		     Printer.pr_constr_env (Global.env ()) obl.obl_type);
-	    Pfedit.by (snd (get_default_tactic ()));
+	    ignore (Pfedit.by (snd (get_default_tactic ())));
 	    Option.iter (fun tac -> Pfedit.set_end_tac tac) tac
       | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
 		      ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a0a355a154..62243781ae 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -475,8 +475,9 @@ let vernac_end_proof ?proof = function
 let vernac_exact_proof c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the begining of a proof. *)
-  by (Tactics.New.exact_proof c);
-  save_named true
+  let status = by (Tactics.New.exact_proof c) in
+  save_named true;
+  if not status then Pp.feedback Interface.AddedAxiom
 
 let vernac_assumption locality (local, kind) l nl =
   let local = enforce_locality_exp locality local in
@@ -774,15 +775,16 @@ let focus_command_cond = Proof.no_cond command_focus
 let vernac_solve n tcom b =
   if not (refining ()) then
     error "Unknown command of the non proof-editing mode.";
-  Proof_global.with_current_proof (fun etac p ->
+  let status = Proof_global.with_current_proof (fun etac p ->
     let with_end_tac = if b then Some etac else None in
-    let p = solve_nth n (Tacinterp.hide_interp tcom None) ?with_end_tac p in
+    let (p,status) = solve_nth n (Tacinterp.hide_interp tcom None) ?with_end_tac p in
     (* in case a strict subtree was completed,
        go back to the top of the prooftree *)
     let p = Proof.maximal_unfocus command_focus p in
-    p);
-    print_subgoals()
-;;
+    p,status) in
+    print_subgoals();
+    if not status then Pp.feedback Interface.AddedAxiom
+ 
 
   (* A command which should be a tactic. It has been
      added by Christine to patch an error in the design of the proof
@@ -1486,7 +1488,7 @@ let vernac_register id r =
 (* Proof management *)
 
 let vernac_focus gln =
-  Proof_global.with_current_proof (fun _ p ->
+  Proof_global.simple_with_current_proof (fun _ p ->
     match gln with
       | None -> Proof.focus focus_command_cond () 1 p
       | Some 0 ->
@@ -1497,7 +1499,7 @@ let vernac_focus gln =
 
   (* Unfocuses one step in the focus stack. *)
 let vernac_unfocus () =
-  Proof_global.with_current_proof (fun _ p -> Proof.unfocus command_focus p ());
+  Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus command_focus p ());
   print_subgoals ()
 
 (* Checks that a proof is fully unfocused. Raises an error if not. *)
@@ -1519,19 +1521,19 @@ let subproof_kind = Proof.new_focus_kind ()
 let subproof_cond = Proof.done_cond subproof_kind
 
 let vernac_subproof gln =
-  Proof_global.with_current_proof (fun _ p ->
+  Proof_global.simple_with_current_proof (fun _ p ->
     match gln with
     | None -> Proof.focus subproof_cond () 1 p
     | Some n -> Proof.focus subproof_cond () n p);
   print_subgoals ()
 
 let vernac_end_subproof () =
-  Proof_global.with_current_proof (fun _ p -> Proof.unfocus subproof_kind p ());
+  Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus subproof_kind p ());
   print_subgoals ()
 
 
 let vernac_bullet (bullet:Proof_global.Bullet.t) =
-  Proof_global.with_current_proof (fun _ p ->
+  Proof_global.simple_with_current_proof (fun _ p ->
     Proof_global.Bullet.put p bullet);
   (* Makes the focus visible in emacs by re-printing the goal. *)
   if !Flags.print_emacs then print_subgoals ()