Merge PR #9139: [engine] Allow debug printers to access the environment.

1 files changed, 5 insertions, 2 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index e2b7df19de..7f1ae6d12b 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -107,11 +107,14 @@ let solve ?with_end_tac gi info_lvl tac pr =
         Proofview.tclTHEN tac Refine.solve_constraints
       else tac
     in
-    let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac pr in
+    let env = Global.env () in
+    let (p,(status,info)) = Proof.run_tactic env tac pr in
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
     let () =
       match info_lvl with
       | None -> ()
-      | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
+      | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info env sigma ~lvl:i info))
     in
     (p,status)
   with