| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-02-06 | Makefiles: Fixes for byte compilation | Gaëtan Gilbert | |
| - default targets don't depend on ocamlopt when it's unavailable - coqc.byte is built by byte target and coqc by coqbinaries target - unit tests use best ocaml - poly-capture-global-univs tests ml compilation with ocamlc - don't try to install .cmx and native-compute .o files cf https://github.com/coq/coq/issues/9464 | |||
| 2019-01-10 | [make] support for QUICK | Enrico Tassi | |
| The variable QUICK enables the quick compilation chain: - all v files are compiled with -quick to vio files (also -native-compiler no, since it is quicker) - then all vio files are turned to vo files $NJOBS at a time All occurrences of .vo use now .$(VO) that can be either .vo or .vio depending of QUICK being defined. Targets that only make sense for .vo files have to use $(VAR:.$(VO)=.vo) | |||
| 2018-05-30 | Makefile: fix undefined NATIVEFILES when -native-compute no | Gaëtan Gilbert | |
| 2018-05-23 | Don't try to install native compiled files if native-compile is not set | Jim Fehrle | |
| 2018-05-16 | Modify make system to include Makefile.common in the test suite | Gaëtan Gilbert | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/Makefile.vofiles