From 63ff356a8546fbcb883bb6a9711c785f75fecd41 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 12 Oct 2016 16:14:00 +0200 Subject: Little addition to 6eede071 for consistency of style in OrdersFacts.v. --- theories/Structures/OrdersFacts.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 6f8fc1b324..0115d8a544 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -434,14 +434,14 @@ Lemma eqb_compare x y : (x =? y) = match compare x y with Eq => true | _ => false end. Proof. apply eq_true_iff_eq. rewrite eqb_eq, <- compare_eq_iff. -destruct compare; now split. +now destruct compare. Qed. Lemma ltb_compare x y : (x true | _ => false end. Proof. apply eq_true_iff_eq. rewrite ltb_lt, <- compare_lt_iff. -destruct compare; now split. +now destruct compare. Qed. Lemma leb_compare x y : -- cgit v1.2.3