From cc3f0838d115830b2f2fba55ff8c53c212db6979 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 26 Sep 2021 17:35:58 +0200 Subject: Selectively turn some Coq 8.14 warnings off Warning "deprecated hint rewrite without locality" cannot be addressed: the suggested fix (qualify with Global or Local or [#export]) is not supported by Coq 8.11 to 8.13 ! Warning "deprecated instance without locality" is turned off for generated file cparser/Parser.v only. Menhir needs to be changed so as to generate the `Global` modifier that would silence this warning. --- Makefile | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 4a9f3772..2bc39c33 100644 --- a/Makefile +++ b/Makefile @@ -53,11 +53,21 @@ endif # deprecated-ident-entry: # warning introduced in 8.13 # suggested change (use `name` instead of `ident`) supported since 8.13 +# deprecated-hint-rewrite-without-locality: +# warning introduced in 8.14 +# suggested change (add Global or Local or [#export] modifier) +# is not supported in 8.13 nor in 8.11, but was supported in 8.9 (go figure) +# deprecated-instance-without-locality: +# warning introduced in 8.14 +# triggered by Menhir-generated files, to be solved upstream in Menhir COQCOPTS ?= \ -w -undeclared-scope \ -w -unused-pattern-matching-variable \ - -w -deprecated-ident-entry + -w -deprecated-ident-entry \ + -w -deprecated-hint-rewrite-without-locality + +cparser/Parser.vo: COQCOPTS += -w -deprecated-instance-without-locality COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS) COQDEP="$(COQBIN)coqdep" $(COQINCLUDES) -- cgit