aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures/OrdersFacts.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Structures/OrdersFacts.v')
-rw-r--r--theories/Structures/OrdersFacts.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index 6f8fc1b32..0115d8a54 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 <? y) = match compare x y with Lt => 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 :