From a825cfbb7b9a96cec2b7b891c1e76195177a7a0c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Jul 2016 19:43:58 -0700 Subject: Fix for 8.4 evars --- src/Util/ZUtil.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Util/ZUtil.v') 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)) -- cgit v1.2.3