| Commit message (Collapse) | Author | Age |
... | |
| | | | | | |
|
| | | | |/
| | | |/|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
In some cases, Format's inner boxes inside an outer box act as break
hints, even though there are already "better" break hints in the outer
box.
We work around this "feature" by not inserting a box around the
default printing rule for a notation if there is no effective break
points in the box.
See https://caml.inria.fr/mantis/view.php?id=7804 for the related
OCaml discussion.
|
| | | |/ |
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
constr in Constr
|
| |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | | |
Fixes #7666. Due to shared mapping of executables Linux doesn't allow
to overwrite binaries that are running; we do as `ocamlopt` and delete
the target file before copy.
|
|\ \ \ \ |
|
|\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
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.
|
| | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|_|/ /
|/| | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
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
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | | | |
|
| | | | | | | | | |/ / / / / / |
|