Skip to content

Commit a303446

Browse files
committed
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.
1 parent 4e053c7 commit a303446

1 file changed

Lines changed: 11 additions & 1 deletion

File tree

Makefile

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -53,11 +53,21 @@ endif
5353
# deprecated-ident-entry:
5454
# warning introduced in 8.13
5555
# suggested change (use `name` instead of `ident`) supported since 8.13
56+
# deprecated-hint-rewrite-without-locality:
57+
# warning introduced in 8.14
58+
# suggested change (add Global or Local or [#export] modifier)
59+
# is not supported in 8.13 nor in 8.11, but was supported in 8.9 (go figure)
60+
# deprecated-instance-without-locality:
61+
# warning introduced in 8.14
62+
# triggered by Menhir-generated files, to be solved upstream in Menhir
5663

5764
COQCOPTS ?= \
5865
-w -undeclared-scope \
5966
-w -unused-pattern-matching-variable \
60-
-w -deprecated-ident-entry
67+
-w -deprecated-ident-entry \
68+
-w -deprecated-hint-rewrite-without-locality
69+
70+
cparser/Parser.vo: COQCOPTS += -w -deprecated-instance-without-locality
6171

6272
COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS)
6373
COQDEP="$(COQBIN)coqdep" $(COQINCLUDES)

0 commit comments

Comments
 (0)