diff options
| author | letouzey | 2007-06-27 01:50:17 +0000 |
|---|---|---|
| committer | letouzey | 2007-06-27 01:50:17 +0000 |
| commit | f6c4669e86a9ad73dd97591829a929be19f89cb9 (patch) | |
| tree | 355819bbbca0b06cd11cf7c2c9d61896dbcc3d28 | |
| parent | e1438154fb28c8071ff4d26459996b9dc0a8bed0 (diff) | |
eqlistA is now equivlistA
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9913 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/Sorting/PermutSetoid.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |