1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
# Origins of the files in this repository
This description corresponds to the first releases.
## Original files from this library
- `posnum.v`
- `classical_set.v`
- `topology.v` (with uniform space (now renamed pseudo metric space) and complete space inspired from Coquelicot's `hierarchy.v`)
- `normedtype.v` (with normed and complete normed spaces inspired from Coquelicot's `hierarchy.v`)
- `landau.v`
- `derive.v`
- `README.md`
- `AUTHORS.md`
- `FILES.md`
- `INSTALL.md`
- `_CoqProject`
- `Makefile`
- `Licence_CeCILL-C_V1-en.txt`
## Files from the former library coq-alternate-reals are now here and should be merged at some point:
- `boolp.v`
- `dedekind.v`
- `discrete.v`
- `distr.v`
- `reals.v`
- `realseq.v`
- `realsum.v`
- `xfinmap.v`
- `xsets.v`
## Files modified from Coquelicot 3.0.1
- `Rbar.v` (now removed in favor of `ereal.v`)
## Other files
- `Rstruct.v` from CoqApprox, with contributions from Sophie Bernard, from her repository (https://github.com/Sobernard/Struct/blob/master/Rstruct.v), and modified to instantiate structures from coq-alternate-reals.
- `forms.v` by Cyril Cohen and Laurence Rideau, temporarily added to this repository until it is merged in the Mathematical Components library
|
