[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.

2 files changed, 15 insertions, 15 deletions

diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 05ab8ab32..a7d6d5bb2 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -82,10 +82,11 @@ VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
   | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [
     Feedback.msg_notice (strbrk "The following ring structures have been declared:");
     Spmap.iter (fun fn fi ->
+      let sigma, env = Pfedit.get_current_context () in
       Feedback.msg_notice (hov 2
         (Ppconstr.pr_id (Libnames.basename fn)++spc()++
-          str"with carrier "++ pr_constr fi.ring_carrier++spc()++
-          str"and equivalence relation "++ pr_constr fi.ring_req))
+          str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++
+          str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req))
     ) !from_name ]
 END
 
@@ -117,10 +118,11 @@ VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
 | [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [
     Feedback.msg_notice (strbrk "The following field structures have been declared:");
     Spmap.iter (fun fn fi ->
+      let sigma, env = Pfedit.get_current_context () in
       Feedback.msg_notice (hov 2
         (Ppconstr.pr_id (Libnames.basename fn)++spc()++
-          str"with carrier "++ pr_constr fi.field_carrier++spc()++
-          str"and equivalence relation "++ pr_constr fi.field_req))
+          str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++
+          str"and equivalence relation "++ pr_constr_env env sigma fi.field_req))
     ) !field_from_name ]
 END
 
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 9e4b896f8..1c3bdb958 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -344,8 +344,6 @@ let _ = add_map "ring"
 (****************************************************************************)
 (* Ring database *)
 
-let pr_constr c = pr_econstr c
-
 module Cmap = Map.Make(Constr)
 
 let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"
@@ -368,7 +366,7 @@ let find_ring_structure env sigma l =
         with Not_found ->
           CErrors.user_err ~hdr:"ring"
             (str"cannot find a declared ring structure over"++
-             spc()++str"\""++pr_constr ty++str"\""))
+             spc() ++ str"\"" ++ pr_econstr_env env sigma ty ++ str"\""))
     | [] -> assert false
 
 let add_entry (sp,_kn) e =
@@ -529,19 +527,19 @@ let ring_equality env evd (r,add,mul,opp,req) =
 		  op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in
 		  Flags.if_verbose
 		    Feedback.msg_info
-		    (str"Using setoid \""++pr_constr req++str"\""++spc()++
-			str"and morphisms \""++pr_constr add_m_lem ++
-			str"\","++spc()++ str"\""++pr_constr mul_m_lem++
-			str"\""++spc()++str"and \""++pr_constr opp_m_lem++
+                    (str"Using setoid \""++ pr_econstr_env env !evd req++str"\""++spc()++
+                        str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++
+                        str"\","++spc()++ str"\""++pr_econstr_env env !evd mul_m_lem++
+                        str"\""++spc()++str"and \""++pr_econstr_env env !evd opp_m_lem++
 			str"\"");
 		  op_morph)
             | None ->
 		(Flags.if_verbose
 		    Feedback.msg_info
-		    (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++
-			str"and morphisms \""++pr_constr add_m_lem ++
+                    (str"Using setoid \""++pr_econstr_env env !evd req ++str"\"" ++ spc() ++
+                        str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++
 			str"\""++spc()++str"and \""++
-			pr_constr mul_m_lem++str"\"");
+                        pr_econstr_env env !evd mul_m_lem++str"\"");
 		 op_smorph r add mul req add_m_lem mul_m_lem) in
           (setoid,op_morph)
 
@@ -861,7 +859,7 @@ let find_field_structure env sigma l =
         with Not_found ->
           CErrors.user_err ~hdr:"field"
             (str"cannot find a declared field structure over"++
-             spc()++str"\""++pr_constr ty++str"\""))
+             spc()++str"\""++pr_econstr_env env sigma ty++str"\""))
     | [] -> assert false
 
 let add_field_entry (sp,_kn) e =