Merge PR #9678: Stop accessing proof env via Pfedit in printers

Ack-by: JasonGross
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

1 files changed, 20 insertions, 20 deletions

diff --git a/plugins/setoid_ring/g_newring.mlg b/plugins/setoid_ring/g_newring.mlg
index f59ca4cef4..3ce6478700 100644
--- a/plugins/setoid_ring/g_newring.mlg
+++ b/plugins/setoid_ring/g_newring.mlg
@@ -38,24 +38,24 @@ END
 open Pptactic
 open Ppconstr
 
-let pr_ring_mod = function
-  | Ring_kind (Computational eq_test) -> str "decidable" ++ pr_arg pr_constr_expr eq_test
+let pr_ring_mod env sigma = function
+  | Ring_kind (Computational eq_test) -> str "decidable" ++ pr_arg (pr_constr_expr env sigma) eq_test
   | Ring_kind Abstract ->  str "abstract"
-  | Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg pr_constr_expr morph
-  | Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]"
+  | Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg (pr_constr_expr env sigma) morph
+  | Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma cst_tac ++ str "]"
   | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]"
-  | Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]"
-  | Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]"
-  | Setoid(sth,ext) -> str "setoid" ++ pr_arg pr_constr_expr sth ++ pr_arg pr_constr_expr ext
-  | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]"
-  | Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]"
-  | Sign_spec t -> str "sign" ++ pr_arg pr_constr_expr t
-  | Div_spec t -> str "div" ++ pr_arg pr_constr_expr t
+  | Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma t ++ str "]"
+  | Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma t ++ str "]"
+  | Setoid(sth,ext) -> str "setoid" ++ pr_arg (pr_constr_expr env sigma) sth ++ pr_arg (pr_constr_expr env sigma) ext
+  | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg (pr_constr_expr env sigma) spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]"
+  | Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg (pr_constr_expr env sigma) spec ++ spc () ++ str "[" ++ pr_raw_tactic env sigma cst_tac ++ str "]"
+  | Sign_spec t -> str "sign" ++ pr_arg (pr_constr_expr env sigma) t
+  | Div_spec t -> str "div" ++ pr_arg (pr_constr_expr env sigma) t
 
 }
 
 VERNAC ARGUMENT EXTEND ring_mod
-  PRINTED BY { pr_ring_mod }
+  PRINTED BY { pr_ring_mod env sigma }
   | [ "decidable" constr(eq_test) ] -> { Ring_kind(Computational eq_test) }
   | [ "abstract" ] -> { Ring_kind Abstract }
   | [ "morphism" constr(morph) ] -> { Ring_kind(Morphism morph) }
@@ -74,12 +74,12 @@ END
 
 {
 
-let pr_ring_mods l = surround (prlist_with_sep pr_comma pr_ring_mod l)
+let pr_ring_mods env sigma l = surround (prlist_with_sep pr_comma (pr_ring_mod env sigma) l)
 
 }
 
 VERNAC ARGUMENT EXTEND ring_mods
-  PRINTED BY { pr_ring_mods }
+  PRINTED BY { pr_ring_mods env sigma }
   | [ "(" ne_ring_mod_list_sep(mods, ",") ")" ] -> { mods }
 END
 
@@ -104,26 +104,26 @@ END
 
 {
 
-let pr_field_mod = function
-  | Ring_mod m -> pr_ring_mod m
-  | Inject inj -> str "completeness" ++ pr_arg pr_constr_expr inj
+let pr_field_mod env sigma = function
+  | Ring_mod m -> pr_ring_mod env sigma m
+  | Inject inj -> str "completeness" ++ pr_arg (pr_constr_expr env sigma) inj
 
 }
 
 VERNAC ARGUMENT EXTEND field_mod
-  PRINTED BY { pr_field_mod }
+  PRINTED BY { pr_field_mod env sigma }
   | [ ring_mod(m) ] -> { Ring_mod m }
   | [ "completeness" constr(inj) ] -> { Inject inj }
 END
 
 {
 
-let pr_field_mods l = surround (prlist_with_sep pr_comma pr_field_mod l)
+let pr_field_mods env sigma l = surround (prlist_with_sep pr_comma (pr_field_mod env sigma) l)
 
 }
 
 VERNAC ARGUMENT EXTEND field_mods
-  PRINTED BY { pr_field_mods }
+  PRINTED BY { pr_field_mods env sigma }
   | [ "(" ne_field_mod_list_sep(mods, ",") ")" ] -> { mods }
 END