From b520fc53e0d4aba563ffc1cbdd480713b280fafc Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 2 Nov 2009 18:51:43 +0000
Subject: List + SetoidList : some cleanup around predicates Exists, Forall,
 Forall2, ForallPairs, etc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12459 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Structures/OrderedType2.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'theories/Structures')

diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v
index c72d3a79dc..16da2162d9 100644
--- a/theories/Structures/OrderedType2.v
+++ b/theories/Structures/OrderedType2.v
@@ -408,23 +408,23 @@ Module KeyOrderedType(Import O:OrderedType).
   exists e; auto.
   Qed.
 
-  Lemma In_alt2 : forall k l, In k l <-> ExistsL (fun p => eq k (fst p)) l.
+  Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l.
   Proof.
   unfold In, MapsTo.
-  setoid_rewrite ExistsL_exists; setoid_rewrite InA_alt.
+  setoid_rewrite Exists_exists; setoid_rewrite InA_alt.
   firstorder.
   exists (snd x), x; auto.
   Qed.
 
   Lemma In_nil : forall k, In k nil <-> False.
   Proof.
-  intros; rewrite In_alt2; apply ExistsL_nil.
+  intros; rewrite In_alt2; apply Exists_nil.
   Qed.
 
   Lemma In_cons : forall k p l,
    In k (p::l) <-> eq k (fst p) \/ In k l.
   Proof.
-  intros; rewrite !In_alt2, ExistsL_cons; intuition.
+  intros; rewrite !In_alt2, Exists_cons; intuition.
   Qed.
 
   Global Instance MapsTo_compat :
-- 
cgit v1.2.3