| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
I knew this feature existed but I did not remember the syntax and I could not find it in the manual
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
On the way I also fixed some minor issues with calling MakeCoq_MinGW from cygwin.
|
|
|
|
Not sure it could have led to a soundness bug, but this is definitely
serious enough to deserve a backport. Also made the code robust by
listing all the constructors.
|
|
Both reminded by Enrico.
|
|
|
|
|
|
|
|
|
