diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index b43828ab4..74e2bafdb 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -3,6 +3,10 @@
 ## [Unreleased]
 
 ### Added
+
+- in `theories/Make`
+  + file `probability.v` (wasn't compiled in OPAM packages up to now)
+
 - in `measure.v`:
   + lemma `lebesgue_regularity_outer`
 
diff --git a/theories/Make b/theories/Make
index fffdba636..eb5a1f241 100644
--- a/theories/Make
+++ b/theories/Make
@@ -28,6 +28,7 @@ derive.v
 measure.v
 numfun.v
 lebesgue_integral.v
+probability.v
 summability.v
 signed.v
 itv.v