From beaa7708db2398121c6ee68499337f2a91d4adb2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 2 Sep 2026 14:05:22 +0900 Subject: [PATCH 1/2] changelog for version 1.18.0 --- CHANGELOG.md | 216 +++++++++++++++++++++++++++++++++++++++- CHANGELOG_UNRELEASED.md | 205 -------------------------------------- INSTALL.md | 22 ++-- README.md | 14 +-- 4 files changed, 233 insertions(+), 224 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a640e09e4d..2fa6e18ad2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,220 @@ # Changelog -Latest releases: [[1.17.0] - 2026-07-31](#1170---2026-07-31), [[1.16.0] - 2026-03-17](#1160---2026-03-17), and [[1.15.0] - 2026-01-15](#1150---2026-01-15) +Latest releases: [[1.18.0] - 2026-09-02](#1180---2026-09-02), [[1.17.0] - 2026-07-31](#1170---2026-07-31), and [[1.16.0] - 2026-03-17](#1160---2026-03-17) + +## [1.18.0] - 2026-09-02 + +### Added + +- in `Rstruct_topology.v`: + + lemmas `RcosE`, `Rtrigo_PIE`, `RsinE` + +- in `topology_structure.v`: + + lemma `id_continuous` + +- in `nat_topology.v`: + + lemma `near_infty_leq` + +- in `num_topology.v`: + + lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, + `at_left_shift`, `at_right_shift` + +- in `function_spaces.v`: + + lemma `within_continuous_big` + +- in `pseudometric_normed_Zmodule.v`: + + lemmas `cvg0D`, `cvgD0`, `cvg0B`, `cvgB0`, `cvgN0` + +- in `normed_module.v`: + + lemmas `cvg1M`, `cvgM1`, `cvg0M`, `cvgM0` + + lemmas `cvg1Z`, `cvg0Z`, `cvgZ0` + +- in `matrix_normedtype.v`: + + lemma `norm_trmx` + +- in `derive.v`: + + lemmas `derive1Dn`, `der1_scaleLR`, `deriveZLR`, `derivableZLR`, + `derivable_comp_shift`, `derive_comp_shift`, `is_derive_comp_shift`, `derive1_comp_shift`, + `near_eq_derive1n_near`, `near_eq_derive1_near`, `near_eq_derive1n`, + `near_eq_derive1` + + global instance `is_derive_exp` + + lemma `derive1_shift` + + lemmas `derivable_trmx`, `derive_trmx` + + global instance `is_derive_trmx` + +- in `esum.v`: + + lemmas `pos_esum_ge1`, `le_pos_esum_fine`, `sum_esum_ge`, `le_esum_fine`, + `subset_esum`, `esum0`, `esum_if_eq_op_set1`, `esum_neq0`, `esum_ge1` + + lemmas `eq_esummable`, `le_esummable`, `esummableZl`, `esummableZr`, + `esummableMl`, `esummableMr`, `esummableM` + + lemmas `esummable_esum_funepos`, `esummable_esum_funeneg`, + `esummable_esum_fin_num`, `esummable_esumN` + + lemma `esumE` + + lemmas `esummable_esumZ`, `esummable_esumD`, `esummableB` + +- in `measurable_realfun.v`: + + lemma `measurable_bigmaxr` + +- in `normal_distribution.v`: + + definition `post_stddev` + + lemmas `post_stddev_gt0`, `post_stddevE` + + definition `post_mean` + + lemmas `normal_fun_conjugate`, `normal_pdf_conjugate`, `normal_prob_conjugate` + +- new files (result of the splitting of `trigo.v`): + + `elementary_functions/trigo.v` + + `elementary_functions/trigonometry_functions.v` + + `elementary_functions/trigonometry_integral.v` + +### Changed + +- in `Rstruct_topology.v`: + + lemma `RealsE` to include `RcosE`, `Rtrigo_PIE`, `RsinE` + +- moved from `prodnormedzmodule.v` to `unstable.v` + + module `ProdNormedZmodule` + * definition `norm` + * lemmas `normD`, `norm_eq0`, `normMn`, `normrN`, `prod_normE` + +- in `metric_structure.v`: + + order of arguments and implicit arguments of `squeeze_cvgr` + +- moved from `metric_structure.v` to `num_topology.v`: + + lemma `cvg_at_right_left_dnbhs`, generalized to `topologicalType` from `metricType`. + +- in `normed_module.v`: + + implicit arguments of `squeeze_cvge` and `sequeeze_fin` + +- in `derive.v`: + + instance `is_derive_mx` is now a lemma + +- moved from `realfun.v` to `derive.v`: + + lemmas `is_deriveV`, `is_derive1_comp` + +- moved from `trigo.v` to `trigonometry_integral.v`: + + lemmas `integral0_oneDsqr`, `integral0y_oneDsqr` + +- moved from `trigo.v` to `trigonometry_functions.v`: + + all contents except lemmas `integral0_oneDsqr`, `integral0y_oneDsqr` + +### Renamed + +- `mathcomp_extra.v` -> `mathcomp_compat.v` + +- in `esum.v`: + + `summable` -> `esummable` + + `summable_pinfty` -> `esummable_pinfty` + + `summableE` -> `esummableE` + + `summableD` -> `esummableD` + + `summableN` -> `esummableN` + + `summableB` -> `esummableB` + + `summable_funepos` -> `esummable_funepos` + + `summable_funeneg` -> `esummable_funeneg` + + `summable_fine_sum` -> `esummable_fine_sum` + + `summable_cvg` -> `esummable_cvg` + + `summable_nneseries_lim` -> `esummable_nneseries_lim` + + `summable_eseries` -> `esummable_eseries` + + `summable_eseries_esum` -> `esummable_eseries_esum` + +- in `lebesgue_integral_nonneg.v`: + + `summable_integral_dirac` -> `esummable_integral_dirac` + +- in `lebesgue_integrable.v`: + + `integrable_summable` -> `integrable_esummable` + +### Generalized + +- in `esum.v`: + + lemmma `le_esum` + +- from `pseudometric_normed_Zmodule.v` to `topology_structure.v`: + + lemma `continuous_comp_cvg` + +- in `pseudometric_normed_Zmodule.v`: + + lemma `within_continuous_continuous` + +- in `derive.v`: + + lemmas `derive1_comp`, `is_derive1_comp` (`realFieldType` -> `numFieldType`) + + lemmas `derive_shift`, `is_derive_shift` (function codomain) + +### Removed + +- in `unstable.v`: + + lemmas `le_bigmax_seq`, `bigmax_sup_seq` (now in MathComp 2.6.0) + +- in `boolp.v`: + + notations `eq_fun2`, `eq_fun3`, `eq_forall2`, `eq_forall3`, `eq_exists3` + (deprecated since 1.10.0) + +- in `classical_sets.v`: + + notations `preimage_itv_o_infty`, `preimage_itv_c_infty`, + `preimage_itv_infty_o`, `preimage_itv_infty_c` + (deprecated since 1.8.0) + +- in `set_interval.v`: + + notations `opp_itv_bnd_infty`, `opp_itv_infty_bnd` (deprecated since 1.9.0) + + notations `set_itv_infty_infty`, `set_itv_o_infty`, `set_itv_c_infty`, + `set_itv_infty_o`, `set_itv_infty_c`, `set_itv_pinfty_bnd`, + `set_itv_bnd_ninfty` (deprecated since 1.10.0) + +- in `Rstruct.v`: + + definition `Rinvx` (deprecated since 1.9.0) + +- in `real_interval.v`: + + notations `itv_bnd_infty_bigcup`, `itv_bnd_infty_bigcup0S`, `itv_infty_bnd_bigcup` + (deprecated since 1.9.0) + + notations `tv_c_inftyEbigcap`, `itv_bnd_inftyEbigcup`, `itv_o_inftyEbigcup` + (deprecated since 1.10.0) + +- file `prodnormedzmodule.v` + +- in `constructive_ereal.v`: + + notations `maxeMr`, `maxeMl`, `mineMr`, `mineMl` + (deprecated since 1.8.0) + +- in `uniform_structure.v`: + + notation `complete_ax` (deprecated) + +- in `num_topology.v`: + + notations `nbhs_lt`, `nbhs_le` (deprecated since 1.9.0) + +- in `normed_module.v`: + + notation `cvge_sub0` (deprecated since 1.9.0) + +- in `num_normedtype.v`: + + notation `cvgyNP` (deprecated since 1.9.0) + +- in `normed_module.v`: + + notations `cvgeMl`, `is_cvgeMl`, `cvgeMr`, `is_cvgeMr` (deprecated since 1.10.0) + +- in `derive.v`: + + notation `le0r_derive1_ndecr` (deprecated since 1.9.0) + + lemmas `ler0_derive1_nincr`, `gtr0_derive1_incr`, `ltr0_derive1_decr` (deprecated since 1.10.0) + +- in `measurable_function.v`: + + notation `preimage_class_measurable_fun` (deprecated since 1.9.0) + + notations `measurable_fun_prod`, `prod_measurable_funP`, + `measurable_pair1`, `measurable_pair2` (deprecated since 1.10.0) + +- in `measurable_structure.v`: + + notations `setDI_closed`, `setDI_semi_setD_closed`, `sedDI_closedP`, + `setringDI`, `preimage_classes`, `preimage_classes_comp` + (deprecated since 1.9.0) + +- in `lebesgue_integral_fubini.v`: + + notations `fubini1a`, `fubini1b`, `fubini1`, `fubini2` (deprecated since 1.10.0) + +- in `lebesgue_Rintegral.v`: + + notation `le_normr_integral` (deprecated since 1.10.0) + +- in `kernel.v`: + + notations `Kernel_isSFinite_subdef`, `Kernel_isSFinite_subdef.Build`, + `SFiniteKernel_isFinite`, `SFiniteKernel_isFinite.Build`, + `FiniteKernel_isSubProbability`, `FiniteKernel_isSubProbability.Build`, + `SubProbability_isProbability`, `SubProbability_isProbability.Build` (deprecated since 1.10.0) + +- in `hoelder.v`: + + notation `minkowski` (deprecated since 1.10.0) ## [1.17.0] - 2026-07-31 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 62967f76da..67bb43c3b6 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,221 +4,16 @@ ### Added -- in `pseudometric_normed_Zmodule.v`: - + lemmas `cvg0D`, `cvgD0`, `cvg0B`, `cvgB0`, `cvgN0` - -- in `normed_module.v`: - + lemmas `cvg1M`, `cvgM1`, `cvg0M`, `cvgM0` - + lemmas `cvg1Z`, `cvg0Z`, `cvgZ0` - -- in `normal_distribution.v`: - + definition `post_stddev` - + lemmas `post_stddev_gt0`, `post_stddevE` - + definition `post_mean` - + lemmas `normal_fun_conjugate`, `normal_pdf_conjugate`, `normal_prob_conjugate` - -- in `function_spaces.v`: - + lemma `within_continuous_big` - -- in `nat_topology.v`: - + lemma `near_infty_leq` - -- in `num_topology.v`: - + lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, - `at_left_shift`, `at_right_shift` -- in `esum.v`: - + lemmas `pos_esum_ge1`, `le_pos_esum_fine`, `sum_esum_ge`, `le_esum_fine`, - `subset_esum`, `esum0`, `esum_if_eq_op_set1`, `esum_neq0`, `esum_ge1` - + lemmas `eq_esummable`, `le_esummable`, `esummableZl`, `esummableZr`, - `esummableMl`, `esummableMr`, `esummableM` - + lemmas `esummable_esum_funepos`, `esummable_esum_funeneg`, - `esummable_esum_fin_num`, `esummable_esumN` - + lemma `esumE` - + lemmas `esummable_esumZ`, `esummable_esumD`, `esummableB` - -- new files (result of the splitting of `trigo.v`): - + `elementary_functions/trigo.v` - + `elementary_functions/trigonometry_functions.v` - + `elementary_functions/trigonometry_integral.v` - -- in `topology_structure.v`: - + lemma `id_continuous` - -- in `derive.v`: - + lemmas `derive1Dn`, `der1_scaleLR`, `deriveZLR`, `derivableZLR`, - `derivable_comp_shift`, `derive_comp_shift`, `is_derive_comp_shift`, `derive1_comp_shift`, - `near_eq_derive1n_near`, `near_eq_derive1_near`, `near_eq_derive1n`, - `near_eq_derive1` - + global instance `is_derive_exp` - + lemma `derive1_shift` - -- in `Rstruct_topology.v`: - + lemmas `RcosE`, `Rtrigo_PIE`, `RsinE` - -- in `measurable_realfun.v`: - + lemma `measurable_bigmaxr` -- in `matrix_normedtype.v`: - + lemma `norm_trmx` - -- in `derive.v`: - + lemmas `derivable_trmx`, `derive_trmx` - + global instance `is_derive_trmx` - ### Changed -- in `derive.v`: - + instance `is_derive_mx` is now a lemma - -- moved from `metric_structure.v` to `num_topology.v`: - + lemma `cvg_at_right_left_dnbhs`, generalized to `topologicalType` from `metricType`. - -- moved from `trigo.v` to `trigonometry_integral.v`: - + lemmas `integral0_oneDsqr`, `integral0y_oneDsqr` - -- moved from `trigo.v` to `trigonometry_functions.v`: - + all contents except lemmas `integral0_oneDsqr`, `integral0y_oneDsqr` - -- moved from `realfun.v` to `derive.v`: - + lemmas `is_deriveV`, `is_derive1_comp` - -- in `Rstruct_topology.v`: - + lemma `RealsE` to include `RcosE`, `Rtrigo_PIE`, `RsinE` - -- in `metric_structure.v`: - + order of arguments and implicit arguments of `squeeze_cvgr` - -- in `normed_module.v`: - + implicit arguments of `squeeze_cvge` and `sequeeze_fin` -- moved from `prodnormedzmodule.v` to `unstable.v` - + module `ProdNormedZmodule` - * definition `norm` - * lemmas `normD`, `norm_eq0`, `normMn`, `normrN`, `prod_normE` - ### Renamed -- in `esum.v`: - + `summable` -> `esummable` - + `summable_pinfty` -> `esummable_pinfty` - + `summableE` -> `esummableE` - + `summableD` -> `esummableD` - + `summableN` -> `esummableN` - + `summableB` -> `esummableB` - + `summable_funepos` -> `esummable_funepos` - + `summable_funeneg` -> `esummable_funeneg` - + `summable_fine_sum` -> `esummable_fine_sum` - + `summable_cvg` -> `esummable_cvg` - + `summable_nneseries_lim` -> `esummable_nneseries_lim` - + `summable_eseries` -> `esummable_eseries` - + `summable_eseries_esum` -> `esummable_eseries_esum` - -- in `lebesgue_integrable.v`: - + `integrable_summable` -> `integrable_esummable` - -- in `lebesgue_integral_nonneg.v`: - + `summable_integral_dirac` -> `esummable_integral_dirac` -- `mathcomp_extra.v` -> `mathcomp_compat.v` - ### Generalized -- in `esum.v`: - + lemmma `le_esum` - -- from `pseudometric_normed_Zmodule.v` to `topology_structure.v`: - + lemma `continuous_comp_cvg` -- in `derive.v`: - + lemmas `derive1_comp`, `is_derive1_comp` (`realFieldType` -> `numFieldType`) - + lemmas `derive_shift`, `is_derive_shift` (function codomain) - -- in `pseudometric_normed_Zmodule.v`: - + lemma `within_continuous_continuous` - ### Deprecated ### Removed -- in `unstable.v`: - + lemmas `le_bigmax_seq`, `bigmax_sup_seq` (now in MathComp 2.6.0) - -- in `classical_sets.v`: - + notations `preimage_itv_o_infty`, `preimage_itv_c_infty`, - `preimage_itv_infty_o`, `preimage_itv_infty_c` - (deprecated since 1.8.0) - -- in `constructive_ereal.v`: - + notations `maxeMr`, `maxeMl`, `mineMr`, `mineMl` - (deprecated since 1.8.0) - -- in `derive.v`: - + notation `le0r_derive1_ndecr` (deprecated since 1.9.0) - -- in `set_interval.v`: - + notations `opp_itv_bnd_infty`, `opp_itv_infty_bnd` (deprecated since 1.9.0) - -- in `Rstruct.v`: - + definition `Rinvx` (deprecated since 1.9.0) - -- in `real_interval.v`: - + notations `itv_bnd_infty_bigcup`, `itv_bnd_infty_bigcup0S`, `itv_infty_bnd_bigcup` - (deprecated since 1.9.0) - -- in `num_topology.v`: - + notations `nbhs_lt`, `nbhs_le` (deprecated since 1.9.0) - -- in `normed_module.v`: - + notation `cvge_sub0` (deprecated since 1.9.0) - -- in `num_normedtype.v`: - + notation `cvgyNP` (deprecated since 1.9.0) - -- in `measurable_function.v`: - + notation `preimage_class_measurable_fun` (deprecated since 1.9.0) - -- in `measurable_structure.v`: - + notations `setDI_closed`, `setDI_semi_setD_closed`, `sedDI_closedP`, - `setringDI`, `preimage_classes`, `preimage_classes_comp` - (deprecated since 1.9.0) - -- file `prodnormedzmodule.v` - -- in `uniform_structure.v`: - + notation `complete_ax` (deprecated) - -- in `derive.v`: - + lemmas `ler0_derive1_nincr`, `gtr0_derive1_incr`, `ltr0_derive1_decr` (deprecated since 1.10.0) - -- in `boolp.v`: - + notations `eq_fun2`, `eq_fun3`, `eq_forall2`, `eq_forall3`, `eq_exists3` (deprecated since 1.10.0) - -- in `set_interval.v`: - + notations `set_itv_infty_infty`, `set_itv_o_infty`, `set_itv_c_infty`, - `set_itv_infty_o`, `set_itv_infty_c`, `set_itv_pinfty_bnd`, - `set_itv_bnd_ninfty` (deprecated since 1.10.0) - -- in `real_interval.v: - + notations `tv_c_inftyEbigcap`, `itv_bnd_inftyEbigcup`, `itv_o_inftyEbigcup` (deprecated since 1.10.0) - -- in `hoelder.v`: - + notation `minkowski` (deprecated since 1.10.0) - -- in `kernel.v`: - + notations `Kernel_isSFinite_subdef`, `Kernel_isSFinite_subdef.Build`, - `SFiniteKernel_isFinite`, `SFiniteKernel_isFinite.Build`, - `FiniteKernel_isSubProbability`, `FiniteKernel_isSubProbability.Build`, - `SubProbability_isProbability`, `SubProbability_isProbability.Build` (deprecated since 1.10.0) - -- in `lebesgue_integral_fubini.v`: - + notations `fubini1a`, `fubini1b`, `fubini1`, `fubini2` (deprecated since 1.10.0) - -- in `lebesgue_Rintegral.v`: - + notation `le_normr_integral` (deprecated since 1.10.0) - -- in `measurable_function.v` - + notations `measurable_fun_prod`, `prod_measurable_funP`, - `measurable_pair1`, `measurable_pair2` (deprecated since 1.10.0) - -- in `normed_module.v`: - + notations `cvgeMl`, `is_cvgeMl`, `cvgeMr`, `is_cvgeMr` (deprecated since 1.10.0) - ### Infrastructure ### Misc diff --git a/INSTALL.md b/INSTALL.md index 367b672e80..56d8142acb 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -19,12 +19,12 @@ Detailed instructions for possible installations of Mathematical Components are ## Short Instructions - Through opam: - + type `opam install coq-mathcomp-analysis.X.Y.Z` where `X.Y.Z` is the version number + + type `opam install rocq-mathcomp-analysis.X.Y.Z` where `X.Y.Z` is the version number (all the dependencies should be automatically installed, assuming `opam` has been properly configured and `coq-released` repository is added) - Custom: + first, install the required dependencies, for example with opam - type `opam install --deps-only coq-mathcomp-analysis.X.Y.Z` + type `opam install --deps-only rocq-mathcomp-analysis.X.Y.Z` + assuming the requirements are met, type `make` to use the provided `Makefile` ## From scratch instructions @@ -46,11 +46,11 @@ $ opam repo add rocq-released https://rocq-prover.org/opam/released ``` 3. Install our package (and all its dependencies) ``` -$ opam install coq-mathcomp-analysis +$ opam install rocq-mathcomp-analysis ``` To install a precise version, type, say ``` -$ opam install coq-mathcomp-analysis.1.17.0 +$ opam install rocq-mathcomp-analysis.1.18.0 ``` 4. Everytime you want to work in this same context, you need to type ``` @@ -61,9 +61,9 @@ $ eval `opam config env` ### How to edit and test the source code If you would rather edit and test the files than intalling them, we suggest that you replace -`opam install coq-mathcomp-analysis` command with the following +`opam install rocq-mathcomp-analysis` command with the following ``` -$ opam install coq-mathcomp-analysis --deps-only +$ opam install rocq-mathcomp-analysis --deps-only $ git clone https://github.com/math-comp/analysis $ cd analysis $ make @@ -73,7 +73,7 @@ using [proof general for emacs](https://github.com/ProofGeneral/PG) ## Break-down of phase 3 of the installation procedure step by step -With the example of Coq 9.1.1 and MathComp 2.6.0. For other versions, update the +With the example of Rocq 9.1.1 and MathComp 2.6.0. For other versions, update the version numbers accordingly. 1. Install Rocq 9.1.1 @@ -88,7 +88,7 @@ $ opam install rocq-mathcomp-field.2.6.0 ``` $ opam install rocq-mathcomp-finmap.2.4.0 ``` -5. Download and compile `coq-mathcomp-analysis` without installing +5. Download and compile `rocq-mathcomp-analysis` without installing ``` $ git clone https://github.com/math-comp/analysis $ cd analysis @@ -97,11 +97,11 @@ $ make ## How to clean your computer -- If you installed the package `coq-mathcomp-analysis` and wish to get rid of it, just type +- If you installed the package `rocq-mathcomp-analysis` and wish to get rid of it, just type ``` -$ opam remove coq-mathcomp-analysis +$ opam remove rocq-mathcomp-analysis ``` -- However if you wish to clean the entire installation (including `coq` and `mathcomp` dependencies) +- However if you wish to clean the entire installation (including `rocq` and `mathcomp` dependencies) you should remove the opam root we created for this purpose: ``` $ rm -rf ~/.opam_mathcomp_analysis diff --git a/README.md b/README.md index d965e18da2..d8dc84172c 100644 --- a/README.md +++ b/README.md @@ -9,16 +9,16 @@ [chat-shield]: https://img.shields.io/badge/zulip-join_chat-brightgreen.svg [chat-link]: https://rocq-prover.zulipchat.com/#narrow/channel/237666-math-comp-analysis -This repository contains a real analysis library for the Coq / Rocq proof-assistant. +This repository contains a real analysis library for the Rocq proof-assistant. It is based on the [Mathematical Components](https://math-comp.github.io/) library. In terms of [opam](https://opam.ocaml.org/doc/Install.html), it comes as the following packages: -- `coq-mathcomp-classical`: a layer for classical reasoning -- `coq-mathcomp-reals`: real numbers for MathComp -- `coq-mathcomp-reals-stdlib`: compatibility with the real numbers of the Coq standard library -- `coq-mathcomp-analysis-stdlib`: compatibility with the Coq standard library (topology only) -- `coq-mathcomp-analysis`: theories for real analysis -- `coq-mathcomp-experimental-reals`: sequences of real numbers and distributions (experimental) +- `rocq-mathcomp-classical`: a layer for classical reasoning +- `rocq-mathcomp-reals`: real numbers for MathComp +- `rocq-mathcomp-reals-stdlib`: compatibility with the real numbers of the Rocq standard library +- `rocq-mathcomp-analysis-stdlib`: compatibility with the Rocq standard library (topology only) +- `rocq-mathcomp-analysis`: theories for real analysis +- `rocq-mathcomp-experimental-reals`: sequences of real numbers and distributions (experimental) ## Meta From 5c5ba4919a7dec246c916ef700f078355dbe18b5 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 2 Sep 2026 15:05:09 +0900 Subject: [PATCH 2/2] fix --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index d8dc84172c..4c464e3f26 100644 --- a/README.md +++ b/README.md @@ -24,7 +24,7 @@ In terms of [opam](https://opam.ocaml.org/doc/Install.html), it comes as the fol - [Authors](AUTHORS.md) - License: [CeCILL-C](LICENSE) -- Compatible Rocq versions: Rocq 9.0 and 9.1 (or dev) +- Compatible Rocq versions: Rocq 9.0--9.3 (or dev) - Additional dependencies: - [MathComp boot 2.6.0 or later](https://math-comp.github.io) - [MathComp finite-group 2.6.0 or later](https://math-comp.github.io) @@ -66,7 +66,7 @@ Each file is documented in its header in ASCII. HTML rendering of the source code and inheritance diagrams for the mathematical structures that MathComp-Analysis adds on top of MathComp's ones (using [`rocqnavi`](https://github.com/affeldt-aist/rocqnavi)): -- last version: [1.17.0](https://math-comp.github.io/analysis/htmldoc/1_17_0/index.html) +- last version: [1.18.0](https://math-comp.github.io/analysis/htmldoc/1_18_0/index.html) - [master](https://math-comp.github.io/analysis/master/) Overview presentations: