2 files changed, 9 insertions, 8 deletions
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index 814ef0408..1ea71972b 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -13,7 +13,7 @@ Require Import Omega Relations Multiset Permutation SetoidList.
 Set Implicit Arguments.
 
 (** This file contains additional results about permutations 
-     with respect to an setoid equality (i.e. an equivalence relation). 
+     with respect to a setoid equality (i.e. an equivalence relation). 
 *)
 
 Section Perm.
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index e9bbf88e3..a92212054 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -12,22 +12,23 @@ Require Import Relations List Multiset Arith.
 
 (** This file define a notion of permutation for lists, based on multisets: 
     there exists a permutation between two lists iff every elements have 
-    the same multiplicities in the two lists. 
+    the same multiplicity in the two lists. 
+
+    Unlike [List.Permutation], the present notion of permutation
+    requires the domain to be equipped with a decidable equality. This
+    equality allows to reason modulo the effective equivalence-class
+    representative used in each list.
 
-    Unlike [List.Permutation], the present notion of permutation requires
-    a decidable equality. At the same time, this definition can be used 
-    with a non-standard equality, whereas [List.Permutation] cannot.
-      
     The present file contains basic results, obtained without any particular
     assumption on the decidable equality used.
-	
+
     File [PermutSetoid] contains additional results about permutations 
     with respect to an setoid equality (i.e. an equivalence relation). 
 
     Finally, file [PermutEq] concerns Coq equality : this file is similar 
     to the previous one, but proves in addition that [List.Permutation]
     and [permutation] are equivalent in this context.
-x*)
+*)
 
 Set Implicit Arguments.