aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Sorting/PermutSetoid.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Sorting/PermutSetoid.v')
-rw-r--r--theories/Sorting/PermutSetoid.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index 6f0d76a62..b2b15c705 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -71,7 +71,7 @@ Qed.
Lemma permut_sym :
forall l1 l2 : list A, permutation l1 l2 -> permutation l2 l1.
Proof.
- unfold permutation, meq; intros; apply sym_eq; trivial.
+ unfold permutation, meq; intros; symmetry; trivial.
Qed.
Lemma permut_trans :