[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, 19 insertions, 2 deletions

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 525ff7fd0f..62906303a4 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -530,7 +530,15 @@ let interp_gen kind ist pattern_mode flags env sigma c =
       invariant that running the tactic returned by push_trace does
       not modify sigma. *)
   let (_, dummy_proofview) = Proofview.init sigma [] in
-  let (trace,_,_,_) = Proofview.apply env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in
+
+  (* Again this is called at times with no open proof! *)
+  let name, poly =
+    try
+      let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in
+      name, poly
+    with | Proof_global.NoCurrentProof -> Id.of_string "tacinterp", false
+  in
+  let (trace,_,_,_) = Proofview.apply ~name ~poly env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in
   let (evd,c) =
     catch_error trace (understand_ltac flags env sigma vars kind) term
   in
@@ -2041,7 +2049,16 @@ let _ =
     let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
     let ist = { lfun = lfun; extra; } in
     let tac = interp_tactic ist tac in
-    let name, poly = Id.of_string "ltac_sub", false in
+    (* XXX: This depends on the global state which is bad; the hooking
+       mechanism should be modified. *)
+    let name, poly =
+      try
+        let (_, poly, _) = Proof_global.get_current_persistence () in
+        let name = Proof_global.get_current_proof_name () in
+        name, poly
+      with | Proof_global.NoCurrentProof ->
+        Id.of_string "ltac_gen", false
+    in
     let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in
     (EConstr.of_constr c, sigma)
   in