From bc1168a4aa0a336e9686b57cc29ec562aa379973 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 18 Dec 2009 15:27:45 +0000
Subject: RelationPairs: stop loading it in all Numbers, stop maximal args with
 fst/snd

 As a consequence, revert to some pedestrian proofs of Equivalence here
 and there, without the need for the Measure class.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12598 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Structures/OrderedType2Ex.v    | 2 +-
 theories/Structures/OrderedType2Lists.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'theories/Structures')

diff --git a/theories/Structures/OrderedType2Ex.v b/theories/Structures/OrderedType2Ex.v
index 6a02319734..c64fb7a97b 100644
--- a/theories/Structures/OrderedType2Ex.v
+++ b/theories/Structures/OrderedType2Ex.v
@@ -46,7 +46,7 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
  Include PairDecidableType O1 O2.
 
  Definition lt :=
-   (relation_disjunction (O1.lt @@ fst) (O1.eq * O2.lt))%signature.
+   (relation_disjunction (O1.lt @@1) (O1.eq * O2.lt))%signature.
 
  Instance lt_strorder : StrictOrder lt.
  Proof.
diff --git a/theories/Structures/OrderedType2Lists.v b/theories/Structures/OrderedType2Lists.v
index 4aa07dfdcd..567cbd9f85 100644
--- a/theories/Structures/OrderedType2Lists.v
+++ b/theories/Structures/OrderedType2Lists.v
@@ -73,9 +73,9 @@ Module KeyOrderedType(Import O:OrderedType).
 
   Local Open Scope signature_scope.
 
-  Definition eqk : relation (key*elt) := eq @@ fst.
+  Definition eqk : relation (key*elt) := eq @@1.
   Definition eqke : relation (key*elt) := eq * Logic.eq.
-  Definition ltk : relation (key*elt) := lt @@ fst.
+  Definition ltk : relation (key*elt) := lt @@1.
 
   Hint Unfold eqk eqke ltk.
 
-- 
cgit v1.2.3