| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
| |
And re-enable the `undeclared-scope` warning.
`Declare Scope` has been available since Coq 8.12, which is now the minimal Coq version supported.
|
| |
|
|
|
|
|
|
|
| |
As proposed in #404.
This is presented as a new option `-clight` to the existing `clightgen` tool.
Revise clightgen testing to test the Csyntax output in addition to
the Clight output.
|
|
|
Split reusable parts of ExportClight.ml off, into
ExportBase.ml and ExportCtypes.ml.
Rename exportclight/ directory to export/
|
