diff options
| -rw-r--r-- | doc/stdlib/index-list.html.template | 1 | ||||
| -rw-r--r-- | test-suite/success/CompatCurrentFlag.v | 4 | ||||
| -rw-r--r-- | test-suite/success/CompatOldFlag.v | 4 | ||||
| -rw-r--r-- | test-suite/success/CompatOldOldFlag.v | 6 | ||||
| -rw-r--r-- | test-suite/success/CompatPreviousFlag.v | 4 | ||||
| -rwxr-xr-x | test-suite/tools/update-compat/run.sh | 2 | ||||
| -rw-r--r-- | theories/Compat/Coq813.v | 2 | ||||
| -rw-r--r-- | theories/Compat/Coq814.v | 11 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 1 |
9 files changed, 28 insertions, 7 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 7201dc6a0e..8ab4265b15 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -709,6 +709,7 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/Coq811.v theories/Compat/Coq812.v theories/Compat/Coq813.v + theories/Compat/Coq814.v </dd> <dt> <b>Array</b>: diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v index 97b4e39168..f1dad301fd 100644 --- a/test-suite/success/CompatCurrentFlag.v +++ b/test-suite/success/CompatCurrentFlag.v @@ -1,3 +1,3 @@ -(* -*- coq-prog-args: ("-compat" "8.13") -*- *) +(* -*- coq-prog-args: ("-compat" "8.14") -*- *) (** Check that the current compatibility flag actually requires the relevant modules. *) -Import Coq.Compat.Coq813. +Import Coq.Compat.Coq814. diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v index c06dd6e450..a737e0c98e 100644 --- a/test-suite/success/CompatOldFlag.v +++ b/test-suite/success/CompatOldFlag.v @@ -1,5 +1,5 @@ -(* -*- coq-prog-args: ("-compat" "8.11") -*- *) +(* -*- coq-prog-args: ("-compat" "8.12") -*- *) (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq814. Import Coq.Compat.Coq813. Import Coq.Compat.Coq812. -Import Coq.Compat.Coq811. diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v new file mode 100644 index 0000000000..f4cf703ec7 --- /dev/null +++ b/test-suite/success/CompatOldOldFlag.v @@ -0,0 +1,6 @@ +(* -*- coq-prog-args: ("-compat" "8.11") -*- *) +(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq814. +Import Coq.Compat.Coq813. +Import Coq.Compat.Coq812. +Import Coq.Compat.Coq811. diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v index 83010f2149..07d5fcd3ab 100644 --- a/test-suite/success/CompatPreviousFlag.v +++ b/test-suite/success/CompatPreviousFlag.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-compat" "8.12") -*- *) +(* -*- coq-prog-args: ("-compat" "8.13") -*- *) (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq814. Import Coq.Compat.Coq813. -Import Coq.Compat.Coq812. diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh index 7ff5571ffb..61273c4f37 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 --release || exit $? +dev/tools/update-compat.py --assert-unchanged --master || exit $? diff --git a/theories/Compat/Coq813.v b/theories/Compat/Coq813.v index 92544c6ed9..fe7431dcd3 100644 --- a/theories/Compat/Coq813.v +++ b/theories/Compat/Coq813.v @@ -9,3 +9,5 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.13 *) + +Require Export Coq.Compat.Coq814. diff --git a/theories/Compat/Coq814.v b/theories/Compat/Coq814.v new file mode 100644 index 0000000000..94948dd280 --- /dev/null +++ b/theories/Compat/Coq814.v @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \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.14 *) diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index ec339c69c6..fbf3b4873b 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -261,6 +261,7 @@ let get_native_name s = with _ -> "" let get_compat_file = function + | "8.14" -> "Coq.Compat.Coq814" | "8.13" -> "Coq.Compat.Coq813" | "8.12" -> "Coq.Compat.Coq812" | "8.11" -> "Coq.Compat.Coq811" |