diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-09-26 17:35:58 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-10-03 18:43:34 +0200 |
| commit | cc3f0838d115830b2f2fba55ff8c53c212db6979 (patch) | |
| tree | 519b9d1631f2d65ce50db239e28583ae2ac801dd /Makefile | |
| parent | 2c46ae4bd8f9f49554daa31988fd98793cc5601e (diff) | |
| download | compcert-kvx-cc3f0838d115830b2f2fba55ff8c53c212db6979.tar.gz compcert-kvx-cc3f0838d115830b2f2fba55ff8c53c212db6979.zip | |
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.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 12 |
1 files changed, 11 insertions, 1 deletions
@@ -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) |