diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-08-05 16:01:46 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-08-07 10:37:28 +0200 |
| commit | f19b7fd7a0b87d7fcce021a264f9b95c43a24a09 (patch) | |
| tree | fd5744aa607522fd096038c41e016d2fe5e89a29 | |
| parent | efb5f52493345a1e17cc10b56023dfe00beb6074 (diff) | |
| download | compcert-f19b7fd7a0b87d7fcce021a264f9b95c43a24a09.tar.gz compcert-f19b7fd7a0b87d7fcce021a264f9b95c43a24a09.zip | |
Coq 8.10 compatibility: (temporarily) silence new warning
The "undeclared-scope" warning fires when we use a "notation" scope
before having declared it. This is a good thing, except that
the "Declare Scope" vernacular that declares a scope was introduced
in Coq 8.10 and is not available in earlier versions.
Hence there is no way to avoid triggering the warning yet remain
compatible with pre-8.10 Coq versions.
This commit silences the warning. It will have to revisited when
Coq 8.10 is the oldest version of Coq we support in CompCert.
| -rw-r--r-- | Makefile | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -30,6 +30,7 @@ RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight \ COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) compcert.$(d)) +COQCOPTS ?= -w -undeclared-scope COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS) COQDEP="$(COQBIN)coqdep" $(COQINCLUDES) COQDOC="$(COQBIN)coqdoc" |