| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
