diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md
index 9cd12a2841..06148c14de 100644
--- a/CHANGELOG_NEXT.md
+++ b/CHANGELOG_NEXT.md
@@ -186,6 +186,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 * Some pieces of `Data.Fin.Extra` from `contrib` were moved to `base` to modules
   `Data.Fin.Properties`, `Data.Fin.Arith` and `Data.Fin.Split`.
 
+* `Decidable.Decidable.decison` is now `public export`.
+
 #### Contrib
 
 * `Data.List.Lazy` was moved from `contrib` to `base`.
diff --git a/libs/base/Decidable/Decidable.idr b/libs/base/Decidable/Decidable.idr
index 314d14bd23..f476f77f5f 100644
--- a/libs/base/Decidable/Decidable.idr
+++ b/libs/base/Decidable/Decidable.idr
@@ -51,5 +51,6 @@ interface Decidable k ts p where
 
 ||| Given a `Decidable` n-ary relation, provides a decision procedure for
 ||| this relation.
+public export
 decision : (ts : Vect k Type) -> (p : Rel ts) -> Decidable k ts p => liftRel ts p Dec
 decision ts p = decide {ts} {p}