| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
The theories/ directory contains no cmi/cmxs files when native_compute is
disabled, so do not try to ship them.
|
| | |
|
| | |
|
| |
|
|
|
| |
Still unsure about .o file (should they be shipped for the native_compute
machinery or .cmxs suffice?)
|
| |
|
|
|
| |
The official Coq logo does not work as a splash screen.
Simplest fix: no splash screen.
|
| |
|
|
|
|
|
|
|
| |
- checks for paths containing whitespaces
- Coqide has syntax highlighting
- does not include the ocaml compiler, since it would not work anyway
for the purpose of native compile. For that we really need the whole
toolchain, including the C linker/assembler. Hence we should just
recommend to install the SDK
|
|
|
Not 100% functional, but coqide works.
The native compiler is embedded but:
- some path mangling problem prevents it from working even when run via
cygwin (like in the build process)
- CAMLLIB must be exported to ${COQ}\ocaml\lib to have it run
(coq should do it).
fix
|
Théo Zimmermann
Gaëtan Gilbert
Enrico Tassi
Maxime Dénès
Guillaume Melquiond