fixes #745

math-comp · Oct 16, 2022 · ae16861 · ae16861
1 parent f4d41cb
commit ae16861
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
@@ -149,6 +149,8 @@
 - file `theories/functions.v` -> `classical/functions.v`
 - file `theories/cardinality.v` -> `classical/cardinality.v`
 - file `theories/fsbigop.v` -> `classical/fsbigop.v`
+- in `lebesgue_integral.v`:
+  + `integral_sum` -> `integral_nneseries`
 
 ### Deprecated