From 27d453641446b3d35aa2211b94f949b57a88ebb2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 1 Mar 2019 15:27:05 +0100
Subject: Stop accessing proof env via Pfedit in printers

This should make https://github.com/coq/coq/pull/9129 easier.
---
 plugins/btauto/refl_btauto.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/btauto')

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 4d817625f5..1bdedcaf26 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -196,7 +196,7 @@ module Btauto = struct
         let assign = List.combine penv var in
         let map_msg (key, v) =
           let b = if v then str "true" else str "false" in
-          let sigma, env = Pfedit.get_current_context () in
+          let sigma, env = Tacmach.project gl, Tacmach.pf_env gl in
           let term = Printer.pr_constr_env env sigma key in
           term ++ spc () ++ str ":=" ++ spc () ++ b
         in
-- 
cgit v1.2.3