[printing] Deprecate all printing functions accessing the global proof.

We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.

We also adapt most of the code, making more explicit where the
printing environment is coming from.

An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.

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