From 3da8243049e21e6e6cff4ce95201ecbaea02479d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 8 Jul 2016 15:30:32 -0700 Subject: Fix NatUtil for 8.4 --- 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 02122719e..83375f99a 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -140,7 +140,7 @@ Hint Resolve pow_nonzero : arith. Lemma S_pred_nonzero : forall a, (a > 0 -> S (pred a) = a)%nat. Proof. - destruct a; omega. + destruct a; simpl; omega. Qed. Hint Rewrite S_pred_nonzero using omega : natsimplify. -- cgit v1.2.3