From 3b06585b1ab4c0e77afcdccf584335b7b8050697 Mon Sep 17 00:00:00 2001
From: Olivier Laurent
Date: Sun, 3 May 2020 11:34:00 +0200
Subject: consistency with Permutation

---
 theories/Sorting/CPermutation.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Sorting/CPermutation.v b/theories/Sorting/CPermutation.v
index fac9cd1d6d..21d04da877 100644
--- a/theories/Sorting/CPermutation.v
+++ b/theories/Sorting/CPermutation.v
@@ -154,7 +154,7 @@ Qed.
 Lemma CPermutation_length_1 : forall a b, CPermutation [a] [b] -> a = b.
 Proof. intros; now apply Permutation_length_1, CPermutation_Permutation. Qed.
 
-Lemma CPermutation_length_1_inv : forall l a, CPermutation [a] l -> l = [a].
+Lemma CPermutation_length_1_inv : forall a l, CPermutation [a] l -> l = [a].
 Proof. intros; now apply Permutation_length_1_inv, CPermutation_Permutation. Qed.
 
 Lemma CPermutation_swap : forall a b, CPermutation [a; b] [b; a].
-- 
cgit v1.2.3