chnage to public re-export of Relation.Nullary.Decidable.Core.decToMaybe

Author: jamesmckinna

CHANGELOG.md

@@ -744,7 +744,7 @@ Additions to existing modules
   recompute          : Reflects A b → Recomputable A
   recompute-constant : (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q
  ```
- 
+
 * Added new definitions in `Relation.Unary`
   ```
   Stable          : Pred A ℓ → Set _

src/Data/Maybe/Base.agda

@@ -16,7 +16,7 @@ open import Data.Unit.Base using (⊤)
 open import Data.These.Base using (These; this; that; these)
 open import Data.Product.Base as Prod using (_×_; _,_)
 open import Function.Base using (_∘_; id; const)
-import Relation.Nullary.Decidable.Core
+import Relation.Nullary.Decidable.Core as Dec
 
 private
   variable
@@ -134,12 +134,15 @@ thatM : Maybe A → B → These A B
 thatM = maybe′ these that
 
 ------------------------------------------------------------------------
--- Deprecated
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
 
 -- Version 2.1
--- decToMaybe
+-- decToMaybe #2330/2336
 
-decToMaybe = Relation.Nullary.Decidable.Core.decToMaybe
+open Dec public using (decToMaybe)
 {-# WARNING_ON_USAGE decToMaybe
 "Warning: decToMaybe was deprecated in v2.1.
 Please use Relation.Nullary.Decidable.Core.decToMaybe instead."

src/Relation/Nullary/Decidable/Core.agda

@@ -11,7 +11,7 @@
 
 module Relation.Nullary.Decidable.Core where
 
--- decToMaybe was intended to be deprecated in v2.1 #2330/#2336
+-- decToMaybe was deprecated in v2.1 #2330/#2336
 -- this can go through `Data.Maybe.Base` once that deprecation is fully done.
 open import Agda.Builtin.Maybe using (Maybe; just; nothing)