diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-01-07 17:47:55 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-01-07 17:47:55 +0100 |
| commit | 728888d8a3f70afd526f6c4454327f52ea4c4746 (patch) | |
| tree | c0e57b9ec1de6c5580bdf296d85a3024af738537 /Makefile | |
| parent | ac8b7ae094cf7741fec63effd8fcfd1467fb2edf (diff) | |
| download | compcert-kvx-728888d8a3f70afd526f6c4454327f52ea4c4746.tar.gz compcert-kvx-728888d8a3f70afd526f6c4454327f52ea4c4746.zip | |
Val_cmp* -> Val.mxcmp*
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 10 |
1 files changed, 7 insertions, 3 deletions
@@ -274,10 +274,14 @@ latexdoc: @tools/ndfun $*.vp > $*.v || { rm -f $*.v; exit 2; } @chmod a-w $*.v +# this trick aims to allow extraction to depend on the target processor +# (currently: export extra Coq-functions for OCaml code, depending on the target) extraction/extraction.v: Makefile extraction/extraction.vexpand - cat extraction/extraction.vexpand > extraction/extraction.v - echo "$(EXTRA_EXTRACTION)" >> extraction/extraction.v - echo "." >> extraction/extraction.v + (echo "(* WARNING: this file is generated from extraction.vexpand *)"; \ + echo "(* by the Makefile -- target \"extraction/extraction.v\" *)\n"; \ + cat extraction/extraction.vexpand; \ + echo "$(EXTRA_EXTRACTION)"; \ + echo ".") > extraction/extraction.v driver/Compiler.v: driver/Compiler.vexpand tools/compiler_expand tools/compiler_expand driver/Compiler.vexpand $@ |