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