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, 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