| Commit message (Collapse) | Author | Age |
... | |
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| |_|_|_|_|_|/ / / / / / / /
|/| | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
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.
|
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
We move the "flag types" to its use place, and mark some arguments
with named parameters better.
|
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
This gets `Tactypes` closer to `tactics/`, however some legacy stuff
blocks it in `proofs`. We consider that is satisfactory for now.
|
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
| | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | |
|
| |/ / / / / / / / / / / / /
|/| | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|/ / / / / / / / / / / /
|/| | | | | | | | | | | | | |
|
| |_|_|_|_|/ / / / / / / /
|/| | | | | | | | | | | | |
|