Merge PR #9173: [tactics] Remove dependency of abstract on global proof state.

Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: mattam82
Ack-by: maximedenes
Reviewed-by: ppedrot

1 files changed, 13 insertions, 4 deletions

diff --git a/engine/proofview.mli b/engine/proofview.mli
index 286703c0dc..680a93f0cc 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -156,10 +156,15 @@ type +'a tactic
     tactic has given up. In case of multiple success the first one is
     selected. If there is no success, fails with
     {!Logic_monad.TacticFailure}*)
-val apply : Environ.env -> 'a tactic -> proofview -> 'a
-                                                   * proofview
-                                                   * (bool*Evar.t list*Evar.t list)
-                                                   * Proofview_monad.Info.tree
+val apply
+  :  name:Names.Id.t
+  -> poly:bool
+  -> Environ.env
+  -> 'a tactic
+  -> proofview
+  -> 'a * proofview
+       * (bool*Evar.t list*Evar.t list)
+       * Proofview_monad.Info.tree
 
 (** {7 Monadic primitives} *)
 
@@ -407,6 +412,10 @@ val tclTIMEOUT : int -> 'a tactic -> 'a tactic
     identifying annotation if present *)
 val tclTIME : string option -> 'a tactic -> 'a tactic
 
+(** Internal, don't use. *)
+val tclProofInfo : (Names.Id.t * bool) tactic
+[@@ocaml.deprecated "internal, don't use"]
+
 (** {7 Unsafe primitives} *)
 
 (** The primitives in the [Unsafe] module should be avoided as much as