Merge PR #11158: [release] Update files for 8.12 release per release process.

Reviewed-by: Zimmi48

18 files changed, 87 insertions, 59 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index d566d56331..493397adee 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -323,7 +323,7 @@ pkg:opam:
     - opam pin add --kind=path coqide.$COQ_VERSION .
     - set +e
   variables:
-    COQ_VERSION: "8.11"
+    COQ_VERSION: "8.12"
     OPAM_SWITCH: "edge"
     OPAM_VARIANT: "+flambda"
   only: *full-ci
diff --git a/META.coq.in b/META.coq.in
index 9869e7f575..49bdea6d9c 100644
--- a/META.coq.in
+++ b/META.coq.in
@@ -1,7 +1,7 @@
 # TODO: Generate automatically with Dune
 
 description = "The Coq Proof Assistant Plugin API"
-version = "8.11"
+version = "8.12"
 
 directory = ""
 requires = ""
@@ -9,7 +9,7 @@ requires = ""
 package "config" (
 
   description = "Coq Configuration Variables"
-  version     = "8.11"
+  version     = "8.12"
 
   directory   = "config"
 
@@ -19,7 +19,7 @@ package "config" (
 
 package "clib" (
   description = "Base General Coq Library"
-  version     = "8.11"
+  version     = "8.12"
 
   directory   = "clib"
   requires    = "str, unix, threads"
@@ -31,7 +31,7 @@ package "clib" (
 package "lib" (
 
   description = "Base Coq-Specific Library"
-  version     = "8.11"
+  version     = "8.12"
 
   directory   = "lib"
 
@@ -45,7 +45,7 @@ package "lib" (
 package "vm" (
 
   description = "Coq VM"
-  version     = "8.11"
+  version     = "8.12"
 
   directory        = "kernel/byterun"
 
@@ -64,7 +64,7 @@ package "vm" (
 package "kernel" (
 
   description = "Coq's Kernel"
-  version     = "8.11"
+  version     = "8.12"
 
   directory   = "kernel"
 
@@ -78,7 +78,7 @@ package "kernel" (
 package "library" (
 
   description = "Coq Libraries (vo) support"
-  version     = "8.11"
+  version     = "8.12"
 
   requires    = "coq.kernel"
 
@@ -92,7 +92,7 @@ package "library" (
 package "engine" (
 
   description = "Coq Tactic Engine"
-  version     = "8.11"
+  version     = "8.12"
 
   requires    = "coq.library"
   directory   = "engine"
@@ -105,7 +105,7 @@ package "engine" (
 package "pretyping" (
 
   description = "Coq Pretyper"
-  version     = "8.11"
+  version     = "8.12"
 
   requires    = "coq.engine"
   directory   = "pretyping"
@@ -118,7 +118,7 @@ package "pretyping" (
 package "interp" (
 
   description = "Coq Term Interpretation"
-  version     = "8.11"
+  version     = "8.12"
 
   requires    = "coq.pretyping"
   directory   = "interp"
@@ -131,7 +131,7 @@ package "interp" (
 package "proofs" (
 
   description = "Coq Proof Engine"
-  version     = "8.11"
+  version     = "8.12"
 
   requires    = "coq.interp"
   directory   = "proofs"
@@ -144,7 +144,7 @@ package "proofs" (
 package "gramlib" (
 
   description = "Coq Grammar Engine"
-  version     = "8.11"
+  version     = "8.12"
 
   requires    = "coq.lib"
   directory   = "gramlib/.pack"
@@ -156,7 +156,7 @@ package "gramlib" (
 package "parsing" (
 
   description = "Coq Parsing Engine"
-  version     = "8.11"
+  version     = "8.12"
 
   requires    = "coq.gramlib, coq.proofs"
   directory   = "parsing"
@@ -169,7 +169,7 @@ package "parsing" (
 package "printing" (
 
   description = "Coq Printing Engine"
-  version     = "8.11"
+  version     = "8.12"
 
   requires    = "coq.parsing"
   directory   = "printing"
@@ -182,7 +182,7 @@ package "printing" (
 package "tactics" (
 
   description = "Coq Basic Tactics"
-  version     = "8.11"
+  version     = "8.12"
 
   requires    = "coq.printing"
   directory   = "tactics"
@@ -195,7 +195,7 @@ package "tactics" (
 package "vernac" (
 
   description = "Coq Vernacular Interpreter"
-  version     = "8.11"
+  version     = "8.12"
 
   requires    = "coq.tactics"
   directory   = "vernac"
@@ -208,7 +208,7 @@ package "vernac" (
 package "stm" (
 
   description = "Coq State Transactional Machine"
-  version     = "8.11"
+  version     = "8.12"
 
   requires    = "coq.vernac"
   directory   = "stm"
@@ -221,7 +221,7 @@ package "stm" (
 package "toplevel" (
 
   description = "Coq Toplevel"
-  version     = "8.11"
+  version     = "8.12"
 
   requires    = "num, coq.stm"
   directory   = "toplevel"
@@ -234,7 +234,7 @@ package "toplevel" (
 package "idetop" (
 
   description = "Coq IDE Libraries"
-  version     = "8.11"
+  version     = "8.12"
 
   requires    = "coq.toplevel"
   directory   = "ide"
@@ -247,7 +247,7 @@ package "idetop" (
 package "ide" (
 
   description = "Coq IDE Libraries"
-  version     = "8.11"
+  version     = "8.12"
 
   requires    = "coq.lib, coq.ideprotocol, lablgtk3, lablgtk3-sourceview3"
   directory   = "ide"
@@ -260,7 +260,7 @@ package "ide" (
 package "ideprotocol" (
 
   description = "Coq IDE protocol"
-  version     = "8.11"
+  version     = "8.12"
 
   requires    = "coq.toplevel"
   directory   = "ide/protocol"
@@ -273,14 +273,14 @@ package "ideprotocol" (
 package "plugins" (
 
   description = "Coq built-in plugins"
-  version     = "8.11"
+  version     = "8.12"
 
   directory   = "plugins"
 
   package "ltac" (
 
     description = "Coq LTAC Plugin"
-    version     = "8.11"
+    version     = "8.12"
 
     requires    = "coq.stm"
     directory   = "ltac"
@@ -295,7 +295,7 @@ package "plugins" (
   package "tauto" (
 
     description = "Coq tauto plugin"
-    version     = "8.11"
+    version     = "8.12"
 
     requires    = "coq.plugins.ltac"
     directory   = "ltac"
@@ -310,7 +310,7 @@ package "plugins" (
   package "omega" (
 
     description = "Coq omega plugin"
-    version     = "8.11"
+    version     = "8.12"
 
     requires    = "coq.plugins.ltac"
     directory   = "omega"
@@ -325,7 +325,7 @@ package "plugins" (
   package "micromega" (
 
     description = "Coq micromega plugin"
-    version     = "8.11"
+    version     = "8.12"
 
     requires    = "num,coq.plugins.ltac"
     directory   = "micromega"
@@ -340,7 +340,7 @@ package "plugins" (
   package "zify" (
 
     description = "Coq Zify plugin"
-    version     = "8.11"
+    version     = "8.12"
 
     requires    = "coq.plugins.ltac"
     directory   = "micromega"
@@ -355,7 +355,7 @@ package "plugins" (
   package "setoid_ring" (
 
     description = "Coq newring plugin"
-    version     = "8.11"
+    version     = "8.12"
 
     requires    = ""
     directory   = "setoid_ring"
@@ -370,7 +370,7 @@ package "plugins" (
   package "extraction" (
 
     description = "Coq extraction plugin"
-    version     = "8.11"
+    version     = "8.12"
 
     requires    = "coq.plugins.ltac"
     directory   = "extraction"
@@ -385,7 +385,7 @@ package "plugins" (
   package "cc" (
 
     description = "Coq cc plugin"
-    version     = "8.11"
+    version     = "8.12"
 
     requires    = "coq.plugins.ltac"
     directory   = "cc"
@@ -400,7 +400,7 @@ package "plugins" (
   package "firstorder" (
 
     description = "Coq ground plugin"
-    version     = "8.11"
+    version     = "8.12"
 
     requires    = "coq.plugins.ltac"
     directory   = "firstorder"
@@ -415,7 +415,7 @@ package "plugins" (
   package "rtauto" (
 
     description = "Coq rtauto plugin"
-    version     = "8.11"
+    version     = "8.12"
 
     requires    = "coq.plugins.ltac"
     directory   = "rtauto"
@@ -430,7 +430,7 @@ package "plugins" (
   package "btauto" (
 
     description = "Coq btauto plugin"
-    version     = "8.11"
+    version     = "8.12"
 
     requires    = "coq.plugins.ltac"
     directory   = "btauto"
@@ -445,7 +445,7 @@ package "plugins" (
   package "funind" (
 
     description = "Coq recdef plugin"
-    version     = "8.11"
+    version     = "8.12"
 
     requires    = "coq.plugins.extraction"
     directory   = "funind"
@@ -460,7 +460,7 @@ package "plugins" (
   package "nsatz" (
 
     description = "Coq nsatz plugin"
-    version     = "8.11"
+    version     = "8.12"
 
     requires    = "num,coq.plugins.ltac"
     directory   = "nsatz"
@@ -475,7 +475,7 @@ package "plugins" (
   package "rsyntax" (
 
     description = "Coq rsyntax plugin"
-    version     = "8.11"
+    version     = "8.12"
 
     requires    = ""
     directory   = "syntax"
@@ -490,7 +490,7 @@ package "plugins" (
   package "int63syntax" (
 
     description = "Coq int63syntax plugin"
-    version     = "8.11"
+    version     = "8.12"
 
     requires    = ""
     directory   = "syntax"
@@ -505,7 +505,7 @@ package "plugins" (
   package "string_notation" (
 
     description = "Coq string_notation plugin"
-    version     = "8.11"
+    version     = "8.12"
 
     requires    = ""
     directory   = "syntax"
@@ -520,7 +520,7 @@ package "plugins" (
   package "derive" (
 
     description = "Coq derive plugin"
-    version     = "8.11"
+    version     = "8.12"
 
     requires    = ""
     directory   = "derive"
@@ -535,7 +535,7 @@ package "plugins" (
   package "ssrmatching" (
 
     description = "Coq ssrmatching plugin"
-    version     = "8.11"
+    version     = "8.12"
 
     requires    = "coq.plugins.ltac"
     directory   = "ssrmatching"
@@ -550,7 +550,7 @@ package "plugins" (
   package "ssreflect" (
 
     description = "Coq ssreflect plugin"
-    version     = "8.11"
+    version     = "8.12"
 
     requires    = "coq.plugins.ssrmatching"
     directory   = "ssr"
diff --git a/README.md b/README.md
index 739bb5148e..d3d5057be9 100644
--- a/README.md
+++ b/README.md
@@ -103,7 +103,7 @@ used, and include a complete source example leading to the bug.
 
 Guidelines for contributing to Coq in various ways are listed in the [contributor's guide](CONTRIBUTING.md).
 
-Information about the next release is at https://github.com/coq/coq/wiki/Release-Plan
+Information about release plans is at https://github.com/coq/coq/wiki/Release-Plan
 
 ## Supporting Coq
 
diff --git a/configure.ml b/configure.ml
index d4521a7872..88bc3f912b 100644
--- a/configure.ml
+++ b/configure.ml
@@ -12,11 +12,11 @@
 #load "str.cma"
 open Printf
 
-let coq_version = "8.11+alpha"
-let coq_macos_version = "8.10.90" (** "[...] should be a string comprised of
+let coq_version = "8.12+alpha"
+let coq_macos_version = "8.11.90" (** "[...] should be a string comprised of
 three non-negative, period-separated integers [...]" *)
-let vo_magic = 81091
-let state_magic = 581091
+let vo_magic = 81191
+let state_magic = 581191
 let is_a_released_version = false
 let distributed_exec =
   ["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt";
diff --git a/default.nix b/default.nix
index 19afc2bd1b..6a7a98aa5e 100644
--- a/default.nix
+++ b/default.nix
@@ -29,7 +29,7 @@
 , shell ? false
   # We don't use lib.inNixShell because that would also apply
   # when in a nix-shell of some package depending on this one.
-, coq-version ? "8.11-git"
+, coq-version ? "8.12-git"
 }:
 
 with pkgs;
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 8ab00c6fd8..7d394c3401 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,3 +1,5 @@
+## Changes between Coq 8.11 and Coq 8.12
+
 ## Changes between Coq 8.10 and Coq 8.11
 
 ### ML API
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 21b5678a85..ac611926b3 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -642,5 +642,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/Compat/Coq89.v
     theories/Compat/Coq810.v
     theories/Compat/Coq811.v
+    theories/Compat/Coq812.v
   </dd>
 </dl>
diff --git a/lib/flags.ml b/lib/flags.ml
index 83588779e5..27ca8e9596 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -62,7 +62,7 @@ let we_are_parsing = ref false
 (* Current means no particular compatibility consideration.
    For correct comparisons, this constructor should remain the last one. *)
 
-type compat_version = V8_9 | V8_10 | Current
+type compat_version = V8_9 | V8_10 | V8_11 | Current
 
 let compat_version = ref Current
 
@@ -73,6 +73,9 @@ let version_compare v1 v2 = match v1, v2 with
   | V8_10, V8_10 -> 0
   | V8_10, _ -> -1
   | _, V8_10 -> 1
+  | V8_11, V8_11 -> 0
+  | V8_11, _ -> -1
+  | _, V8_11 -> 1
   | Current, Current -> 0
 
 let version_strictly_greater v = version_compare !compat_version v > 0
@@ -81,6 +84,7 @@ let version_less_or_equal v = not (version_strictly_greater v)
 let pr_version = function
   | V8_9 -> "8.9"
   | V8_10 -> "8.10"
+  | V8_11 -> "8.11"
   | Current -> "current"
 
 (* Translate *)
diff --git a/lib/flags.mli b/lib/flags.mli
index 5df07399c5..36a996401d 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -52,7 +52,7 @@ val we_are_parsing : bool ref
 (* Set Printing All flag. For some reason it is a global flag *)
 val raw_print : bool ref
 
-type compat_version = V8_9 | V8_10 | Current
+type compat_version = V8_9 | V8_10 | V8_11 | Current
 val compat_version : compat_version ref
 val version_compare : compat_version -> compat_version -> int
 val version_strictly_greater : compat_version -> bool
diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v
index fd6101bf89..c86548440b 100644
--- a/test-suite/success/CompatCurrentFlag.v
+++ b/test-suite/success/CompatCurrentFlag.v
@@ -1,3 +1,3 @@
-(* -*- coq-prog-args: ("-compat" "8.11") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.12") -*- *)
 (** Check that the current compatibility flag actually requires the relevant modules. *)
-Import Coq.Compat.Coq811.
+Import Coq.Compat.Coq812.
diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v
index f774cef44f..a1c1209db6 100644
--- a/test-suite/success/CompatOldFlag.v
+++ b/test-suite/success/CompatOldFlag.v
@@ -1,5 +1,5 @@
-(* -*- coq-prog-args: ("-compat" "8.9") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.10") -*- *)
 (** Check that the current-minus-two 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/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v
new file mode 100644
index 0000000000..dd259988ac
--- /dev/null
+++ b/test-suite/success/CompatOldOldFlag.v
@@ -0,0 +1,6 @@
+(* -*- 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/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v
index 1c5ccc1a92..00f4747e3e 100644
--- a/test-suite/success/CompatPreviousFlag.v
+++ b/test-suite/success/CompatPreviousFlag.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-compat" "8.10") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.11") -*- *)
 (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq812.
 Import Coq.Compat.Coq811.
-Import Coq.Compat.Coq810.
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/Coq811.v b/theories/Compat/Coq811.v
index 4a9a041d4e..4d28e4f708 100644
--- a/theories/Compat/Coq811.v
+++ b/theories/Compat/Coq811.v
@@ -9,3 +9,5 @@
 (************************************************************************)
 
 (** Compatibility file for making Coq act similar to Coq v8.11 *)
+
+Require Export Coq.Compat.Coq812.
diff --git a/theories/Compat/Coq812.v b/theories/Compat/Coq812.v
new file mode 100644
index 0000000000..5d2fbc56d5
--- /dev/null
+++ b/theories/Compat/Coq812.v
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*         *   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.12 *)
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 8dd1c45024..e3116550d9 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -178,7 +178,8 @@ let add_compat_require opts v =
   match v with
   | Flags.V8_9 -> add_vo_require opts "Coq.Compat.Coq89" None (Some false)
   | Flags.V8_10 -> add_vo_require opts "Coq.Compat.Coq810" None (Some false)
-  | Flags.Current -> add_vo_require opts "Coq.Compat.Coq811" None (Some false)
+  | Flags.V8_11 -> add_vo_require opts "Coq.Compat.Coq811" None (Some false)
+  | Flags.Current -> add_vo_require opts "Coq.Compat.Coq812" None (Some false)
 
 let add_load_vernacular opts verb s =
   { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }}
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 5b97e06b2b..3095ab3fe1 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -63,7 +63,8 @@ let make_bullet s =
   | _ -> assert false
 
 let parse_compat_version = let open Flags in function
-  | "8.11" -> Current
+  | "8.12" -> Current
+  | "8.11" -> V8_11
   | "8.10" -> V8_10
   | "8.9" -> V8_9
   | ("8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->