diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-13 16:25:49 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-13 16:25:49 +0100 |
| commit | 8e7de2a327b202130192a784f921699f70e707cb (patch) | |
| tree | 1a9460251285bb124898a0c1c29c5531fc9017f6 | |
| parent | e0aab135237aaa9334afe9acc9b519bbe2b53ae9 (diff) | |
| download | compcert-kvx-8e7de2a327b202130192a784f921699f70e707cb.tar.gz compcert-kvx-8e7de2a327b202130192a784f921699f70e707cb.zip | |
Turn warning "deprecated-implicit-arguments" off while compiling Flocq
Perhaps for reasons of backward compatibility with Coq 8.4, Flocq 2.5.2 still uses the "Implicit Arguments foo" idiom, which is deprecated in Coq 8.6.
| -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 |