diff options
| -rw-r--r-- | doc/stdlib/index-list.html.template | 1 | ||||
| -rw-r--r-- | sysinit/coqargs.ml | 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/Coq818.v | 2 | ||||
| -rw-r--r-- | theories/Compat/Coq819.v | 11 | ||||
| -rw-r--r-- | tools/configure/configure.ml | 4 |
10 files changed, 30 insertions, 9 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 13a6951..7ab1265 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -716,6 +716,7 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/Coq816.v theories/Compat/Coq817.v theories/Compat/Coq818.v + theories/Compat/Coq819.v </dd> <dt> <b>Array</b>: diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index 94a4102..3f4e5f0 100644 --- a/sysinit/coqargs.ml +++ b/sysinit/coqargs.ml @@ -225,6 +225,7 @@ let set_option = let open Goptions in function | opt, OptionAppend v -> set_string_option_append_value_gen ~locality:OptLocal opt v let get_compat_file = function + | "8.19" -> "Coq.Compat.Coq819" | "8.18" -> "Coq.Compat.Coq818" | "8.17" -> "Coq.Compat.Coq817" | "8.16" -> "Coq.Compat.Coq816" diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v index 0466fd7..04ef2e7 100644 --- a/test-suite/success/CompatCurrentFlag.v +++ b/test-suite/success/CompatCurrentFlag.v @@ -1,3 +1,3 @@ -(* -*- coq-prog-args: ("-compat" "8.18") -*- *) +(* -*- coq-prog-args: ("-compat" "8.19") -*- *) (** Check that the current compatibility flag actually requires the relevant modules. *) -Import Coq.Compat.Coq818. +Import Coq.Compat.Coq819. diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v index a9bcc36..8511745 100644 --- a/test-suite/success/CompatOldFlag.v +++ b/test-suite/success/CompatOldFlag.v @@ -1,5 +1,5 @@ -(* -*- coq-prog-args: ("-compat" "8.16") -*- *) +(* -*- coq-prog-args: ("-compat" "8.17") -*- *) (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq819. Import Coq.Compat.Coq818. Import Coq.Compat.Coq817. -Import Coq.Compat.Coq816. diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v new file mode 100644 index 0000000..f3c2b46 --- /dev/null +++ b/test-suite/success/CompatOldOldFlag.v @@ -0,0 +1,6 @@ +(* -*- coq-prog-args: ("-compat" "8.16") -*- *) +(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq819. +Import Coq.Compat.Coq818. +Import Coq.Compat.Coq817. +Import Coq.Compat.Coq816. diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v index ea5470d..5ff8ded 100644 --- a/test-suite/success/CompatPreviousFlag.v +++ b/test-suite/success/CompatPreviousFlag.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-compat" "8.17") -*- *) +(* -*- coq-prog-args: ("-compat" "8.18") -*- *) (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq819. Import Coq.Compat.Coq818. -Import Coq.Compat.Coq817. diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh index 7ff5571..61273c4 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/Coq818.v b/theories/Compat/Coq818.v index 41d28e6..68edeb3 100644 --- a/theories/Compat/Coq818.v +++ b/theories/Compat/Coq818.v @@ -9,3 +9,5 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.18 *) + +Require Export Coq.Compat.Coq819. diff --git a/theories/Compat/Coq819.v b/theories/Compat/Coq819.v new file mode 100644 index 0000000..5ab9dc6 --- /dev/null +++ b/theories/Compat/Coq819.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.19 *) diff --git a/tools/configure/configure.ml b/tools/configure/configure.ml index 60bfcab..66bb3f1 100644 --- a/tools/configure/configure.ml +++ b/tools/configure/configure.ml @@ -22,8 +22,8 @@ open CmdArgs.Prefs let (/) = Filename.concat -let coq_version = "8.18+alpha" -let vo_magic = 81799 +let coq_version = "8.19+alpha" +let vo_magic = 81899 let is_a_released_version = false (** Default OCaml binaries *) |