[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, 6 insertions, 3 deletions

diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 69341d97df..80eb9d0124 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -177,7 +177,7 @@ module P = struct
   type s = proofview * Environ.env
 
   (** Recording info trace (true) or not. *)
-  type e = bool
+  type e = { trace: bool; name : Names.Id.t; poly : bool }
 
   (** Status (safe/unsafe) * shelved goals * given up *)
   type w = bool * goal list
@@ -254,13 +254,16 @@ end
 
 (** Lens and utilies pertaining to the info trace *)
 module InfoL = struct
-  let recording = Logical.current
+  let recording = Logical.(map (fun {P.trace} -> trace) current)
   let if_recording t =
     let open Logical in
     recording >>= fun r ->
     if r then t else return ()
 
-  let record_trace t = Logical.local true t
+  let record_trace t =
+    Logical.(
+      current >>= fun s ->
+      local {s with P.trace = true} t)
 
   let raw_update = Logical.update
   let update f = if_recording (raw_update f)