From 25483cf1acce8695a438f4f2164b09fb1ecd9d2e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 21 Jan 2021 16:54:40 +0100 Subject: Silence some new warnings of Coq 8.13 Either because the code change that would silence the warning is not desirable, or because it would break compatibility with earlier versions of Coq. Explain the silenced warnings as comments in the Makefile. --- Makefile | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 971b1394..d0b0029a 100644 --- a/Makefile +++ b/Makefile @@ -41,7 +41,23 @@ DIRS += MenhirLib COQINCLUDES += -R MenhirLib MenhirLib endif -COQCOPTS ?= -w -undeclared-scope +# Notes on silenced Coq warnings: +# +# undeclared-scope: +# warning introduced in 8.12 +# suggested change (use `Declare Scope`) supported since 8.12 +# unused-pattern-matching-variable: +# warning introduced in 8.13 +# the code rewrite that avoids the warning is not desirable +# deprecated-ident-entry: +# warning introduced in 8.13 +# suggested change (use `name` instead of `ident`) supported since 8.13 + +COQCOPTS ?= \ + -w -undeclared-scope \ + -w -unused-pattern-matching-variable \ + -w -deprecated-ident-entry + COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS) COQDEP="$(COQBIN)coqdep" $(COQINCLUDES) COQDOC="$(COQBIN)coqdoc" -- cgit