diff options
| author | Emilio Jesus Gallego Arias | 2020-02-09 16:08:57 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-09 16:08:57 +0100 |
| commit | 1820f40590ec358b40e3a9c444f80c5283e55292 (patch) | |
| tree | 8ef176a84123972e1f51a14a3450152aa4091ff8 | |
| parent | d96e6bc44437de5c27ff26b6a75b92904e4e7887 (diff) | |
| parent | 67ad410e48608682f48c6bf8c27b2657a48f71ab (diff) | |
Merge PR #11551: Remove -compat 8.9.
Reviewed-by: JasonGross
Reviewed-by: ejgallego
| -rw-r--r-- | doc/stdlib/index-list.html.template | 1 | ||||
| -rw-r--r-- | test-suite/success/CompatOldOldFlag.v | 6 | ||||
| -rwxr-xr-x | test-suite/tools/update-compat/run.sh | 2 | ||||
| -rw-r--r-- | theories/Compat/Coq89.v | 19 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 3 |
5 files changed, 2 insertions, 29 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 5e13214a1a..b2ddf36b65 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -664,7 +664,6 @@ through the <tt>Require Import</tt> command.</p> </dt> <dd> theories/Compat/AdmitAxiom.v - theories/Compat/Coq89.v theories/Compat/Coq810.v theories/Compat/Coq811.v theories/Compat/Coq812.v diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v deleted file mode 100644 index dd259988ac..0000000000 --- a/test-suite/success/CompatOldOldFlag.v +++ /dev/null @@ -1,6 +0,0 @@ -(* -*- coq-prog-args: ("-compat" "8.9") -*- *) -(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *) -Import Coq.Compat.Coq812. -Import Coq.Compat.Coq811. -Import Coq.Compat.Coq810. -Import Coq.Compat.Coq89. diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh index 61273c4f37..7ff5571ffb 100755 --- a/test-suite/tools/update-compat/run.sh +++ b/test-suite/tools/update-compat/run.sh @@ -6,4 +6,4 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )" # we assume that the script lives in test-suite/tools/update-compat/, # and that update-compat.py lives in dev/tools/ cd "${SCRIPT_DIR}/../../.." -dev/tools/update-compat.py --assert-unchanged --master || exit $? +dev/tools/update-compat.py --assert-unchanged --release || exit $? diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v deleted file mode 100644 index 274cb4afd3..0000000000 --- a/theories/Compat/Coq89.v +++ /dev/null @@ -1,19 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Compatibility file for making Coq act similar to Coq v8.9 *) -Local Set Warnings "-deprecated". - -Require Export Coq.Compat.Coq810. - -Unset Private Polymorphic Universes. - -(** Unsafe flag, can hide inconsistencies. *) -Global Unset Template Check. diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 74d9c113d6..7d919956e8 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -271,8 +271,7 @@ let get_compat_file = function | "8.12" -> "Coq.Compat.Coq812" | "8.11" -> "Coq.Compat.Coq811" | "8.10" -> "Coq.Compat.Coq810" - | "8.9" -> "Coq.Compat.Coq89" - | ("8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> + | ("8.9" | "8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> CErrors.user_err ~hdr:"get_compat_file" Pp.(str "Compatibility with version " ++ str s ++ str " not supported.") | s -> |