Skip to content

Commit 21595c3

Browse files
committed
removed alias Zmod:=Z.modulo (deprecated since 8.17)
1 parent 499c6e5 commit 21595c3

2 files changed

Lines changed: 6 additions & 2 deletions

File tree

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
- in `Zdiv.v`
2+
3+
+ alias `Zmod` for `Z.modulo`, deprecated since 8.17
4+
(`#149 <https://github.com/coq/stdlib/pull/149>`_,
5+
by Andres Erbsen).
6+

theories/ZArith/Zdiv.v

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,6 @@ Local Open Scope Z_scope.
2222

2323
#[deprecated(since="8.17",note="Use Coq.ZArith.BinIntDef.Z.pos_div_eucl instead")]
2424
Notation Zdiv_eucl_POS := Z.pos_div_eucl (only parsing).
25-
#[deprecated(since="8.17",note="Use Coq.ZArith.BinIntDef.Z.modulo instead")]
26-
Notation Zmod := Z.modulo (only parsing).
2725

2826
#[deprecated(since="8.17",note="Use BinInt.Z.pos_div_eucl_bound instead")]
2927
Notation Zmod_POS_bound := Z.pos_div_eucl_bound (only parsing).

0 commit comments

Comments
 (0)