| Commit message (Collapse) | Author | Age |
... | |
| |_|_|_|_|_|_|_|_|_|/ / / /
|/| | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
This was completely wrong, such a term could not even be type-checked by
the kernel as it was internally using a match construct over a negative
record. They were luckily only used in upper layers, namley printing
and extraction.
Recomputing the projection body might be costly in detyping, but this only
happens when the compatibility flag is turned on, which is not the default.
Such flag is probably bound to disappear anyways.
Extraction should be fixed though so as to define directly primitive
projections, similarly to what has been done in native compute.
|
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
This field was not used inside the kernel and not used in
performance-critical code where caching is essential, so we extrude
the code that computes it out of the kernel.
|
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
This reduces kernel bloat and removes code from the TCB, as compatibility
projections are now retypechecked as normal definitions would have been.
This should have no effect on efficiency as this only happens once at
definition time.
|
| |_|_|_|_|/ / / / / / / / /
|/| | | | | | | | | | | | | |
|
| |_|_|_|_|/ / / / / / / /
|/| | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
This field used to signal that a constant was the compatibility
eta-expansion of a primitive projections, but since a previous cleanup in
the kernel it had become useless.
|
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
We untangle the implementation in several ways.
- No higher-order self argument function as there is only one caller.
- Compute composition of lifts + substitution on terms using a dedicated
function instead of mk_clos followed by to_constr.
- Take more advantage of identity substitutions.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|_|_|/ /
|/| | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| |_|_|_|_|_|/ / / / / / / / /
|/| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
Rather than trying to keep the version of dependencies in sync with GitLab CI.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|_|_|_|/ / /
|/| | | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|_|_|_|/ / /
|/| | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
|
|/ / / / / / / / / / / / / |
|
| | | | | | | | | | | | | |
|
| | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|_|/ / /
|/| | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
This ensures that computations are shared as much as possible, mimicking
the "positive" records computational behavior if possible.
|
|\ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|/ / / / / /
|/| | | | | | | | | | | |
|
| |_|_|_|_|/ / / / / /
|/| | | | | | | | | | |
|
| |_|_|_|_|/ / / / /
|/| | | | | | | | | |
|
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Although the fix is not a proper one, it seems to solve
every instance of #2800 that could be tested.
|
|\ \ \ \ \ \ \ \ \ \
| |/ / / / / / / / /
|/| | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \
| |/ / / / / / / / / / /
|/| | | | | | | | | | |
| | | | | | | | | | | | |
of submodules.
|
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
to anomaly)
|
|\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
in unification
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
names" warnings
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| |_|_|_|_|_|/ / / / / / / / /
|/| | | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
Currently, if one of the inductives is non recursive, it defaults to a
case analysis schems taking fewer predicates and methods just for that
inductive. This irregularity prevents doing a combined scheme afterwards
to gather all eliminators into one, as combined scheme expects all the
eliminators to have the same predicates and methods. I have a use case
in building function graphs in Equations where some of the inductives
might not be recursive but I expect many other use cases could exist.
|
| |_|_|_|_|_|_|_|_|_|_|/ / / /
|/| | | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | | | | |
|
| |/ / / / / / / / / / / / / / /
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
[ci skip]
|
|/ / / / / / / / / / / / / / /
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
We had mostly used absolute links in the past.
I just discovered that GitHub recommends using relative links instead:
https://help.github.com/articles/basic-writing-and-formatting-syntax/#relative-links
and indeed my Emacs Markdown mode can handle relative links but doesn't
interpret absolute links relatively to the root of the git repository.
[ci skip]
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / /
|/| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
possibility of an "eqn" clause
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|_|/ / / / / / /
|/| | | | | | | | | | | | | | | | |
|
| |_|_|_|/ / / / / / / / / / / /
|/| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
Not all runners are equipped with docker services, thus we must add a
hard dependency on the `docker` tag for our Docker job.
|
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
This is a quick fix. Code should be made nicer along these lines:
- try to pass the name of the variable created by "mkletin_goal" in
the monad using "refine_one";
- use a disjunctive type of "inhyps" to indicate when it is
meaningful, rather than using [].
|
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
To be removed in 8.10.
|
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
We move the last 3 types to more adequate places.
|