fix #2253 (#2357)

agda · Apr 20, 2024 · e0d58fc · e0d58fc
1 parent 90db673
commit e0d58fc
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 0 deletions.
diff --git 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
@@ -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."
+#-}