diff --git a/README.md b/README.md index e1615b4a2..336a25e70 100644 --- a/README.md +++ b/README.md @@ -89,6 +89,7 @@ We try to preserve backward compatibility as best as we can. Each file is documented in its header in ASCII. [HTML rendering of the source code](https://math-comp.github.io/analysis/htmldoc_1_7_0/index.html) (using a fork of [`coq2html`](https://github.com/xavierleroy/coq2html)). +It includes inheritance diagrams for the mathematical structures that MathComp-Analysis adds on top of MathComp's ones. Overview presentations: - [Classical Analysis with Coq](https://perso.crans.org/cohen/CoqWS2018.pdf) (2018) @@ -110,24 +111,6 @@ Other work using MathComp-Analysis: - [Experimenting with an intrinsically-typed probabilistic programming language in Coq](https://staff.aist.go.jp/reynald.affeldt/documents/syntax-aplas2023.pdf) (2023) - [Taming Differentiable Logics with Coq Formalisation](https://drops.dagstuhl.de/storage/00lipics/lipics-vol309-itp2024/LIPIcs.ITP.2024.4/LIPIcs.ITP.2024.4.pdf) (2024) -## Mathematical structures - -MathComp-Analysis adds mathematical structures on top of MathComp's ones. -The following inheritance diagram displays the resulting hierarchy as of version 1.1.0 -(excluding most MathComp structures). -The structures introduced by MathComp-Analysis are highlighted. -(See `topology.v`, `normedtype.v`, `reals.v`, `measure.v`.) - -Main_inheritance_graph - - -### Hierarchies of functions - -| Functions | Functions with a finite image | Measures | Kernels | -|:----------:|:-----------------------------:|:--------:|:-------:| -| Functions | Functions_with_a_finite_image | Measures | Kernels | -| (see `functions.v`) | (see `cardinality.v`, `lebesgue_integral.v`) | (see `measure.v`, `charge.v`) | (see `kernel.v`) | - ## Development information [Detailed requirements and installation procedure](INSTALL.md) diff --git a/etc/hierarchy_fimfun.1.1.0.png b/etc/hierarchy_fimfun.1.1.0.png deleted file mode 100644 index 5c8dd645f..000000000 Binary files a/etc/hierarchy_fimfun.1.1.0.png and /dev/null differ diff --git a/etc/hierarchy_functions.1.1.0.png b/etc/hierarchy_functions.1.1.0.png deleted file mode 100644 index f6eb6575b..000000000 Binary files a/etc/hierarchy_functions.1.1.0.png and /dev/null differ diff --git a/etc/hierarchy_kernel.1.1.0.png b/etc/hierarchy_kernel.1.1.0.png deleted file mode 100644 index 9b13c4d0b..000000000 Binary files a/etc/hierarchy_kernel.1.1.0.png and /dev/null differ diff --git a/etc/hierarchy_main.1.1.0.png b/etc/hierarchy_main.1.1.0.png deleted file mode 100644 index e56906426..000000000 Binary files a/etc/hierarchy_main.1.1.0.png and /dev/null differ diff --git a/etc/hierarchy_measure.1.1.0.png b/etc/hierarchy_measure.1.1.0.png deleted file mode 100644 index 6dd713ec4..000000000 Binary files a/etc/hierarchy_measure.1.1.0.png and /dev/null differ