| Commit message (Collapse) | Author | Age |
|\
| |
| |
| | |
"_something")
|
|\ \
| | |
| | |
| | | |
inductive definition)
|
|\ \ \ |
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
BZ#4852)
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | |
|
| |_|/ / / / / / /
|/| | | | | | | | |
|
| |_|/ / / / / /
|/| | | | | | |
| | | | | | | |
| | | | | | | | |
Also simplifies the way it is presented (no need to be overly precise).
|
| | | | | | | | |
|
|\ \ \ \ \ \ \ \
| |_|/ / / / / /
|/| | | | | | | |
|
|\ \ \ \ \ \ \ \ |
|
| | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
to escape non-UTF-8 file names)
|
|\ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
BZ#5757)
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
cleared context.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|_|/ / / / /
|/| | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
coq_makefile are in sync (supersed #1039)…
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| |_|_|_|_|_|_|_|_|_|_|/ / / /
|/| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
BZ#4852)
This code simplification isn't that important, but it can trigger further
simplifications elsewhere, see for instance BZ#4852.
NB: normally, the extraction favors eta-expanded forms, since that's the usual
way to avoid issues about '_a type variables that cannot be generalized. But
the atomic eta-reductions done here shouldn't be problematic (no applications
put outside of functions).
|
| |_|_|_|_|_|_|_|_|_|_|/ / /
|/| | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
The typical Coq `Pp.t` document contains a lot of "gluing" which
produces efficient structures but it is quite painful in
serialization.
We optimize a common document building case so we don't create as much
glue nodes as with the "naive" strategy, and without incurring in the
large performance cost full flattening would produce.
This is a temporal fixup, see #505 for more context on the discussion
and medium-term plans.
|
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
This is inconvenient because it can only be tested on tags
and it didn't work for V8.7+beta1.
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
This includes _ and insecable space which can be used in idents and
this allows more precise heuristics.
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | |/ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ /
|/| | | | | | | | | | | | | | | |
|
| | | | | | | | | | | |_|_|_|/
| | | | | | | | | | |/| | | | |
|
| | | | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | |
proof for coqwc
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
3e70ea9c.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
?INTERNAL#42 style is ugly
|
| | | | | | | | | | | | | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | |
See also GeoCoq/GeoCoq#7.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
an OCaml "when" clause to the r.h.s of the matching clause
|