Forgotten probability.v in theories/Make (#1001)

This means probability.v is not compiled in any OPAM package for instance.
math-comp · Aug 5, 2023 · ad68bdd · ad68bdd
1 parent 779afdf
commit ad68bdd
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 0 deletions.
diff --git 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
@@ -28,6 +28,7 @@ derive.v
 measure.v
 numfun.v
 lebesgue_integral.v
+probability.v
 summability.v
 signed.v
 itv.v