Readme 20240417 (#1211)

* add all_analysis.v file

CHANGELOG_UNRELEASED.md

@@ -29,6 +29,7 @@
 
 - in `realfun.v`
   + lemmas `total_variation_nondecreasing`, `total_variation_bounded_variation`
+- new file `theories/all_analysis.v`
 
 ### Changed
 

README.md

@@ -70,21 +70,22 @@ make   # or make -j <number-of-cores-on-your-machine>
 make install
 ```
 
-## Disclaimer
+## About the stability of this library
 
-This library is still at an experimental stage.  Contents may
-change, definitions and theorems may be renamed, and inference
-mechanisms may be replaced at any major version bump.  Use at your
-own risk.
+Changes are documented systematically in [CHANGELOG.md](CHANGELOG.md) and
+[CHANGELOG_UNRELEASED.md](CHANGELOG_UNRELEASED.md).
+
+We bump the minor part of the version number for breaking changes.
+
+We use deprecation warnings to help transitioning to new versions.
+
+We try to preserve backward compatibility as best as we can.
 
 ## Documentation
 
 Each file is documented in its header
 ([`coq2html`](https://github.com/xavierleroy/coq2html) [documentation for the last version](https://math-comp.github.io/analysis/htmldoc_1_1_0/index.html)).
 
-Changes are documented in [CHANGELOG.md](CHANGELOG.md) and
-[CHANGELOG_UNRELEASED.md](CHANGELOG_UNRELEASED.md).
-
 Overview presentation: [Classical Analysis with Coq](https://perso.crans.org/cohen/CoqWS2018.pdf) (2018)
 
 See also "Related publication(s)" [above](https://github.com/math-comp/analysis#meta).

_CoqProject

@@ -17,6 +17,7 @@ classical/functions.v
 classical/cardinality.v
 classical/fsbigop.v
 classical/set_interval.v
+theories/all_analysis.v
 theories/constructive_ereal.v
 theories/ereal.v
 theories/reals.v

theories/Make

@@ -40,6 +40,7 @@ itv.v
 convex.v
 charge.v
 kernel.v
+all_analysis.v
 altreals/xfinmap.v
 altreals/discrete.v
 altreals/realseq.v

theories/all_analysis.v

@@ -0,0 +1,33 @@
+From mathcomp Require Export constructive_ereal.
+From mathcomp Require Export ereal.
+From mathcomp Require Export reals.
+From mathcomp Require Export landau.
+From mathcomp Require Export Rstruct.
+From mathcomp Require Export topology.
+From mathcomp Require Export function_spaces.
+From mathcomp Require Export cantor.
+From mathcomp Require Export prodnormedzmodule.
+From mathcomp Require Export normedtype.
+From mathcomp Require Export realfun.
+From mathcomp Require Export sequences.
+From mathcomp Require Export exp.
+From mathcomp Require Export trigo.
+From mathcomp Require Export nsatz_realtype.
+From mathcomp Require Export esum.
+From mathcomp Require Export real_interval.
+From mathcomp Require Export lebesgue_measure.
+From mathcomp Require Export forms.
+From mathcomp Require Export derive.
+From mathcomp Require Export measure.
+From mathcomp Require Export numfun.
+From mathcomp Require Export lebesgue_integral.
+From mathcomp Require Export ftc.
+From mathcomp Require Export hoelder.
+From mathcomp Require Export probability.
+From mathcomp Require Export lebesgue_stieltjes_measure.
+From mathcomp Require Export summability.
+From mathcomp Require Export signed.
+From mathcomp Require Export itv.
+From mathcomp Require Export convex.
+From mathcomp Require Export charge.
+From mathcomp Require Export kernel.

theories/forms.v

@@ -26,7 +26,7 @@ Reserved Notation "'[ u , v ]_ M"
 Reserved Notation "'[ u ]_ M" (at level 2, format "''[' u ]_ M").
 Reserved Notation "'[ u ]" (at level 2, format "''[' u ]").
 Reserved Notation "u '``_' i"
-    (at level 3, i at level 2, left associativity, format "u '``_' i").
+    (at level 3, i at level 2, format "u '``_' i").
 Reserved Notation "A ^_|_"    (at level 8, format "A ^_|_").
 Reserved Notation "A _|_ B" (at level 69, format "A  _|_  B").
 Reserved Notation "eps_theta .-sesqui" (at level 2, format "eps_theta .-sesqui").