aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2022-06-25 10:27:28 +0200
committerXavier Leroy <xavier.leroy@college-de-france.fr>2022-06-25 10:27:28 +0200
commit971c8ea8397b74aabfe0245d3f1c0645f3f77554 (patch)
tree68fedba5ce9838ad616fdc80812d1a214ce3307b
parent11938ee7ee136cfdb7d6e5f7c2b4956dc320807a (diff)
downloadcompcert-971c8ea8397b74aabfe0245d3f1c0645f3f77554.tar.gz
compcert-971c8ea8397b74aabfe0245d3f1c0645f3f77554.zip
Support Coq 8.15.2
-rw-r--r--Changelog2
-rwxr-xr-xconfigure4
2 files changed, 3 insertions, 3 deletions
diff --git a/Changelog b/Changelog
index f0cc7ac9..7690630b 100644
--- a/Changelog
+++ b/Changelog
@@ -34,7 +34,7 @@ Bug fixes:
Coq development:
- Updated the Flocq library to version 4.1.
-- Support for Coq 8.14.1, 8.15.0, 8.15.1.
+- Support for Coq 8.14.1, 8.15.0, 8.15.1, 8.15.2.
- Minimal Coq version supported is now 8.12.0.
diff --git a/configure b/configure
index 424bba6e..f199e046 100755
--- a/configure
+++ b/configure
@@ -504,14 +504,14 @@ missingtools=false
echo "Testing Coq... " | tr -d '\n'
coq_ver=$(${COQBIN}coqc -v 2>/dev/null | tr -d '\r' | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p')
case "$coq_ver" in
- 8.12.0|8.12.1|8.12.2|8.13.0|8.13.1|8.13.2|8.14.0|8.14.1|8.15.0|8.15.1)
+ 8.12.0|8.12.1|8.12.2|8.13.0|8.13.1|8.13.2|8.14.0|8.14.1|8.15.0|8.15.1|8.15.2)
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 a version of Coq between 8.12.0 and 8.15.1"
+ echo "Error: CompCert requires a version of Coq between 8.12.0 and 8.15.2"
missingtools=true
fi;;
"")