diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 83f356738..08c7e13dd 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -12,6 +12,7 @@ - in `mathcomp_extra.v`: + lemma `partition_disjoint_bigfcup` + - in `constructive_ereal.v`: + notations `\prod` in scope ereal_scope + lemmas `prode_ge0`, `prode_fin_num`