diff options
-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 |