| Commit message (Collapse) | Author | Age |
|\ |
|
|\ \ |
|
|\ \ \
| | | |
| | | | |
Simplify the newring hack
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Primary maintainers should be responsive.
[ci skip]
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
global env
|
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
| |_|/ / / / / / / / / /
|/| | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
We remove the `fix N / cofix N` forms from the tactic language. This
way, these tactics don't depend anymore on the proof context, in
particular on the proof name, which seems like a fragile practice.
Apart from the concerns wrt maintenability of proof scripts, this also
helps making the "proof state" functional; as we don't have to
propagate the proof name to the tactic layer.
|
|/ / / / / / / / / / /
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
Caused by a semantic conflict with the separate toplevels PR.
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
comments.
[ci skip]
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
[ci skip]
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
Clarification prompted by Jim Fehrle.
[ci skip]
|
|\ \ \ \ \ \ \ \ \ \ \ \
| |/ / / / / / / / / / /
|/| | | | | | | | | | |
| | | | | | | | | | | | |
in CArray
|
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
spawn timeout.
|
| |_|/ / / / / / / / / /
|/| | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
instances
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|/ / / / / / / / / / /
|/| | | | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
This follows the model of smartmap and smartmap2.
|
| |_|_|_|_|_|/ / / / / / / / / /
|/| | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|_|_|/ / / / /
|/| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
As per PR comment suggestion
|
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
There were a few spurious dependencies on the `Vernac` AST in the
pretyper, we remove them and move `Vernacexpr` and `Extend` to parsing,
where they do belong more.
|
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
`Proof_global` is the main consumer of the flag, which doesn't seem to
belong to the AST as plugins show.
This will allow the vernac AST to be placed in `vernac` indeed.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |/ / / / / / / / / / / / / /
|/| | | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
This should hopefully alleviate memory problems on gitlab, by first
building the `lite` targets, and then building the remaining
not-that-big targets.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|/ / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
lib.cma).
|
| |_|_|_|_|_|_|/ / / / / / / / /
|/| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
This closes #7580
c.f. https://github.com/coq/coq/pull/7559#issuecomment-390749207 and
https://github.com/coq/coq/pull/7559#issuecomment-390872924. This
should be reverted if and when we move to autogenerated docs for
warnings and errors, as suggested in #7373.
|