diff options
Diffstat (limited to 'theories/Structures/OrderedType.v')
-rw-r--r-- | theories/Structures/OrderedType.v | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index 57f491d2..f84cdf32 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: OrderedType.v 12732 2010-02-10 22:46:59Z letouzey $ *) - Require Export SetoidList Morphisms OrdersTac. Set Implicit Arguments. Unset Strict Implicit. @@ -22,6 +20,10 @@ Inductive Compare (X : Type) (lt eq : X -> X -> Prop) (x y : X) : Type := | EQ : eq x y -> Compare lt eq x y | GT : lt y x -> Compare lt eq x y. +Arguments LT [X lt eq x y] _. +Arguments EQ [X lt eq x y] _. +Arguments GT [X lt eq x y] _. + Module Type MiniOrderedType. Parameter Inline t : Type. @@ -143,7 +145,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma elim_compare_eq : forall x y : t, - eq x y -> exists H : eq x y, compare x y = EQ _ H. + eq x y -> exists H : eq x y, compare x y = EQ H. Proof. intros; case (compare x y); intros H'; try (exfalso; order). exists H'; auto. @@ -151,7 +153,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma elim_compare_lt : forall x y : t, - lt x y -> exists H : lt x y, compare x y = LT _ H. + lt x y -> exists H : lt x y, compare x y = LT H. Proof. intros; case (compare x y); intros H'; try (exfalso; order). exists H'; auto. @@ -159,7 +161,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma elim_compare_gt : forall x y : t, - lt y x -> exists H : lt y x, compare x y = GT _ H. + lt y x -> exists H : lt y x, compare x y = GT H. Proof. intros; case (compare x y); intros H'; try (exfalso; order). exists H'; auto. @@ -318,16 +320,13 @@ Module KeyOrderedType(O:OrderedType). Hint Immediate eqk_sym eqke_sym. Global Instance eqk_equiv : Equivalence eqk. - Proof. split; eauto. Qed. + Proof. constructor; eauto. Qed. Global Instance eqke_equiv : Equivalence eqke. Proof. split; eauto. Qed. Global Instance ltk_strorder : StrictOrder ltk. - Proof. - split; eauto. - intros (x,e); compute; apply (StrictOrder_Irreflexive x). - Qed. + Proof. constructor; eauto. intros x; apply (irreflexivity (x:=fst x)). Qed. Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk. Proof. |