| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
symlink from repo
|
|
This was introduced between v8.5 and v8.6 (presumably 63f3ca8).
|
|
Fixes #7065
|
|
only-printing declarations.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
OpenBSD mktemp fails with an error otherwise.
|
|
|
