| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
info
|
|
|
|
|
|
|
|
|
|
We add .mli files, removed dead code and use standard combinators
instead of redefined ad-hoc ones in a few places.
A lot of cleaning still has to be done on this code: documenting the
interfaces, resolving the many abstraction leaks. I suspect there is
still a lot of code duplication.
|
|
|
|
GitLab CI.
|
|
This fixes #7734.
|
|
|
|
|
|
|
|
|
|
Packages such as `menhir` or `elpi` are fragile w.r.t. updates, so
allowing a non-deterministic install in the Dockefile seems risky. We
have found trouble with Menhir in the past. We thus specify a concrete
version for all `CI_OPAM` packages.
cc: https://github.com/AbsInt/CompCert/issues/234
We also add remove `hevea` from `apt` dependencies as it hasn't been
needed since #7466 and add `texlive-science` which is needed to build
the `source-doc` target due to the `textgreek` package being used.
|
|
|
|
|
|
https://github.com/AbsInt/CompCert/issues/234
|
|
|
|
|
|
vm_compute and native_compute (partial fix to #7068; also fixes #7076))
|
|
|
|
|
|
|
|
Actually all the new_ functions are in evarutil still
|
|
|
|
|
|
Many still remain.
|
|
|
|
|
|
|
|
|
|
|
|
Instead of having a constant-based compilation of projections, we
generate them at the compilation time of the inductive block to which
they pertain.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
