fix: #2752

Author: jamesmckinna

src/Data/Fin/Permutation.agda

@@ -12,7 +12,8 @@ open import Data.Bool.Base using (true; false)
 open import Data.Fin.Base using (Fin; suc; cast; opposite; punchIn; punchOut)
 open import Data.Fin.Patterns using (0F; 1F)
 open import Data.Fin.Properties using (punchInᵢ≢i; punchOut-punchIn;
-  punchOut-cong; punchOut-cong′; punchIn-punchOut; _≟_; ¬Fin0; cast-involutive)
+  punchOut-cong; punchOut-cong′; punchIn-punchOut
+  ; _≟_; ¬Fin0; cast-involutive; opposite-involutive)
 import Data.Fin.Permutation.Components as PC
 open import Data.Nat.Base using (ℕ; suc; zero)
 open import Data.Product.Base using (_,_; proj₂)
@@ -130,8 +131,8 @@ reverse : Permutation n n
 reverse = permutation
   opposite
   opposite
-  PC.reverse-involutive
-  PC.reverse-involutive
+  opposite-involutive
+  opposite-involutive
 
 ------------------------------------------------------------------------
 -- Element removal

src/Data/Fin/Permutation/Components.agda

@@ -69,20 +69,20 @@ Please use opposite from Data.Fin.Base instead."
 #-}
 
 reverse-prop = opposite-prop
-{-# WARNING_ON_USAGE reverse
+{-# WARNING_ON_USAGE reverse-prop
 "Warning: reverse-prop was deprecated in v2.0.
 Please use opposite-prop from Data.Fin.Properties instead."
 #-}
 
 reverse-involutive = opposite-involutive
-{-# WARNING_ON_USAGE reverse
+{-# WARNING_ON_USAGE reverse-involutive
 "Warning: reverse-involutive was deprecated in v2.0.
 Please use opposite-involutive from Data.Fin.Properties instead."
 #-}
 
 reverse-suc : ∀ {n} {i : Fin n} → toℕ (opposite (suc i)) ≡ toℕ (opposite i)
 reverse-suc {i = i} = opposite-suc i
-{-# WARNING_ON_USAGE reverse
+{-# WARNING_ON_USAGE reverse-suc
 "Warning: reverse-suc was deprecated in v2.0.
 Please use opposite-suc from Data.Fin.Properties instead."
 #-}