3 files changed, 12 insertions, 12 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 7e9711bba5..6582b2a872 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -785,11 +785,10 @@ Section ListOps.
   End Reverse_Induction.
 
 
+  (*********************************************************************)
+  (** ** List permutations as a composition of adjacent transpositions *)
+  (*********************************************************************)
 
-  (***********************************)
-  (** ** Lists modulo permutation    *)
-  (***********************************)
-  
   Section Permutation.
 
     Inductive Permutation : list A -> list A -> Prop :=
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index 814ef0408d..1ea71972b5 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 e9bbf88e3f..a922120545 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.