Merge PR #8500: [api] Deprecate two forgotten print functions that use global state.

2 files changed, 8 insertions, 7 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index 5b3ead181f..f0ea6532de 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -930,8 +930,8 @@ let pr_assumptionset env sigma s =
 	let mp,_,lab = Constant.repr3 kn in
         str (ModPath.to_string mp) ++ str "." ++ Label.print lab
     in
-    let safe_pr_ltype typ =
-      try str " : " ++ pr_ltype typ
+    let safe_pr_ltype env sigma typ =
+      try str " : " ++ pr_ltype_env env sigma typ
       with e when CErrors.noncritical e -> mt ()
     in
     let safe_pr_ltype_relctx (rctx, typ) =
@@ -942,7 +942,7 @@ let pr_assumptionset env sigma s =
     let pr_axiom env ax typ =
       match ax with
       | Constant kn ->
-          safe_pr_constant env kn ++ safe_pr_ltype typ
+          safe_pr_constant env kn ++ safe_pr_ltype env sigma typ
       | Positive m ->
           hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.")
       | Guarded kn ->
@@ -952,7 +952,7 @@ let pr_assumptionset env sigma s =
       let (v, a, o, tr) = accu in
       match t with
       | Variable id ->
-        let var = pr_id id ++ str " : " ++ pr_ltype typ in
+        let var = pr_id id ++ str " : " ++ pr_ltype_env env sigma typ in
         (var :: v, a, o, tr)
       | Axiom (axiom, []) ->
         let ax = pr_axiom env axiom typ in
@@ -966,10 +966,10 @@ let pr_assumptionset env sigma s =
           l in
         (v, ax :: a, o, tr)
       | Opaque kn ->
-        let opq = safe_pr_constant env kn ++ safe_pr_ltype typ in
+        let opq = safe_pr_constant env kn ++ safe_pr_ltype env sigma typ in
         (v, a, opq :: o, tr)
       | Transparent kn ->
-        let tran = safe_pr_constant env kn ++ safe_pr_ltype typ in
+        let tran = safe_pr_constant env kn ++ safe_pr_ltype env sigma typ in
         (v, a, o, tran :: tr)
     in
     let (vars, axioms, opaque, trans) = 
diff --git a/printing/printer.mli b/printing/printer.mli
index 971241d5f9..428dced117 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -200,13 +200,14 @@ val pr_ne_evar_set         : Pp.t -> Pp.t -> evar_map ->
   Evar.Set.t -> Pp.t
 
 val pr_prim_rule           : prim_rule -> Pp.t
+[@@ocaml.deprecated "[pr_prim_rule] is scheduled to be removed along with the legacy proof engine"]
 
 val print_and_diff : Proof.t option -> Proof.t option -> unit
 
 (** Backwards compatibility *)
 
 val prterm                 : constr -> Pp.t (** = pr_lconstr *)
-
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 (** Declarations for the "Print Assumption" command *)
 type axiom =