From f74327c2ea2a8905fcc74e14cdcf97616a1bbfce Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 9 Apr 2017 13:11:33 -0400 Subject: Fix missing unfold --- 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 ef4be9e64..e8d963b1b 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -269,7 +269,7 @@ Module Z. Lemma sub_le_ge_Proper : Proper (Z.le ==> Z.ge ==> Z.le) Z.sub. Proof. repeat (omega || intro). Qed. Lemma sub_le_flip_le_Proper : Proper (Z.le ==> Basics.flip Z.le ==> Z.le) Z.sub. - Proof. repeat (omega || intro). Qed. + Proof. unfold Basics.flip; repeat (omega || intro). Qed. Lemma sub_le_eq_Proper : Proper (Z.le ==> Logic.eq ==> Z.le) Z.sub. Proof. repeat (omega || intro). Qed. Lemma log2_up_le_Proper : Proper (Z.le ==> Z.le) Z.log2_up. -- cgit v1.2.3