diff options
| author | Emilio Jesus Gallego Arias | 2017-10-15 19:11:48 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-10-15 19:11:48 +0200 |
| commit | cc03c37b48af466e6673fa4cb034e6ef19f709c0 (patch) | |
| tree | ca2d65fd304bddfcd896db64a8856e32fff9207a /plugins/setoid_ring/InitialRing.v | |
| parent | f8975f9fce08c7d43e6e57be980cfa36635969a9 (diff) | |
[stdlib] Fix warnings on deprecated `Add Setoid`
The test suite cases are preserved until the feature is actually removed.
Diffstat (limited to 'plugins/setoid_ring/InitialRing.v')
| -rw-r--r-- | plugins/setoid_ring/InitialRing.v | 24 |
1 files changed, 20 insertions, 4 deletions
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index bd4e94687d..8aa0b1c91f 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. |