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.