aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2020-02-05 18:33:13 +0100
committerGitHub <noreply@github.com>2020-02-05 18:33:13 +0100
commitb0fdbb0e88d6decd068709ea673dbe51fd6727b0 (patch)
tree1e49fbdcd5eb05b4fd2da01c378ca440fb5df86c
parent3e5fba812749b9240b655a99809e62231d1145aa (diff)
downloadcompcert-kvx-b0fdbb0e88d6decd068709ea673dbe51fd6727b0.tar.gz
compcert-kvx-b0fdbb0e88d6decd068709ea673dbe51fd6727b0.zip
Support Coq 8.11.0 (#212)
Update configure. Ignore and clean up .vok and .vos files, which Coq 8.11.0 generates.
-rw-r--r--.gitignore2
-rw-r--r--Changelog4
-rw-r--r--Makefile2
-rwxr-xr-xconfigure2
4 files changed, 8 insertions, 2 deletions
diff --git a/.gitignore b/.gitignore
index 4b497387..da883cff 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,7 @@
# Object files, in general
*.vo
+*.vok
+*.vos
*.glob
*.o
*.a
diff --git a/Changelog b/Changelog
index 935f77f2..08586da5 100644
--- a/Changelog
+++ b/Changelog
@@ -1,3 +1,7 @@
+Coq development:
+- Compatibility with Coq version 8.11.0 (#316)
+
+
Release 3.6, 2019-09-17
=======================
diff --git a/Makefile b/Makefile
index 80eca80d..af069e3f 100644
--- a/Makefile
+++ b/Makefile
@@ -258,7 +258,7 @@ endif
clean:
- rm -f $(patsubst %, %/*.vo, $(DIRS))
+ rm -f $(patsubst %, %/*.vo*, $(DIRS))
rm -f $(patsubst %, %/.*.aux, $(DIRS))
rm -rf doc/html doc/*.glob
rm -f driver/Version.ml
diff --git a/configure b/configure
index b964c124..d91bfebf 100755
--- a/configure
+++ b/configure
@@ -530,7 +530,7 @@ 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.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)
echo "version $coq_ver -- good!";;
?*)
echo "version $coq_ver -- UNSUPPORTED"