- Add more precise error localisation when one of the application fails

  in a chain of apply or apply-in.
- Improved comments on the notions of permutation used in the library (still
  the equality relation in file Permutation.v misses the property of being
  effectively an equivalence relation, hence missing expected properties of
  this notion of permutation).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12261 85f007b7-540e-0410-9357-904b9bb8a0f7

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.