diff options
Diffstat (limited to 'src/Util/NatUtil.v')
-rw-r--r-- | src/Util/NatUtil.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 51a0bb407..027fd28b1 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -316,7 +316,7 @@ Lemma setbit_high : forall x i, (x < 2^i -> setbit x i = x + 2^i)%nat. Proof. intros x i H; apply bits_inj; intro n. rewrite setbit_eqb. - destruct (i =? n) eqn:H'; simpl. + destruct (beq_nat i n) eqn:H'; simpl. { apply beq_nat_true in H'; subst. symmetry; apply testbit_true. rewrite div_minus, div_small by omega. |