| Age | Commit message (Collapse) | Author |
|---|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
Add headers to a few files which were missing them.
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
Instead of relying on the Coq_config immutable flag, we introduce an
initialization-only flag to govern the use of the native compiler. This
allows to make coqc passed with "-native-compiler no" behave as if it had
been configured without native compilation.
|
|
|
|
|
|
One other call still remains, but will require to refactor some
section-handling code.
|
|
These modules do actually belong there.
We have to slightly reorganize printers, removing a couple of
duplicated ones in the way.
|
