diff options
Diffstat (limited to 'theories/Structures/OrdersAlt.v')
| -rw-r--r-- | theories/Structures/OrdersAlt.v | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/theories/Structures/OrdersAlt.v b/theories/Structures/OrdersAlt.v index 21ef8eb8..5dd917a7 100644 --- a/theories/Structures/OrdersAlt.v +++ b/theories/Structures/OrdersAlt.v @@ -11,8 +11,6 @@ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud * 91405 Orsay, France *) -(* $Id: OrdersAlt.v 12754 2010-02-12 16:21:48Z letouzey $ *) - Require Import OrderedType Orders. Set Implicit Arguments. @@ -142,7 +140,7 @@ Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType. Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z. Proof. unfold lt, eq; intros x y z Hxy Hyz. - destruct (compare x z) as [ ]_eqn:Hxz; auto. + destruct (compare x z) eqn:Hxz; auto. rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz. rewrite (compare_trans Hxz Hyz) in Hxy; discriminate. rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy. @@ -152,7 +150,7 @@ Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType. Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z. Proof. unfold lt, eq; intros x y z Hxy Hyz. - destruct (compare x z) as [ ]_eqn:Hxz; auto. + destruct (compare x z) eqn:Hxz; auto. rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy. rewrite (compare_trans Hxy Hxz) in Hyz; discriminate. rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz. @@ -171,7 +169,7 @@ Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType. Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). Proof. unfold eq, lt, compare; intros. - destruct (O.compare x y) as [ ]_eqn:H; auto. + destruct (O.compare x y) eqn:H; auto. apply CompGt. rewrite compare_sym, H; auto. Qed. |