diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-10-29 21:56:59 +0200 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-10-29 21:56:59 +0200 |
| commit | ae2d228c04f4fca1e281b146764646cbdd7d6b1d (patch) | |
| tree | 244f88aebc77a9ca2ef7e69731deb1dfee434ece /Makefile | |
| parent | e19d179d1f30d5893e5f30dbd33188350656831e (diff) | |
| parent | d194e47a7d494944385ff61c194693f8a67787cb (diff) | |
| download | compcert-kvx-ae2d228c04f4fca1e281b146764646cbdd7d6b1d.tar.gz compcert-kvx-ae2d228c04f4fca1e281b146764646cbdd7d6b1d.zip | |
Merge remote-tracking branch 'origin/master' into towards_3.10
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 12 |
1 files changed, 11 insertions, 1 deletions
@@ -61,11 +61,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) |