diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-23 16:09:02 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-23 16:09:02 -0400 |
| commit | ab53befd3fed21e63a9a94d4cac20ff59bb225de (patch) | |
| tree | 96ab422ba5849199e542d4d26969b3658b51964f /src/Util/NatUtil.v | |
| parent | ecf1d8a89e84a1f80f0c0cc6e4ad9c68465965ab (diff) | |
Fix 8.4 build issue
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. |