[tactics] Remove dependency of abstract on global proof state.

In order to do so we place the polymorphic status and name in the
read-only part of the monad.

Note the added comments, as well as the fact that almost no part of
tactics depends on `proofs` nor `interp`, thus they should be placed
just after pretyping.

Gaëtan Gilbert noted that ideally, abstract should not depend on the
polymorphic status, should we be able to defer closing of the
constant, however this will require significant effort.

Also, we may deprecate nameless abstract, thus rending both of the
changes this PR need unnecessary.

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