| Commit message (Collapse) | Author | Age |
... | |
| | | | | | | |
|
| |/ / / / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
I reused the sentence from the version 8.7 credits.
It wasn't initially decided like this but it looks like
I'm the de facto maintainer for this release as well.
|
|\ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ |
|
| | | | | | | | |
|
|\ \ \ \ \ \ \ \ |
|
| |_|/ / / / / /
|/| | | | | | |
| | | | | | | | |
I knew this feature existed but I did not remember the syntax and I could not find it in the manual
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | |
|
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
It's a bit shorter and more direct.
|
| |_|_|_|_|/ / / /
|/| | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ |
|
| |_|_|/ / / / / /
|/| | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ |
|
|/ / / / / / / / / / |
|
|\ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
We are now actively looking for sponsors, let's make our communication
more visible.
|
| | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|_|/ /
|/| | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
This shall eventually allow to use contexts of declarations in the
definition of the "Case" constructor.
Basically, this means that Constr now includes Context and that the
"t" types of Context which were specialized on constr are not defined
in Constr (unfortunately using a heavy boilerplate).
|
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
in notations).
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
We use a buffer instead of O(n) appending to a string, and we also
make the parser tail-call.
|
| |/ / / / / / / / / /
|/| | | | | | | | | | |
|
| | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | |
|
| | | | | | |_|/ / / /
| | | | | |/| | | | | |
|
| | | | |_|_|/ / / /
| | | |/| | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Was revealing a critical bug in VM universe handling introduced in 8.5.
|
|\ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|/ / / / /
|/| | | | | | | | | | |
|
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
We fix the issue by removing terms of the substitutions which have
free variables and are thus not interpretable in the context of the
"ltac:" subterm.
This remains rather ad hoc, since, in an expression "Notation f x :=
ltac:(foo)", we interpret "x" at calling time of "foo" rather than at
use time of "x" in foo, even if "x" is not necessary.
We could also imagine that binders in the ltac expressions are then
interpreted but that would start to be (very) complicated.
Note that this will presumably "fix" ltac2 quotations at the same
time.
|
|\ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|/ / / / / /
|/| | | | | | | | | |
| | | | | | | | | | | |
constants
|
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
obligations.
|
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
build
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | | | |
|
| | | | | | | | | |/ / / / / / |
|
| | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
Apparently it was not useful. I don't remember what I was thinking
when I added it.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|/ / / / / /
|/| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
subtyping.
|
| |_|_|_|_|_|_|_|_|/ / / / / /
|/| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
On the way I also fixed some minor issues with calling MakeCoq_MinGW from cygwin.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|/ / / / / / / / /
|/| | | | | | | | | | | | | | |
|