From a028e70817e7fd43b35643a8faa9bc7f59897ddb Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 9 Nov 2020 14:55:23 +0100
Subject: [compat] remove 8.10

---
 doc/stdlib/index-list.html.template   |  1 -
 test-suite/success/CompatOldOldFlag.v |  6 ------
 test-suite/tools/update-compat/run.sh |  2 +-
 theories/Compat/Coq810.v              | 13 -------------
 toplevel/coqargs.ml                   |  3 +--
 5 files changed, 2 insertions(+), 23 deletions(-)
 delete mode 100644 test-suite/success/CompatOldOldFlag.v
 delete mode 100644 theories/Compat/Coq810.v

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index b08d7e9d2c..7201dc6a0e 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -706,7 +706,6 @@ through the <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     theories/Compat/AdmitAxiom.v
-    theories/Compat/Coq810.v
     theories/Compat/Coq811.v
     theories/Compat/Coq812.v
     theories/Compat/Coq813.v
diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v
deleted file mode 100644
index f408e95d2e..0000000000
--- a/test-suite/success/CompatOldOldFlag.v
+++ /dev/null
@@ -1,6 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.10") -*- *)
-(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *)
-Import Coq.Compat.Coq813.
-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 61273c4f37..7ff5571ffb 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 --master || exit $?
+dev/tools/update-compat.py --assert-unchanged --release || exit $?
diff --git a/theories/Compat/Coq810.v b/theories/Compat/Coq810.v
deleted file mode 100644
index d559bd96c3..0000000000
--- a/theories/Compat/Coq810.v
+++ /dev/null
@@ -1,13 +0,0 @@
-(************************************************************************)
-(*         *   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.10 *)
-
-Require Export Coq.Compat.Coq811.
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index d587e57fd8..c6ccf2a427 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -266,8 +266,7 @@ let get_compat_file = function
   | "8.13" -> "Coq.Compat.Coq813"
   | "8.12" -> "Coq.Compat.Coq812"
   | "8.11" -> "Coq.Compat.Coq811"
-  | "8.10" -> "Coq.Compat.Coq810"
-  | ("8.9" | "8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
+  | ("8.10" | "8.9" | "8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
     CErrors.user_err ~hdr:"get_compat_file"
       Pp.(str "Compatibility with version " ++ str s ++ str " not supported.")
   | s ->
-- 
cgit v1.2.3