| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Replacing ; with && and enabling bash's pipefail option
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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 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.
|
|
|
