Revert "[ refactor ] fix #2865 for v2.4 (#2954)" (#2973)

This reverts commit 7847620.

Author: MatthewDaggitt

CHANGELOG.md

@@ -104,11 +104,6 @@ Deprecated names
   witness   ↦   satisfiable
   ```
 
-* In `Data.List.Relation.Unary.Any`:
-  ```agda
-  satisfiable    ↦  satisfiable⁺
-  ```
-
 * In `Data.Rational.Properties`:
   ```agda
   nonPos*nonPos⇒nonPos  ↦  nonPos*nonPos⇒nonNeg
@@ -333,7 +328,7 @@ Additions to existing modules
 
 * In `Data.List.NonEmpty.Relation.Unary.All`:
   ```
-  map : P ⊆ Q → All P ⊆ All Q
+  map : P ⊆ Q → All P xs → All Q xs
   ```
 
 * In `Data.List.Properties`:
@@ -343,11 +338,6 @@ Additions to existing modules
   filter-swap : filter P? ∘ filter Q? ≗ filter Q? ∘ filter P?
   ```
 
-* In `Data.List.Relation.Unary.Any`:
-  ```agda
-  satisfiable⁻ : Satisfiable (Any P) → Satisfiable P
-  ```
-
 * In `Data.Nat.Divisibility`:
   ```agda
   m∣n⇒m^o∣n^o : ∀ o → m ∣ n → m ^ o ∣ n ^ o

src/Data/List/NonEmpty/Relation/Unary/Any.agda

@@ -42,6 +42,6 @@ map g (there pxs) = there (List.map g pxs)
 ------------------------------------------------------------------------
 -- Predicates
 
-satisfiable : Any P xs → Satisfiable P
-satisfiable (here px)  = _ , px
-satisfiable (there pxs) = List.satisfied pxs
+satisfied : Any P xs → Satisfiable P
+satisfied (here px)  = _ , px
+satisfied (there pxs) = List.satisfied pxs

src/Data/List/Relation/Unary/Any.agda

@@ -69,11 +69,7 @@ infixl 4 _─_
 _─_ : {P : Pred A p} → ∀ xs → Any P xs → List A
 xs ─ x∈xs = removeAt xs (index x∈xs)
 
--- If any element satisfies P, then P is satisfiable.
-
--- v2.4 `satisfied` is being retained for compatibility reasons,
---      while `satisfiable` below is renamed to `satisfiable⁺`
--- v3.0 `satisfied` will be renamed to `satisfiable`
+-- If any element satisfies P, then P is satisfied.
 
 satisfied : Any P xs → Satisfiable P
 satisfied (here px)   = _ , px
@@ -94,16 +90,12 @@ any? : Decidable P → Decidable (Any P)
 any? P? []       = no λ()
 any? P? (x ∷ xs) = Dec.map′ fromSum toSum (P? x ⊎? any? P? xs)
 
-satisfiable⁺ : Satisfiable P → Satisfiable (Any P)
-satisfiable⁺ (x , Px) = [ x ] , here Px
-
-satisfiable⁻ : Satisfiable (Any P) → Satisfiable P
-satisfiable⁻ (x ∷ _  , here px)   = x , px
-satisfiable⁻ (_ ∷ xs , there pxs) = satisfiable⁻ (xs , pxs)
+satisfiable : Satisfiable P → Satisfiable (Any P)
+satisfiable (x , Px) = [ x ] , here Px
 
 
 ------------------------------------------------------------------------
--- DEPRECATED NAMES
+-- DEPRECATED
 ------------------------------------------------------------------------
 -- Please use the new names as continuing support for the old names is
 -- not guaranteed.
@@ -115,14 +107,3 @@ any = any?
 "Warning: any was deprecated in v1.4.
 Please use any? instead."
 #-}
-
--- Version 2.4
-
-satisfiable = satisfiable⁺
-{-# WARNING_ON_USAGE satisfiable
-"Warning: satisfiable was deprecated in v2.4.
-Please use satisfiable⁺ instead. Moreover,
-the name satisfied will be renamed in v3.0
-to satisfiable, so users should refactor
-as soon as they can."
-#-}