diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 5 |
1 files changed, 4 insertions, 1 deletions
@@ -29,7 +29,7 @@ RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight cpars COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) compcert.$(d)) -COQC="$(COQBIN)coqc" -q $(COQINCLUDES) +COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS) COQDEP="$(COQBIN)coqdep" $(COQINCLUDES) COQDOC="$(COQBIN)coqdoc" COQEXEC="$(COQBIN)coqtop" $(COQINCLUDES) -batch -load-vernac-source @@ -147,6 +147,9 @@ endif proof: $(FILES:.v=.vo) +# Turn off some warnings for compiling Flocq +flocq/%.vo: COQCOPTS+=-w -deprecated-implicit-arguments + extraction: extraction/STAMP extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v $(ARCH)/extractionMachdep.v |