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

9 files changed, 227 insertions, 82 deletions

diff --git a/proofs/monads.ml b/proofs/monads.ml
index ba1440864..803715a45 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 55c46a340..6c0ddfc11 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 3a0c25c46..73f12db98 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 89f3638a1..3a00d76f0 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 fa6007061..66aee0313 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 3f84f6500..5e11cfdb2 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 9b5015e0c..867010fb0 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 3f80da785..a3791e7a4 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 d2db5be9a..4536180e2 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