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.
---
 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 +-
 4 files changed, 13 insertions(+), 37 deletions(-)
 delete mode 100644 test-suite/success/Compat88.v
 delete mode 100644 test-suite/success/CompatOldOldFlag.v

(limited to 'test-suite')

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 $?
-- 
cgit v1.2.3