fixes #745

math-comp · Oct 20, 2022 · bffe427 · bffe427
1 parent cd23cba
commit bffe427
Show file tree

Hide file tree

Showing 2 changed files with 81 additions and 74 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -175,6 +175,8 @@
   + `nneseries_pred0` -> `eseries_pred0`
   + `eq_nneseries` -> `eq_eseries`
   + `nneseries_mkcond` -> `eseries_mkcond`
+- in `lebesgue_integral.v`:
+  + `integral_sum` -> `integral_nneseries`
 
 ### Deprecated