fixes math-comp#745 (math-comp#767)

* fixes math-comp#745 * Context rather than Variables
IshiguroYoshihiro · Dec 21, 2022 · 6a024c9 · 6a024c9
1 parent 65dec2b
commit 6a024c9
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