Skip to content

Commit ff720a5

Browse files
authored
Merge pull request #98 from mrhaandi/N-Z-div-mod
compatibility with PR #14037
2 parents a0d437c + f2d060a commit ff720a5

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

implementations/stdlib_binary_integers.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -226,7 +226,7 @@ Instance Z_mod: ModEuclid Z := Zmod.
226226
Instance: EuclidSpec Z _ _.
227227
Proof.
228228
split; try apply _.
229-
exact Z_div_mod_eq_full.
229+
exact Z.div_mod.
230230
intros x y Ey. destruct (Z_mod_remainder x y); intuition.
231231
now intros [].
232232
now intros [].

0 commit comments

Comments
 (0)