| Commit message (Collapse) | Author | Age |
|
|
|
| |
Move credits to its own chapter (closes #6573).
|
| |
|
|\ |
|
|\ \ |
|
|\ \ \ |
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
| | | | | | | |
|
|/ / / / / / |
|
|\ \ \ \ \ \ |
|
| |_|_|_|_|/
|/| | | | | |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
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
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
| |_|_|_|_|_|/ / / / /
|/| | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | |
|
| |/ / / / / / / / / / / /
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
[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.
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
|
| |/ / / / / / / / / / / /
|/| | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \
| |_|/ / / / / / / / / / /
|/| | | | | | | | | | | | |
|
| |_|_|_|_|/ / / / / / /
|/| | | | | | | | | | | |
|
| |/ / / / / / / / / /
|/| | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
The renaming is internal only. I believe the name reloc is legacy and
a bit confusing now that the structure contains a full compilation
environment.
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
not found
|
|\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
to cmx.
|