Merge PR #6173: [printing] Deprecate all printing functions accessing the global proof.

1 files changed, 2 insertions, 1 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index da8955f0d7..a09abfa193 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -200,7 +200,8 @@ module Btauto = struct
         let assign = List.combine env var in
         let map_msg (key, v) =
           let b = if v then str "true" else str "false" in
-          let term = Printer.pr_constr key in
+          let sigma, env = Pfedit.get_current_context () in
+          let term = Printer.pr_constr_env env sigma key in
           term ++ spc () ++ str ":=" ++ spc () ++ b
         in
         let assign = List.map map_msg assign in