aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--Makefile2
-rwxr-xr-xconfigure6
2 files changed, 4 insertions, 4 deletions
diff --git a/Makefile b/Makefile
index df5fb03f..d91c5f37 100644
--- a/Makefile
+++ b/Makefile
@@ -35,7 +35,7 @@ RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight \
COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) compcert.$(d))
-COQCOPTS ?= -w -undeclared-scope
+COQCOPTS ?= -w -undeclared-scope -w -omega-is-deprecated
COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS)
COQDEP="$(COQBIN)coqdep" $(COQINCLUDES)
COQDOC="$(COQBIN)coqdoc"
diff --git a/configure b/configure
index d5264654..b358f3cb 100755
--- a/configure
+++ b/configure
@@ -530,19 +530,19 @@ missingtools=false
echo "Testing Coq... " | tr -d '\n'
coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p')
case "$coq_ver" in
- 8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2)
+ 8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0)
echo "version $coq_ver -- good!";;
?*)
echo "version $coq_ver -- UNSUPPORTED"
if $ignore_coq_version; then
echo "Warning: this version of Coq is unsupported, proceed at your own risks."
else
- echo "Error: CompCert requires one of the following Coq versions: 8.11.1, 8.11.0, 8.10.2, 8.10.1, 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0"
+ echo "Error: CompCert requires a version of Coq between 8.8.0 and 8.12.0"
missingtools=true
fi;;
"")
echo "NOT FOUND"
- echo "Error: make sure Coq version 8.9.1 is installed."
+ echo "Error: make sure Coq version 8.11.2 is installed."
missingtools=true;;
esac