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 /Makefile | |
| parent | e0aab135237aaa9334afe9acc9b519bbe2b53ae9 (diff) | |
| download | compcert-8e7de2a327b202130192a784f921699f70e707cb.tar.gz compcert-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.
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 |