[stdlib] Fix warnings on deprecated `Add Setoid`

The test suite cases are preserved until the feature is actually removed.

3 files changed, 30 insertions, 6 deletions

diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index 88e2cb1da..462ffde31 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -1612,7 +1612,11 @@ Section Complete.
   Notation "x / y " := (rdiv x y).  Notation "/ x" := (rinv x).
   Notation "x == y" := (req x y) (at level 70, no associativity).
  Variable Rsth : Setoid_Theory R req.
-   Add Setoid R req Rsth as R_setoid3.
+   Add Parametric Relation : R req
+     reflexivity  proved by Rsth.(@Equivalence_Reflexive _ _)
+     symmetry     proved by Rsth.(@Equivalence_Symmetric _ _)
+     transitivity proved by Rsth.(@Equivalence_Transitive _ _)
+    as R_setoid3.
  Variable Reqe : ring_eq_ext radd rmul ropp req.
    Add Morphism radd with signature (req ==> req ==> req) as radd_ext3.
    Proof. exact (Radd_ext Reqe). Qed.
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index bd4e94687..8aa0b1c91 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -48,7 +48,11 @@ Section ZMORPHISM.
   Notation "x - y " := (rsub x y).  Notation "- x" := (ropp x).
   Notation "x == y" := (req x y).
   Variable Rsth : Setoid_Theory R req.
-     Add Setoid R req Rsth as R_setoid3.
+     Add Parametric Relation : R req
+       reflexivity  proved by Rsth.(@Equivalence_Reflexive _ _)
+       symmetry     proved by Rsth.(@Equivalence_Symmetric _ _)
+       transitivity proved by Rsth.(@Equivalence_Transitive _ _)
+      as R_setoid3.
      Ltac rrefl := gen_reflexivity Rsth.
  Variable Reqe : ring_eq_ext radd rmul ropp req.
    Add Morphism radd with signature (req ==> req ==> req) as radd_ext3.
@@ -260,7 +264,11 @@ Section NMORPHISM.
   Notation "0" := rO.  Notation "1" := rI.
   Notation "x + y" := (radd x y).  Notation "x * y " := (rmul x y).
  Variable Rsth : Setoid_Theory R req.
-     Add Setoid R req Rsth as R_setoid4.
+     Add Parametric Relation : R req
+       reflexivity  proved by Rsth.(@Equivalence_Reflexive _ _)
+       symmetry     proved by Rsth.(@Equivalence_Symmetric _ _)
+       transitivity proved by Rsth.(@Equivalence_Transitive _ _)
+       as R_setoid4.
      Ltac rrefl := gen_reflexivity Rsth.
  Variable SReqe : sring_eq_ext radd rmul req.
  Variable SRth : semi_ring_theory 0 1 radd rmul req.
@@ -381,7 +389,11 @@ Section NWORDMORPHISM.
   Notation "x - y " := (rsub x y).  Notation "- x" := (ropp x).
   Notation "x == y" := (req x y).
   Variable Rsth : Setoid_Theory R req.
-     Add Setoid R req Rsth as R_setoid5.
+     Add Parametric Relation : R req
+       reflexivity  proved by Rsth.(@Equivalence_Reflexive _ _)
+       symmetry     proved by Rsth.(@Equivalence_Symmetric _ _)
+       transitivity proved by Rsth.(@Equivalence_Transitive _ _)
+      as R_setoid5.
      Ltac rrefl := gen_reflexivity Rsth.
  Variable Reqe : ring_eq_ext radd rmul ropp req.
    Add Morphism radd with signature (req ==> req ==> req) as radd_ext5.
@@ -566,7 +578,11 @@ Section GEN_DIV.
  Variable morph : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi.
 
   (* Useful tactics *)
-  Add Setoid R req Rsth as R_set1.
+  Add Parametric Relation : R req
+    reflexivity  proved by Rsth.(@Equivalence_Reflexive _ _)
+    symmetry     proved by Rsth.(@Equivalence_Symmetric _ _)
+    transitivity proved by Rsth.(@Equivalence_Transitive _ _)
+   as R_set1.
  Ltac rrefl := gen_reflexivity Rsth.
   Add Morphism radd with signature (req ==> req ==> req) as radd_ext.
   Proof. exact (Radd_ext Reqe). Qed.
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 335a68d70..776ebd808 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -404,7 +404,11 @@ Section ALMOST_RING.
  Variable Csth : Equivalence ceq.
  Variable Ceqe : ring_eq_ext cadd cmul copp ceq.
 
-   Add Setoid C ceq Csth as C_setoid.
+   Add Parametric Relation : C ceq
+     reflexivity  proved by Csth.(@Equivalence_Reflexive _ _)
+     symmetry     proved by Csth.(@Equivalence_Symmetric _ _)
+     transitivity proved by Csth.(@Equivalence_Transitive _ _)
+    as C_setoid.
 
    Add Morphism cadd with signature (ceq ==> ceq ==> ceq) as cadd_ext.
    Proof. exact (Radd_ext Ceqe). Qed.