From d82fad78d2c09f75a5fadaded2dd3bd056288739 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 10 Nov 2016 13:22:56 -0500 Subject: Fix for 8.4 --- src/Util/WordUtil.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Util/WordUtil.v') 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 -- cgit v1.2.3