Skip to content

Commit e54ffec

Browse files
jamesmckinnaandreasabel
authored andcommittedJul 10, 2024
fix #2253 (#2357)
1 parent 9148fa5 commit e54ffec

File tree

2 files changed

+18
-0
lines changed

2 files changed

+18
-0
lines changed
 

‎CHANGELOG.md

+6
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,12 @@ Deprecated names
4949
_-_ ↦ _//_
5050
```
5151

52+
* In `Algebra.Structures.Biased`:
53+
```agda
54+
IsRing* ↦ Algebra.Structures.IsRing
55+
isRing* ↦ Algebra.Structures.isRing
56+
```
57+
5258
* In `Data.Nat.Divisibility.Core`:
5359
```agda
5460
*-pres-∣ ↦ Data.Nat.Divisibility.*-pres-∣

‎src/Algebra/Structures/Biased.agda

+12
Original file line numberDiff line numberDiff line change
@@ -262,5 +262,17 @@ Please use the standard `IsRing` instead."
262262
#-}
263263
{-# WARNING_ON_USAGE isRingWithoutAnnihilatingZero
264264
"Warning: isRingWithoutAnnihilatingZero was deprecated in v2.0.
265+
Please use the standard `isRing` instead."
266+
#-}
267+
268+
-- Version 2.1
269+
270+
-- issue #2253
271+
{-# WARNING_ON_USAGE IsRing*
272+
"Warning: IsRing* was deprecated in v2.1.
265273
Please use the standard `IsRing` instead."
266274
#-}
275+
{-# WARNING_ON_USAGE isRing*
276+
"Warning: isRing* was deprecated in v2.1.
277+
Please use the standard `isRing` instead."
278+
#-}

0 commit comments

Comments
 (0)
Please sign in to comment.