| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
| |
The GPL makes sense for whole applications, but the dual-licensed Coq
and OCaml files are more like libraries to be combined with other
code, so the LGPL is more appropriate.
|
|
|
|
|
|
|
|
|
|
|
| |
Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal.
Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`,
and `xomegaContradiction` with `lia` and `extlia`.
Turn back on the deprecation warning for uses of `omega`.
Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
|
|
|
|
|
|
|
|
|
| |
IEEE754_extra: clear unused context so that none of the context is
picked up by tactics and ends as extra parameters to theorems
int_round_odd_bits and int_round_odd_le
Floats: simplify uses of int_round_odd_bits and int_round_odd_le
accordingly.
|
|
|
|
| |
configure flags -use-external-Flocq and -use external-MenhirLib.
|
|
To match the new module names from version 3 of Flocq.
Plus, it's shorter.
|