diff --git a/CHANGELOG.md b/CHANGELOG.md index 469c926af8..216c53482d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -49,6 +49,12 @@ Deprecated names _-_ ↦ _//_ ``` +* In `Algebra.Structures.Biased`: + ```agda + IsRing* ↦ Algebra.Structures.IsRing + isRing* ↦ Algebra.Structures.isRing + ``` + * In `Data.Nat.Divisibility.Core`: ```agda *-pres-∣ ↦ Data.Nat.Divisibility.*-pres-∣ diff --git a/src/Algebra/Structures/Biased.agda b/src/Algebra/Structures/Biased.agda index 8218a1ee1b..59e47da553 100644 --- a/src/Algebra/Structures/Biased.agda +++ b/src/Algebra/Structures/Biased.agda @@ -262,5 +262,17 @@ Please use the standard `IsRing` instead." #-} {-# WARNING_ON_USAGE isRingWithoutAnnihilatingZero "Warning: isRingWithoutAnnihilatingZero was deprecated in v2.0. +Please use the standard `isRing` instead." +#-} + +-- Version 2.1 + +-- issue #2253 +{-# WARNING_ON_USAGE IsRing* +"Warning: IsRing* was deprecated in v2.1. Please use the standard `IsRing` instead." #-} +{-# WARNING_ON_USAGE isRing* +"Warning: isRing* was deprecated in v2.1. +Please use the standard `isRing` instead." +#-}