From 1499565d4ef1165d34b5bbb927e52a754903e077 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 5 Dec 2018 02:49:07 +0100
Subject: [engine] Allow debug printers to access the environment.

This should improve correctness and will be needed for the PRs that
remove global access to the proof state.
---
 proofs/refine.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs/refine.ml')

diff --git a/proofs/refine.ml b/proofs/refine.ml
index d812a8cad7..1d796fece5 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -107,8 +107,8 @@ let generic_refine ~typecheck f gl =
   (* Mark goals *)
   let sigma = Proofview.Unsafe.mark_as_goals sigma comb in
   let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in
-  let trace () = Pp.(hov 2 (str"simple refine"++spc()++
-                            Termops.Internal.print_constr_env env sigma c)) in
+  let trace env sigma = Pp.(hov 2 (str"simple refine"++spc()++
+                                   Termops.Internal.print_constr_env env sigma c)) in
   Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v ->
   Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*>
   Proofview.Unsafe.tclEVARS sigma <*>
-- 
cgit v1.2.3