| Commit message (Collapse) | Author | Age |
|\ |
|
| |
| |
| |
| |
| | |
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
|
|\ \ \ \ \ |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
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]
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
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 [].
|
| |/ / / /
|/| | | | |
|
| | | | | |
|
|/ / / /
| | | |
| | | |
| | | |
| | | | |
Redundancy between finding section variables in both interp_var and
interp_qualid could probably be cleaned.
|
| | | | |
|
| |_|/
|/| |
| | |
| | |
| | |
| | |
| | | |
We store the universe context in the inlined terms and apply it to
the instance provided to the substitution function. Technically the
context is not needed, but we use it to assert that the length of the
instance corresponds, just in case.
|
|\ \ \
| | | |
| | | |
| | | | |
vm_compute and native_compute (partial fix to #7068; also fixes #7076))
|
|\ \ \ \ |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Dependency analysis for separate compilation was not iterated properly
on rel_context and named_context.
|
|\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
"rename" flag
|
| |_|/ / /
|/| | | | |
|
|\ \ \ \ \ |
|
| | | | | | |
|
|\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
pattern-matching names
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
tactic unification.
|
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
coinductive types.
|
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
| |_|_|_|_|_|_|/ / / / /
|/| | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|/ / /
|/| | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | |
|
| |_|_|_|_|_|/ / / / / /
|/| | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
When creating a scheme for bifinite inductive types, we do not create a
fixpoint.
|
| | | | | | | | | | | | |
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
The file `config/Makefile` doesn't exist unless we run `./configure`.
We shouldn't have to run `./configure` to run `make clean`. We now no
longer error in any case if `config/Makefile` doesn't exist; this is
simpler than only not erroring if the target is `clean`.
We also now test this property when building on CI.
This fixes #7542
|
| |_|_|_|_|_|_|_|/ / /
|/| | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
Using a formulation which makes it is clear that no renaming has been
done. See discussion at issue #2987.
|
| | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
instances
|
| |_|_|_|/ / / / / / / /
|/| | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
The old unification engine was using the unfiltered environment when a
context had been cleared, leading to an ill-typed goal.
|
|\ \ \ \ \ \ \ \ \ \ \ \
| |_|_|/ / / / / / / / /
|/| | | | | | | | | | | |
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
Failed in v8.7.2 but were fixed by v8.8.0.
|
| |_|_|_|/ / / / / / /
|/| | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
The reduction machine of the checker was not taking into account the fact
that cofixpoints needed to be unfolded when applied against a projection.
|
|/ / / / / / / / / / |
|
|\ \ \ \ \ \ \ \ \ \
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
by default.
|
| | | | | | | | | | | |
|
| | | | | | | | | | | |
|
| | | | | | | | | | | |
|
|/ / / / / / / / / / |
|
|\ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | |
|