| Commit message (Collapse) | Author | Age |
... | |
| | | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|/ / / / / / / / / / / /
|/| | | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|/ / / / / / / /
|/| | | | | | | | | | | | | | |
|
| |_|_|/ / / / / / / / / / /
|/| | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
Fixes #6963.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|/ / / / / / / / / /
|/| | | | | | | | | | | | | |
|
|/ / / / / / / / / / / / / |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|/ / / / / / / /
|/| | | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| |/ / / / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|_|_|_|/ / / /
|/| | | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
Most of these warnings should really be errors (ill-formed input,
invalid cross references, etc.) so we make it the default.
|
| | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
The Ubuntu Font License requires substantially modified fonts to be renamed
entirely.
|
| |/ / / / / / / / / / / / / /
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
Including cross-reference TODOs.
I took down the number of warnings from 300 to 50.
|
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
Chapter ported by Théo Zimmermann and Maxime Dénès.
|
|/ / / / / / / / / / / / / / |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|/ / / / / /
|/| | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| |_|/ / / / / / / / / / / /
|/| | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
Fixes #7243.
|
| |_|_|_|_|_|_|_|_|_|/ / /
|/| | | | | | | | | | | | |
|
| |_|_|_|_|_|_|/ / / / /
|/| | | | | | | | | | | |
|
| | | | | | | | | | | | |
|
| |/ / / / / / / / / /
|/| | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
|
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
contains evars
|
| |_|_|/ / / / / / / /
|/| | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
LTAC's `fix` and `cofix` do require access to the proof object inside
the tactic monad when used without a name. This is a bit inconvenient
as we aim to make the handling of the proof object purely functional.
Alternatives have been discussed in #7196, and it seems that
deprecating the nameless forms may have the best cost/benefit ratio,
so opening this PR for discussion.
See also #6171.
|
| | | | | | | | | | | |
|
| |/ / / / / / / / /
|/| | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ |
|
| |_|_|_|/ / / / / /
|/| | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
We take into account all future ipats, not just the ones in
the current branch
|
|\ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
removing the test.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
The "Stream.Error" printer does add a period, so, the messages
themselves should not.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | |
anymore
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | |
failure in other file
|
| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | |
Thanks to Clément Pit Claudel for porting this chapter.
Backport universe polymorphism changes from 2017 and 2018.
|
| |_|_|_|_|_|_|_|_|_|/ / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | |
These were used very inconsistenty, serve no purpose and the link
to the source is particularly useless because it's a moving target.
|
| |_|_|_|_|_|_|_|_|_|/ / / / / / / / /
|/| | | | | | | | | | | | | | | | | | |
|