fixes #745 (#767)

* fixes #745 * Context rather than Variables
math-comp · Nov 25, 2022 · 6cc1091 · 6cc1091
1 parent 0e7dd9b
commit 6cc1091
Show file tree

Hide file tree

Showing 4 changed files with 164 additions and 168 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -409,6 +409,8 @@
   + `nat_cvgPpinfty` -> `cvgnyPge`
 - in file `topology.v`
   + `prod_topo_apply` -> `proj`
+- in `lebesgue_integral.v`:
+  + `integral_sum` -> `integral_nneseries`
 
 ### Deprecated