fixes #745

math-comp · Nov 13, 2022 · 18a6588 · 18a6588
1 parent 3bee163
commit 18a6588
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
@@ -372,6 +372,8 @@
   + `ereal_lim_sum` -> `cvg_nnesum`
 - moved from `sequences.v` to `topology.v`:
   + `nat_cvgPpinfty` -> `cvgnyPge`
+- in `lebesgue_integral.v`:
+  + `integral_sum` -> `integral_nneseries`
 
 ### Deprecated