Update -compat to support -compat 8.10

This commit was created via `./dev/tools/update-compat.py --master`

12 files changed, 37 insertions, 11 deletions

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 51f94d7e5a..c33df52038 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -618,5 +618,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/Compat/Coq87.v
     theories/Compat/Coq88.v
     theories/Compat/Coq89.v
+    theories/Compat/Coq810.v
   </dd>
 </dl>
diff --git a/lib/flags.ml b/lib/flags.ml
index ae4d337ded..55bfa3cbde 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -66,7 +66,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_7 | V8_8 | Current
+type compat_version = V8_7 | V8_8 | V8_9 | Current
 
 let compat_version = ref Current
 
@@ -77,6 +77,9 @@ let version_compare v1 v2 = match v1, v2 with
   | V8_8, V8_8 -> 0
   | V8_8, _ -> -1
   | _, V8_8 -> 1
+  | V8_9, V8_9 -> 0
+  | V8_9, _ -> -1
+  | _, V8_9 -> 1
   | Current, Current -> 0
 
 let version_strictly_greater v = version_compare !compat_version v > 0
@@ -85,6 +88,7 @@ let version_less_or_equal v = not (version_strictly_greater v)
 let pr_version = function
   | V8_7 -> "8.7"
   | V8_8 -> "8.8"
+  | V8_9 -> "8.9"
   | Current -> "current"
 
 (* Translate *)
diff --git a/lib/flags.mli b/lib/flags.mli
index d883cf1e30..7336b9beaf 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -58,7 +58,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_7 | V8_8 | Current
+type compat_version = V8_7 | V8_8 | V8_9 | 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 5650dba236..81469d79c3 100644
--- a/test-suite/success/CompatCurrentFlag.v
+++ b/test-suite/success/CompatCurrentFlag.v
@@ -1,3 +1,3 @@
-(* -*- coq-prog-args: ("-compat" "8.9") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.10") -*- *)
 (** Check that the current compatibility flag actually requires the relevant modules. *)
-Import Coq.Compat.Coq89.
+Import Coq.Compat.Coq810.
diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v
index 37d50ee67d..afeb57f9f2 100644
--- a/test-suite/success/CompatOldFlag.v
+++ b/test-suite/success/CompatOldFlag.v
@@ -1,5 +1,5 @@
-(* -*- coq-prog-args: ("-compat" "8.7") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
 (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq810.
 Import Coq.Compat.Coq89.
 Import Coq.Compat.Coq88.
-Import Coq.Compat.Coq87.
diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v
new file mode 100644
index 0000000000..1f62635f50
--- /dev/null
+++ b/test-suite/success/CompatOldOldFlag.v
@@ -0,0 +1,6 @@
+(* -*- coq-prog-args: ("-compat" "8.7") -*- *)
+(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq810.
+Import Coq.Compat.Coq89.
+Import Coq.Compat.Coq88.
+Import Coq.Compat.Coq87.
diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v
index 9981388381..c8f75915c8 100644
--- a/test-suite/success/CompatPreviousFlag.v
+++ b/test-suite/success/CompatPreviousFlag.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.9") -*- *)
 (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq810.
 Import Coq.Compat.Coq89.
-Import Coq.Compat.Coq88.
diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh
index 02a2348450..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 --cur-version=8.9 || exit $?
+dev/tools/update-compat.py --assert-unchanged --master || exit $?
diff --git a/theories/Compat/Coq810.v b/theories/Compat/Coq810.v
new file mode 100644
index 0000000000..f10201661e
--- /dev/null
+++ b/theories/Compat/Coq810.v
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <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.10 *)
diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v
index decb5c7519..05d63d9a47 100644
--- a/theories/Compat/Coq89.v
+++ b/theories/Compat/Coq89.v
@@ -11,5 +11,7 @@
 (** Compatibility file for making Coq act similar to Coq v8.9 *)
 Local Set Warnings "-deprecated".
 
+Require Export Coq.Compat.Coq810.
+
 Unset Private Polymorphic Universes.
 Set Refine Instance Mode.
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 0a32879764..eaa050bdce 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -165,7 +165,8 @@ let add_compat_require opts v =
   match v with
   | Flags.V8_7 -> add_vo_require opts "Coq.Compat.Coq87" None (Some false)
   | Flags.V8_8 -> add_vo_require opts "Coq.Compat.Coq88" None (Some false)
-  | Flags.Current -> add_vo_require opts "Coq.Compat.Coq89" None (Some false)
+  | Flags.V8_9 -> add_vo_require opts "Coq.Compat.Coq89" None (Some false)
+  | Flags.Current -> add_vo_require opts "Coq.Compat.Coq810" None (Some false)
 
 let set_batch_mode opts =
   (* XXX: This should be in the argument record *)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3bc4aecdb1..79adefdcf7 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -61,7 +61,8 @@ let make_bullet s =
   | _ -> assert false
 
 let parse_compat_version = let open Flags in function
-  | "8.9" -> Current
+  | "8.10" -> Current
+  | "8.9" -> V8_9
   | "8.8" -> V8_8
   | "8.7" -> V8_7
   | ("8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->