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.
---
 engine/proofview_monad.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine/proofview_monad.mli')

diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index 9d75242175..a08cab3bf6 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -45,7 +45,7 @@ end
 
 (** We typically label nodes of [Trace.tree] with messages to
     print. But we don't want to compute the result. *)
-type lazy_msg = unit -> Pp.t
+type lazy_msg = Environ.env -> Evd.evar_map -> Pp.t
 
 (** Info trace. *)
 module Info : sig
@@ -60,7 +60,7 @@ module Info : sig
   type state = tag Trace.incr
   type tree = tag Trace.forest
 
-  val print : tree -> Pp.t
+  val print : Environ.env -> Evd.evar_map -> tree -> Pp.t
 
   (** [collapse n t] flattens the first [n] levels of [Tactic] in an
       info trace, effectively forgetting about the [n] top level of
-- 
cgit v1.2.3