| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
In unix one can concatenate a prefix with an absolute path in
order to obtain a valid path. This is not the case on Windows.
|
|
In particular, find it under $(COQBIN)
|
|
|
|
|
|
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 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).
|
|
|
|
|
