changelog for version 0.3.13

CHANGELOG.md

@@ -1,6 +1,54 @@
 # Changelog
 
-Last releases: [[0.3.11] - 2021-11-14](#0311---2021-11-14) and [[0.3.12] - 2021-12-29](#0312---2021-12-29)
+Last releases: [[0.3.12] - 2021-12-29](#0312---2021-12-29) and [[0.3.13] - 2022-01-24](#0313---2022-01-24)
+
+## [0.3.13] - 2022-01-24
+
+### Added
+
+- in `topology.v`:
+  + definitions `kolmogorov_space`, `accessible_space`
+  + lemmas `accessible_closed_set1`, `accessible_kolmogorov`
+  + lemma `filter_pair_set`
+  + definition `prod_topo_apply`
+  + lemmas `prod_topo_applyE`, `prod_topo_apply_continuous`, `hausdorff_product`
+- in `ereal.v`:
+  + lemmas `lee_pemull`, `lee_nemul`, `lee_pemulr`, `lee_nemulr`
+  + lemma `fin_numM`
+  + definition `mule_def`, notation `x *? y`
+  + lemma `mule_defC`
+  + notations `\*` in `ereal_scope`, and `ereal_dual_scope`
+  + lemmas `mule_def_fin`, `mule_def_neq0_infty`, `mule_def_infty_neq0`, `neq0_mule_def`
+  + notation `\-` in `ereal_scope` and `ereal_dual_scope`
+  + lemma `fin_numB`
+  + lemmas `mule_eq_pinfty`, `mule_eq_ninfty`
+  + lemmas `fine_eq0`, `abse_eq0`
+- in `sequences.v`:
+  + lemmas `ereal_cvgM_gt0_pinfty`, `ereal_cvgM_lt0_pinfty`, `ereal_cvgM_gt0_ninfty`,
+    `ereal_cvgM_lt0_ninfty`, `ereal_cvgM`
+
+### Changed
+
+- in `topology.v`:
+  + renamed and generalized `setC_subset_set1C` implication to
+    equivalence `subsetC1`
+- in `ereal.v`:
+  + lemmas `ereal_sup_gt`, `ereal_inf_lt` now use `exists2`
+- notation `\*` moved from `realseq.v` to `topology.v`
+
+### Renamed
+
+- in `topology.v:
+  + `hausdorff` -> `hausdorff_space`
+
+### Removed
+
+- in `realseq.v`:
+  + notation `\-`
+
+### Infrastructure
+
+- add `.dir-locals.el` for company-coq symbols
 
 ## [0.3.12] - 2021-12-29
 

CHANGELOG_UNRELEASED.md

@@ -4,52 +4,12 @@
 
 ### Added
 
-- in `topology.v`:
-  + definitions `kolmogorov_space`, `accessible_space`
-  + lemmas `accessible_closed_set1`, `accessible_kolmogorov`
-- in `ereal.v`:
-  + lemmas `lee_pemull`, `lee_nemul`, `lee_pemulr`, `lee_nemulr`
-- in `sequences.v`:
-  + lemmas `ereal_cvgM_gt0_pinfty`, `ereal_cvgM_lt0_pinfty`, `ereal_cvgM_gt0_ninfty`,
-    `ereal_cvgM_lt0_ninfty`, `ereal_cvgM`
-- in `ereal.v`:
-  + lemma `fin_numM`
-  + definition `mule_def`, notation `x *? y`
-  + lemma `mule_defC`
-  + notations `\*` in `ereal_scope`, and `ereal_dual_scope`
-- in `ereal.v`:
-  + lemmas `mule_def_fin`, `mule_def_neq0_infty`, `mule_def_infty_neq0`, `neq0_mule_def`
-  + notation `\-` in `ereal_scope` and `ereal_dual_scope`
-  + lemma `fin_numB`
-  + lemmas `mule_eq_pinfty`, `mule_eq_ninfty`
-  + lemmas `fine_eq0`, `abse_eq0`
-- in `topology.v`:
-  + lemma `filter_pair_set`
-- in `topology.v`:
-  + definition `prod_topo_apply`
-  + lemmas `prod_topo_applyE`, `prod_topo_apply_continuous`, `hausdorff_product`
-
 ### Changed
 
-- in `topology.v`:
-  + renamed and generalized `setC_subset_set1C` implication to
-    equivalence `subsetC1`
-- in `ereal.v`:
-  + lemmas `ereal_sup_gt`, `ereal_inf_lt` now use `exists2`
-- notation `\*` moved from `realseq.v` to `topology.v`
-
 ### Renamed
 
-- in `topology.v:
-  + `hausdorff` -> `hausdorff_space`
-
 ### Removed
 
-- in `realseq.v`:
-  + notation `\-`
-
 ### Infrastructure
 
-- add `.dir-locals.el` for company-coq symbols
-
 ### Misc

INSTALL.md

@@ -5,7 +5,7 @@
 - [The Coq Proof Assistant version ≥ 8.12](https://coq.inria.fr)
 - [Mathematical Components version ≥ 1.12.0](https://github.com/math-comp/math-comp)
 - [Finmap library version ≥ 1.5.1](https://github.com/math-comp/finmap)
-- [Hierarchy builder version >= 0.10.0](https://github.com/math-comp/hierarchy-builder)
+- [Hierarchy builder version >= 1.0.0](https://github.com/math-comp/hierarchy-builder)
 
 These requirements can be installed in a custom way, or through
 [opam](https://opam.ocaml.org/) (the recommended way) using
@@ -47,7 +47,7 @@ $ opam install coq-mathcomp-analysis
 ```
 To install a precise version, type, say
 ```
-$ opam install coq-mathcomp-analysis.0.3.12
+$ opam install coq-mathcomp-analysis.0.3.13
 ```
 4. Everytime you want to work in this same context, you need to type
 ```

README.md

@@ -46,7 +46,7 @@ the Coq proof-assistant and using the Mathematical Components library.
   - [MathComp field 1.12 or later](https://math-comp.github.io)
   - [MathComp finmap 1.5.1](https://github.com/math-comp/finmap)
   - [MathComp bigenough 1.0.0](https://github.com/math-comp/bigenough)
-  - [Hierarchy Builder >= 0.10.0](https://github.com/math-comp/hierarchy-builder)
+  - [Hierarchy Builder >= 1.0.0](https://github.com/math-comp/hierarchy-builder)
 - Coq namespace: `mathcomp.analysis`
 - Related publication(s):
   - [Formalization Techniques for Asymptotic Reasoning in Classical Analysis](https://jfr.unibo.it/article/view/8124) doi:[10.6092/issn.1972-5787/8124](https://doi.org/10.6092/issn.1972-5787/8124)

coq-mathcomp-analysis.opam

@@ -26,7 +26,7 @@ depends: [
   "coq-mathcomp-field" { (>= "1.12.0" & < "1.15~") | (= "dev") }
   "coq-mathcomp-finmap" { (>= "1.5.1" & < "1.6~") | (= "dev") }
   "coq-mathcomp-bigenough" { (>= "1.0.0") }
-  "coq-hierarchy-builder" { (>= "0.10.0") }
+  "coq-hierarchy-builder" { (>= "1.0.0") }
 ]
 
 tags: [

meta.yml

@@ -63,7 +63,7 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-dev'
+- version: '1.14.0-coq-dev'
   repo: 'mathcomp/mathcomp'
 - version: 'coq-8.13'
   repo: 'mathcomp/mathcomp-dev'
@@ -75,27 +75,27 @@ tested_coq_opam_versions:
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "1.12.0" & < "1.14~") | (= "dev") }'
+    version: '{ (>= "1.12.0" & < "1.15~") | (= "dev") }'
   description: |-
     [MathComp ssreflect 1.12 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-fingroup
-    version: '{ (>= "1.12.0" & < "1.14~") | (= "dev") }'
+    version: '{ (>= "1.12.0" & < "1.15~") | (= "dev") }'
   description: |-
     [MathComp fingroup 1.12 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{ (>= "1.12.0" & < "1.14~") | (= "dev") }'
+    version: '{ (>= "1.12.0" & < "1.15~") | (= "dev") }'
   description: |-
     [MathComp algebra 1.12 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-solvable
-    version: '{ (>= "1.12.0" & < "1.14~") | (= "dev") }'
+    version: '{ (>= "1.12.0" & < "1.15~") | (= "dev") }'
   description: |-
     [MathComp solvable 1.12 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-field
-    version: '{ (>= "1.12.0" & < "1.14~") | (= "dev") }'
+    version: '{ (>= "1.12.0" & < "1.15~") | (= "dev") }'
   description: |-
     [MathComp field 1.12 or later](https://math-comp.github.io)
 - opam:
@@ -110,9 +110,9 @@ dependencies:
     [MathComp bigenough 1.0.0](https://github.com/math-comp/bigenough)
 - opam:
     name: coq-hierarchy-builder
-    version: '{ (>= "0.10.0") }'
+    version: '{ (>= "1.0.0") }'
   description: |-
-    [Hierarchy Builder >= 0.10.0](https://github.com/math-comp/hierarchy-builder)
+    [Hierarchy Builder >= 1.0.0](https://github.com/math-comp/hierarchy-builder)
 namespace: mathcomp.analysis
 
 keywords: