4 files changed, 25 insertions, 25 deletions
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index dba72337b2..f5d13053b1 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -1789,5 +1789,5 @@ End Field.
 
 End Complete.
 
-Arguments FEO [C].
-Arguments FEI [C].
+Arguments FEO {C}.
+Arguments FEI {C}.
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index 9ef24144d2..12f716c496 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -1507,5 +1507,5 @@ Qed.
 
 End MakeRingPol.
 
-Arguments PEO [C].
-Arguments PEI [C].
+Arguments PEO {C}.
+Arguments PEI {C}.
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
 
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 65201d922f..3f69701bd3 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -153,7 +153,7 @@ let decl_constant na univs c =
   let open Constr in
   let vars = CVars.universes_of_constr c in
   let univs = UState.restrict_universe_context univs vars in
-  let univs = Monomorphic_const_entry univs in
+  let univs = Monomorphic_entry univs in
   mkConst(declare_constant (Id.of_string na) 
             (DefinitionEntry (definition_entry ~opaque:true ~univs c),
 	     IsProof Lemma))