diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-10 13:22:56 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-10 13:22:56 -0500 |
| commit | d82fad78d2c09f75a5fadaded2dd3bd056288739 (patch) | |
| tree | 4e208bdecde5dfdca23e4a0a0fc3cd5e8f0c44bc /src/Util/WordUtil.v | |
| parent | 64d2f58133b105f46ce9c832e5cbdc13342c1c50 (diff) | |
Fix for 8.4
Diffstat (limited to 'src/Util/WordUtil.v')
| -rw-r--r-- | src/Util/WordUtil.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index 36867958f..97d40db6b 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -910,12 +910,12 @@ Section Updates. Local Ltac mul_mono := etransitivity; [|apply Z.mul_le_mono_nonneg_r]; - repeat first + repeat (instantiate; first [ eassumption | reflexivity | apply Z.mul_le_mono_nonneg_l | rewrite Z.mul_0_l - | omega]. + | omega]). Lemma mul_valid_update: forall n, valid_update n |