From d6c45c99a9fd0dae4932f375ac663c368b1bdaf3 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sat, 2 Nov 2019 22:06:07 +0100
Subject: Run update-compat script with --release option.

This should ideally have been done before the 8.11 branching.
---
 doc/stdlib/index-list.html.template      |  1 -
 lib/flags.ml                             |  6 +-----
 lib/flags.mli                            |  2 +-
 test-suite/success/Compat88.v            | 18 ------------------
 test-suite/success/CompatOldOldFlag.v    |  6 ------
 test-suite/success/NotationDeprecation.v | 24 ++++++++++++------------
 test-suite/tools/update-compat/run.sh    |  2 +-
 theories/Compat/Coq88.v                  | 30 ------------------------------
 toplevel/coqargs.ml                      |  1 -
 vernac/g_vernac.mlg                      |  3 +--
 10 files changed, 16 insertions(+), 77 deletions(-)
 delete mode 100644 test-suite/success/Compat88.v
 delete mode 100644 test-suite/success/CompatOldOldFlag.v
 delete mode 100644 theories/Compat/Coq88.v

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 851510b465..21b5678a85 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -639,7 +639,6 @@ through the <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     theories/Compat/AdmitAxiom.v
-    theories/Compat/Coq88.v
     theories/Compat/Coq89.v
     theories/Compat/Coq810.v
     theories/Compat/Coq811.v
diff --git a/lib/flags.ml b/lib/flags.ml
index 90b5f877d5..83588779e5 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -62,14 +62,11 @@ 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_8 | V8_9 | V8_10 | Current
+type compat_version = V8_9 | V8_10 | Current
 
 let compat_version = ref Current
 
 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
@@ -82,7 +79,6 @@ let version_strictly_greater v = version_compare !compat_version v > 0
 let version_less_or_equal v = not (version_strictly_greater v)
 
 let pr_version = function
-  | V8_8 -> "8.8"
   | V8_9 -> "8.9"
   | V8_10 -> "8.10"
   | Current -> "current"
