[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, 4 insertions, 3 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index b98b10315..cee6d4bea 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -464,15 +464,16 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
       in
       let tac = run_hint t tac in
       let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in
+      let _, env = Pfedit.get_current_context () in
       let pp =
         match p with
         | Some pat when get_typeclasses_filtered_unification () ->
-           str " with pattern " ++ Printer.pr_constr_pattern pat
+           str " with pattern " ++ Printer.pr_constr_pattern_env env sigma pat
         | _ -> mt ()
       in
         match repr_hint t with
-        | Extern _ -> (tac, b, true, name, lazy (pr_hint t ++ pp))
-        | _ -> (tac, b, false, name, lazy (pr_hint t ++ pp))
+        | Extern _ -> (tac, b, true, name, lazy (pr_hint env sigma t ++ pp))
+        | _ -> (tac, b, false, name, lazy (pr_hint env sigma t ++ pp))
   in List.map tac_of_hint hintl
 
 and e_trivial_resolve db_list local_db secvars only_classes sigma concl =