| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
Imitating the kernel in anticipation for the kernel being more obedient
|
|
|
|
This doesn't change behaviour currently as the kernel also makes this
decision, but in the future it won't.
|
|
|
|
It seems people don't always look at the test suite readme.
|
|
This allows for nicer formatting without having to deal with Make's
semantic whitespace.
|
|
|
|
|
|
|
|
|
|
compilation.
|
|
branches and return predicate
|
|
As far as I know, this plugin is untested and barely maintained. I don't
think it has real use cases any more, so let's move it out from the repo
and see if somebody wants to take over and maintain it.
We also remove the documentation, which was telling our users to look at
ring to see an example of reification done using quote, when in fact it
wasn't using it anymore.
|
|
|
|
|
|
|
|
arguments
|
|
|
|
|
|
make make-pretty-timed- after -> make make-pretty-timed-after (remove
space between - and after) (and reflow paragraph)
Fix spacing around :: in print-pretty-single-time-diff
Closes #8396
|
|
This concerns e.g. "?[id]", "?[?id]" or "?id" (in terms, not in
patterns), so that all names occurring in terms are consistently
interpreted as ltac names.
Moreover, with that, we can for instance do:
Ltac pick x := eexists ?[x].
Goal exists x, x = 0.
pick foo.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(It's unused after moving coercions to globrefs)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
from compiles files
|
|
variables
|
|
|
|
|
|
|
|
Removing in passing two Local which are no-ops in practice.
|
|
This is for use in modules. By default, the behavior is local in
sections and Global is forbidden in sections. By default, the behavior
is global in modules.
|
|
|