diff --git a/lib/flags.mli b/lib/flags.mli
index 76a78e61fc..5df07399c5 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_8 | V8_9 | V8_10 | Current
+type compat_version = V8_9 | V8_10 | 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/Compat88.v b/test-suite/success/Compat88.v
deleted file mode 100644
index 1233a4b8f5..0000000000
--- a/test-suite/success/Compat88.v
+++ /dev/null
@@ -1,18 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
-(** Check that various syntax usage is available without importing
-    relevant files. *)
-Require Coq.Strings.Ascii Coq.Strings.String.
-Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef.
-Require Coq.Reals.Rdefinitions.
-Require Coq.Numbers.Cyclic.Int63.Cyclic63.
-
-Require Import Coq.Compat.Coq88. (* XXX FIXME Should not need [Require], see https://github.com/coq/coq/issues/8311 *)
-
-Check String.String "a" String.EmptyString.
-Check String.eqb "a" "a".
-Check Nat.eqb 1 1.
-Check BinNat.N.eqb 1 1.
-Check BinInt.Z.eqb 1 1.
-Check BinPos.Pos.eqb 1 1.
-Check Rdefinitions.Rplus 1 1.
-Check Int63.is_zero 1.
diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v
deleted file mode 100644
index 20eef955b4..0000000000
--- a/test-suite/success/CompatOldOldFlag.v
+++ /dev/null
@@ -1,6 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
-(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *)
-Import Coq.Compat.Coq811.
-Import Coq.Compat.Coq810.
-Import Coq.Compat.Coq89.
-Import Coq.Compat.Coq88.
diff --git a/test-suite/success/NotationDeprecation.v b/test-suite/success/NotationDeprecation.v
index d313ba0aa4..96814a1b97 100644
--- a/test-suite/success/NotationDeprecation.v
+++ b/test-suite/success/NotationDeprecation.v
@@ -1,13 +1,13 @@
 Module Syndefs.
 
-#[deprecated(since = "8.8", note = "Do not use.")]
+#[deprecated(since = "8.9", note = "Do not use.")]
 Notation foo := Prop.
 
-Notation bar := Prop (compat "8.8").
+Notation bar := Prop (compat "8.9").
 
 Fail
-#[deprecated(since = "8.8", note = "Do not use.")]
-Notation zar := Prop (compat "8.8").
+#[deprecated(since = "8.9", note = "Do not use.")]
+Notation zar := Prop (compat "8.9").
 
 Check foo.
 Check bar.
@@ -21,14 +21,14 @@ End Syndefs.
 
 Module Notations.
 
-#[deprecated(since = "8.8", note = "Do not use.")]
+#[deprecated(since = "8.9", note = "Do not use.")]
 Notation "!!" := Prop.
 
-Notation "##" := Prop (compat "8.8").
+Notation "##" := Prop (compat "8.9").
 
 Fail
-#[deprecated(since = "8.8", note = "Do not use.")]
-Notation "**" := Prop (compat "8.8").
+#[deprecated(since = "8.9", note = "Do not use.")]
+Notation "**" := Prop (compat "8.9").
 
 Check !!.
 Check ##.
@@ -42,14 +42,14 @@ End Notations.
 
 Module Infix.
 
-#[deprecated(since = "8.8", note = "Do not use.")]
+#[deprecated(since = "8.9", note = "Do not use.")]
 Infix "!!" := plus (at level 1).
 
-Infix "##" := plus (at level 1, compat "8.8").
+Infix "##" := plus (at level 1, compat "8.9").
 
 Fail
-#[deprecated(since = "8.8", note = "Do not use.")]
-Infix "**" := plus (at level 1, compat "8.8").
+#[deprecated(since = "8.9", note = "Do not use.")]
+Infix "**" := plus (at level 1, compat "8.9").
 
 Check (_ !! _).
 Check (_ ## _).
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/Coq88.v b/theories/Compat/Coq88.v
deleted file mode 100644
index 130aa35633..0000000000
--- a/theories/Compat/Coq88.v
+++ /dev/null
@@ -1,30 +0,0 @@
-(************************************************************************)
-(*         *   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.8 *)
-Local Set Warnings "-deprecated".
-
-Require Export Coq.Compat.Coq89.
-
-(** In Coq 8.9, prim token notations follow [Import] rather than
-    [Require].  So we make all of the relevant notations accessible in
-    compatibility mode. *)
-Require Coq.Strings.Ascii Coq.Strings.String.
-Export String.StringSyntax Ascii.AsciiSyntax.
-Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef.
-Require Coq.Reals.Rdefinitions.
-Require Coq.Numbers.Cyclic.Int63.Int63.
-Require Coq.Numbers.Cyclic.Int31.Int31.
-Declare ML Module "r_syntax_plugin".
-Declare ML Module "int63_syntax_plugin".
-Numeral Notation BinNums.Z BinIntDef.Z.of_int BinIntDef.Z.to_int : Z_scope.
-Numeral Notation BinNums.positive BinPosDef.Pos.of_int BinPosDef.Pos.to_int : positive_scope.
-Numeral Notation BinNums.N BinNatDef.N.of_int BinNatDef.N.to_int : N_scope.
-Numeral Notation Int31.int31 Int31.phi_inv_nonneg Int31.phi : int31_scope.
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 1529959cc6..8dd1c45024 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -176,7 +176,6 @@ let add_vo_require opts d p export =
 
 let add_compat_require opts v =
   match v with
-  | Flags.V8_8 -> add_vo_require opts "Coq.Compat.Coq88" None (Some false)
   | 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)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index b4c0a33585..4243d0c911 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -65,8 +65,7 @@ let parse_compat_version = let open Flags in function
   | "8.11" -> Current
   | "8.10" -> V8_10
   | "8.9" -> V8_9
-  | "8.8" -> V8_8
-  | ("8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
+  | ("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_version"
       Pp.(str "Compatibility with version " ++ str s ++ str " not supported.")
   | s ->
-- 
cgit v1.2.3