Merge PR coq#18319: Bump version (8.20+alpha)

Reviewed-by: ppedrot Co-authored-by: ppedrot <[email protected]>
SkySkimmer · Dec 4, 2023 · ababbf4 · ababbf4
2 parents 89a5cee + 1d38647
commit ababbf4
Show file tree

Hide file tree

Showing 10 changed files with 30 additions and 9 deletions.
diff --git 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/Coq817.v
     theories/Compat/Coq818.v
     theories/Compat/Coq819.v
+    theories/Compat/Coq820.v
   </dd>
 
   <dt> <b>Array</b>:

diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
@@ -227,6 +227,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.20" -> "Coq.Compat.Coq820"
   | "8.19" -> "Coq.Compat.Coq819"
   | "8.18" -> "Coq.Compat.Coq818"
   | "8.17" -> "Coq.Compat.Coq817"

diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v
@@ -1,3 +1,3 @@
-(* -*- coq-prog-args: ("-compat" "8.19") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.20") -*- *)
 (** Check that the current compatibility flag actually requires the relevant modules. *)
-Import Coq.Compat.Coq819.
+Import Coq.Compat.Coq820.
diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v
@@ -1,5 +1,5 @@
-(* -*- coq-prog-args: ("-compat" "8.17") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.18") -*- *)
 (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq820.
 Import Coq.Compat.Coq819.
 Import Coq.Compat.Coq818.
-Import Coq.Compat.Coq817.
diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v
@@ -0,0 +1,6 @@
+(* -*- coq-prog-args: ("-compat" "8.17") -*- *)
+(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq820.
+Import Coq.Compat.Coq819.
+Import Coq.Compat.Coq818.
+Import Coq.Compat.Coq817.
diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-compat" "8.18") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.19") -*- *)
 (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq820.
 Import Coq.Compat.Coq819.
-Import Coq.Compat.Coq818.
diff --git 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/Coq819.v b/theories/Compat/Coq819.v
@@ -9,3 +9,5 @@
 (************************************************************************)
 
 (** Compatibility file for making Coq act similar to Coq v8.19 *)
+
+Require Export Coq.Compat.Coq820.
diff --git a/theories/Compat/Coq820.v b/theories/Compat/Coq820.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.20 *)
diff --git a/tools/configure/configure.ml b/tools/configure/configure.ml
@@ -22,8 +22,8 @@ open CmdArgs.Prefs
 
 let (/) = Filename.concat
 
-let coq_version = "8.19+alpha"
-let vo_magic = 81899
+let coq_version = "8.20+alpha"
+let vo_magic = 81999
 let is_a_released_version = false
 
 (** Default OCaml binaries *)
Original file line number	Diff line number	Diff line change
Expand Up		@@ -9,3 +9,5 @@
		(************************************************************************)

		(** Compatibility file for making Coq act similar to Coq v8.19 *)

		Require Export Coq.Compat.Coq820.