Skip to content

Commit

Permalink
Selectively turn some Coq 8.14 warnings off
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
xavierleroy committed Sep 27, 2021
1 parent 4e053c7 commit a303446
Showing 1 changed file with 11 additions and 1 deletion.
12 changes: 11 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down

0 comments on commit a303446

Please sign in to comment.