| Commit message (Collapse) | Author | Age |
|\ |
|
|\ \ |
|
|\ \ \ |
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
persistent states.
|
| | | | | |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \
| |_|_|_|/ / / /
|/| | | | | | | |
|
|\ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
8.5.
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
| |_|_|_|_|_|_|_|_|/ /
|/| | | | | | | | | | |
|
| |_|_|_|_|_|_|_|/ /
|/| | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`,
`Miscprint`) to their proper place as they were declared in different
`mllib` files than the one in their directory.
In some cases this could be refined but we don't do anything fancy, we
just reflect the status quo.
|
|\ \ \ \ \ \ \ \ \ \ |
|
| |_|_|_|_|_|_|_|/ /
|/| | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Fix bug introduced by a Haskell programmer.
|
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
It seems we were not testing the checker on cumulative inductive types,
because judging from the code, it would just have exploded in anomalies.
Before this patch, the checker was mixing De Bruijn indices with named
variables, resulting in ill-formed universe contexts used throughout the
checking of cumulative inductive types.
This patch also gets rid of a lot of now dead code, and removes abstraction
breaking code from the checker.
|
|\ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|/ /
|/| | | | | | | | | |
|
| |_|_|_|_|_|_|_|/
|/| | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
It used to compute the dependencies of all undefined evars of the
evar_map, while only the dependencies of resolvable evars are necessary.
|
|/ / / / / / / / |
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
It breaks ocamlmerlin.
|
| | | | | | | | | | | |
|
| |_|_|/ / / / / / /
|/| | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
moved to Global).
|
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
rather than colors
|
| | | | | | | | | | | | |\ \ \ \ \ |
|
| |_|_|_|_|/ / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | |
|
| |_|_|_|/ / / / / / / / / / / /
|/| | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
This is probably the hardest case of them all, because tclABSTRACT fundamentally
relies on the names of universes from the constant instance being the same as
the one in the current goal. Adding to that the fact that the kernel is doing
strange things when provided with a polymorphic definition with body universe
constraints, it turns out to be a hellish nightmare to handle properly.
At some point we need to clarifiy this in the kernel as well, although we
leave it for some other patch.
|
| |_|_|_|_|_|_|_|_|_|_|_|_|/ /
|/| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
We only delay monomorphic proofs in quick mode, so that their universe context
will always be empty.
|
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
I had to slightly tweak a test in order to work around a bug of simpl that
loses universes constraints when refolding polymorphic fixpoints.
|
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
It is a valid git tag (unlike 8.7~alpha) and will be considered by most
tools as < 8.7.0 (unlike 8.7.0+alpha).
|
| | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | |
|