From ab53befd3fed21e63a9a94d4cac20ff59bb225de Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 23 Oct 2016 16:09:02 -0400 Subject: Fix 8.4 build issue --- src/Util/NatUtil.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Util/NatUtil.v') 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. -- cgit v1.2.3