| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
| |
Currently, if one of the inductives is non recursive, it defaults to a
case analysis schems taking fewer predicates and methods just for that
inductive. This irregularity prevents doing a combined scheme afterwards
to gather all eliminators into one, as combined scheme expects all the
eliminators to have the same predicates and methods. I have a use case
in building function graphs in Equations where some of the inductives
might not be recursive but I expect many other use cases could exist.
|
|\ |
|
|\ \ |
|
| | |
| | |
| | |
| | | |
To be removed in 8.10.
|
| | |
| | |
| | |
| | | |
We move the last 3 types to more adequate places.
|
| | |
| | |
| | |
| | |
| | | |
We move the "flag types" to its use place, and mark some arguments
with named parameters better.
|
| | |
| | |
| | |
| | |
| | | |
This gets `Tactypes` closer to `tactics/`, however some legacy stuff
blocks it in `proofs`. We consider that is satisfactory for now.
|
| | |
| | |
| | |
| | |
| | | |
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
| | | |
|
| | | |
|
| | | |
|
| |/
|/| |
|
|\ \ |
|
| |/
|/|
| |
| |
| |
| | |
The renaming is internal only. I believe the name reloc is legacy and
a bit confusing now that the structure contains a full compilation
environment.
|
|\ \ |
|
|\ \ \
| | | |
| | | |
| | | | |
not found
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
to cmx.
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
| |_|_|_|_|/
|/| | | | | |
|
|\ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ |
|
| |/ / / / / /
|/| | | | | | |
|
| |_|_|_|_|/
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
It was actually a hack since those names are never used to represent
values, only to be passed as arguments to bytecode instructions. So
instead of reusing the structured_constant type, we follow the same
pattern as switch annotations.
|
| |_|_|_|/
|/| | | |
| | | | |
| | | | |
| | | | | |
Redundancy between finding section variables in both interp_var and
interp_qualid could probably be cleaned.
|
| |/ / /
|/| | | |
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
| | | | | | | |
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
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
|
|\ \ \ \ \ \ \ \ \ \ |
|