From 8e7de2a327b202130192a784f921699f70e707cb Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Mon, 13 Feb 2017 16:25:49 +0100
Subject: 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.
---
 Makefile | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 24953280..7bb2650d 100644
--- a/Makefile
+++ b/Makefile
@@ -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
-- 
cgit