Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

upd readme #1283

Merged
merged 1 commit into from
Aug 6, 2024
Merged

upd readme #1283

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -130,17 +130,17 @@ The structures introduced by MathComp-Analysis are highlighted.

This library was inspired by the [Coquelicot library](http://coquelicot.saclay.inria.fr/)
by Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond.
`topology.v` and `normedtype.v` contained a reimplementation of file
In the first releases, `topology.v` and `normedtype.v` contained a reimplementation of the file
`Hierarchy.v` from the library Coquelicot.

The instantiation of the mathematical structures of the Mathematical Components library
with the real numbers of the standard Coq library used a well-known file (`Rstruct.v`)
from the [CoqApprox library](http://tamadi.gforge.inria.fr/CoqApprox/) (with
modifications from various authors).
modifications by various authors).

Our proof of Zorn's Lemma in `classical_sets.v` (NB: new filename) is a reimplementation
of the one by Daniel Schepler (https://github.com/coq-community/zorns-lemma); we also took
inspiration from his work on topology (https://github.com/coq-community/topology) for parts
The proof of Zorn's Lemma in `classical_sets.v` (NB: new filename) was a reimplementation
of the one by Daniel Schepler (https://github.com/coq-community/zorns-lemma) but it has been rewritten for version 1.3.0;
we also originally took inspiration from Schepler's work on topology (https://github.com/coq-community/topology) for parts
of `topology.v`.

[ORIGINAL_FILES.md](ORIGINAL_FILES.md) gives more details about the
Expand Down
Loading