From f6c4669e86a9ad73dd97591829a929be19f89cb9 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 27 Jun 2007 01:50:17 +0000
Subject: eqlistA is now equivlistA

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9913 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Sorting/PermutSetoid.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index e973db4ad3..f262f5e400 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -185,7 +185,7 @@ Proof.
   destruct H2; apply eqA_trans with a; auto.
 Qed.
 
-Lemma NoDupA_eqlistA_permut : 
+Lemma NoDupA_equivlistA_permut : 
   forall l l', NoDupA eqA l -> NoDupA eqA l' -> 
     equivlistA eqA l l' -> permutation l l'.
 Proof.
-- 
cgit v1.2.3