Merge pull request #98 from mrhaandi/N-Z-div-mod

compatibility with PR #14037
coq-community · May 21, 2021 · ff720a5 · ff720a5
2 parents a0d437c + f2d060a
commit ff720a5
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/implementations/stdlib_binary_integers.v b/implementations/stdlib_binary_integers.v
@@ -226,7 +226,7 @@ Instance Z_mod: ModEuclid Z := Zmod.
 Instance: EuclidSpec Z _ _.
 Proof.
   split; try apply _.
-     exact Z_div_mod_eq_full.
+     exact Z.div_mod.
     intros x y Ey. destruct (Z_mod_remainder x y); intuition.
    now intros [].
   now intros [].