diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-01 19:43:58 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-01 19:43:58 -0700 |
| commit | a825cfbb7b9a96cec2b7b891c1e76195177a7a0c (patch) | |
| tree | 666fce33a561e49814ddaa5da3b420202d6df37c /src/Util/ZUtil.v | |
| parent | be267954b7267b8564e4125b58349e0860f31967 (diff) | |
Fix for 8.4 evars
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index fe329d3f9..a8b18ffef 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -812,7 +812,7 @@ Proof. assert (Hn : -X <= a - b) by lia. assert (Hp : a - b <= X - 1) by lia. split; etransitivity; [ | apply Z_div_le, Hn; lia | apply Z_div_le, Hp; lia | ]; - autorewrite with zsimplify; reflexivity. + instantiate; autorewrite with zsimplify; try reflexivity. Qed. Hint Resolve (fun a b X H0 H1 => proj1 (Zsub_pos_bound_div a b X H0 H1)) |