diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-04 12:37:05 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-04 12:37:05 +0000 |
| commit | 0fec4583628dfba57c4bbcf10e8c1fc053c5ec93 (patch) | |
| tree | 18018c90d6c3587d1b5d65d4e57ae32f0ef500de /theories/Sorting/PermutSetoid.v | |
| parent | a42d753ac38896e58158311b3c384e80c9fd3fd4 (diff) | |
- 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
Diffstat (limited to 'theories/Sorting/PermutSetoid.v')
| -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 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. |