Skip to content

Commit 5c0d0b5

Browse files
Fix deprecation warning
1 parent 2029472 commit 5c0d0b5

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

theories/FillInTheBlanks.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -349,7 +349,7 @@ Proof.
349349
lia. }
350350
assert (H1 : (2 * length withBlanks) / 2 = length withBlanks).
351351
{ rewrite Nat.mul_comm. apply Nat.div_mul. easy. }
352-
rewrite H. rewrite <- (Nat.divide_div_mul_exact _ _ _).
352+
rewrite H. rewrite <- (Lcm0.divide_div_mul_exact _ _ _).
353353
* rewrite H1. rewrite subtractToCountNone. reflexivity.
354354
* easy.
355355
* unfold possibleToFillBool in h.

0 commit comments

Comments
 (0)