Skip to content

Commit 94590a1

Browse files
theryandres-erbsen
authored andcommitted
correct typos in deprecated warnings
1 parent 12b55f9 commit 94590a1

File tree

1 file changed

+4
-4
lines changed

1 file changed

+4
-4
lines changed

theories/ZArith/Zbool.v

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -152,13 +152,13 @@ Definition Zeven_odd_bool (x:Z) := bool_of_sumbool (Zeven_odd_dec x).
152152
(**********************************************************************)
153153
(** * Boolean comparisons of binary integers *)
154154

155-
#[deprecated(use=Z.eqb, since="9.0")]
155+
#[deprecated(use=Z.leb, since="9.0")]
156156
Notation Zle_bool := Z.leb (only parsing).
157-
#[deprecated(use=Z.eqb, since="9.0")]
157+
#[deprecated(use=Z.geb, since="9.0")]
158158
Notation Zge_bool := Z.geb (only parsing).
159-
#[deprecated(use=Z.eqb, since="9.0")]
159+
#[deprecated(use=Z.ltb, since="9.0")]
160160
Notation Zlt_bool := Z.ltb (only parsing).
161-
#[deprecated(use=Z.eqb, since="9.0")]
161+
#[deprecated(use=Z.gtb, since="9.0")]
162162
Notation Zgt_bool := Z.gtb (only parsing).
163163

164164
(** We now provide a direct [Z.eqb] that doesn't refer to [Z.compare].

0 commit comments

Comments
 (0)