diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-01-21 16:54:40 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-01-21 17:17:34 +0100 |
| commit | 25483cf1acce8695a438f4f2164b09fb1ecd9d2e (patch) | |
| tree | d7c96d261975a0b4bc5bbce4209a9e1e19b13e2f /Makefile | |
| parent | fc82b6c80fd3feeb4ef9478e6faa16b5b1104593 (diff) | |
| download | compcert-kvx-25483cf1acce8695a438f4f2164b09fb1ecd9d2e.tar.gz compcert-kvx-25483cf1acce8695a438f4f2164b09fb1ecd9d2e.zip | |
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.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 18 |
1 files changed, 17 insertions, 1 deletions
@@ -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" |