From 4136f69ea08425cff59c463b10a5db73b3dfc59a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 5 Aug 2019 16:01:46 +0200 Subject: Coq 8.10 compatibility: (temporarily) silence new warning The "undeclared-scope" warning fires when we use a "notation" scope before having declared it. This is a good thing, except that the "Declare Scope" vernacular that declares a scope was introduced in Coq 8.10 and is not available in earlier versions. Hence there is no way to avoid triggering the warning yet remain compatible with pre-8.10 Coq versions. This commit silences the warning. It will have to revisited when Coq 8.10 is the oldest version of Coq we support in CompCert. --- Makefile | 1 + 1 file changed, 1 insertion(+) (limited to 'Makefile') diff --git a/Makefile b/Makefile index ae19225a..80eca80d 100644 --- a/Makefile +++ b/Makefile @@ -30,6 +30,7 @@ RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight \ COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) compcert.$(d)) +COQCOPTS ?= -w -undeclared-scope COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS) COQDEP="$(COQBIN)coqdep" $(COQINCLUDES) COQDOC="$(COQBIN)coqdoc" -- cgit