diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-08 15:30:32 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-08 15:30:32 -0700 |
| commit | 3da8243049e21e6e6cff4ce95201ecbaea02479d (patch) | |
| tree | e3cb6ecac655da7cefcfe51036cde353f95aa70d /src/Util/NatUtil.v | |
| parent | 0c687b54156b415684a78ae6d702f5efc41aca87 (diff) | |
Fix NatUtil for 8.4
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 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. |