From ff7be36add22cf3c6efd24a27ebdde818fc1dc06 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 20 Feb 2018 14:10:58 +0100
Subject: Turn warning for deprecated notations on.

Fix new deprecation warnings in the standard library.
---
 test-suite/output/PrintInfos.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'test-suite')

diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v
index 08918981a4..a498db3e89 100644
--- a/test-suite/output/PrintInfos.v
+++ b/test-suite/output/PrintInfos.v
@@ -26,6 +26,7 @@ About bar.
 Print bar.
 
 About Peano. (* Module *)
+Set Warnings "-deprecated".
 About existS2. (* Notation *)
 
 Arguments eq_refl {A} {x}, {A} x.
-- 
cgit v1.2.3


From a4817d25befc71b7dbf707637660431144985133 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 20 Feb 2018 13:55:46 +0100
Subject: Remove VOld compatibility flag.

---
 test-suite/bugs/closed/4785_compat_85.v | 46 ---------------------------------
 test-suite/bugs/closed/4798.v           |  2 +-
 2 files changed, 1 insertion(+), 47 deletions(-)
 delete mode 100644 test-suite/bugs/closed/4785_compat_85.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4785_compat_85.v b/test-suite/bugs/closed/4785_compat_85.v
deleted file mode 100644
index bbb34f465c..0000000000
--- a/test-suite/bugs/closed/4785_compat_85.v
+++ /dev/null
@@ -1,46 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.5") -*- *)
-Require Coq.Lists.List Coq.Vectors.Vector.
-Require Coq.Compat.Coq85.
-
-Module A.
-Import Coq.Lists.List Coq.Vectors.Vector.
-Import ListNotations.
-Check [ ]%list : list _.
-Import VectorNotations ListNotations.
-Delimit Scope vector_scope with vector.
-Check [ ]%vector : Vector.t _ _.
-Check []%vector : Vector.t _ _.
-Check [ ]%list : list _.
-Fail Check []%list : list _.
-
-Goal True.
-  idtac; [ ]. (* Note that vector notations break the [ | .. | ] syntax of Ltac *)
-Abort.
-
-Inductive mylist A := mynil | mycons (x : A) (xs : mylist A).
-Delimit Scope mylist_scope with mylist.
-Bind Scope mylist_scope with mylist.
-Arguments mynil {_}, _.
-Arguments mycons {_} _ _.
-Notation " [] " := mynil (compat "8.5") : mylist_scope.
-Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
-Notation " [ x ] " := (mycons x nil) : mylist_scope.
-Notation " [ x ; y ; .. ; z ] " :=  (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope.
-
-Import Coq.Compat.Coq85.
-Locate Module VectorNotations.
-Import VectorDef.VectorNotations.
-
-Check []%vector : Vector.t _ _.
-Check []%mylist : mylist _.
-Check [ ]%mylist : mylist _.
-Check [ ]%list : list _.
-End A.
-
-Module B.
-Import Coq.Compat.Coq85.
-
-Goal True.
-  idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *)
-Abort.
-End B.
diff --git a/test-suite/bugs/closed/4798.v b/test-suite/bugs/closed/4798.v
index dbc3d46fce..6f2bcb9685 100644
--- a/test-suite/bugs/closed/4798.v
+++ b/test-suite/bugs/closed/4798.v
@@ -1,3 +1,3 @@
 Check match 2 with 0 => 0 | S n => n end.
-Notation "|" := 1 (compat "8.4").
+Notation "|" := 1 (compat "8.6").
 Check match 2 with 0 => 0 | S n => n end. (* fails *)
-- 
cgit v1.2.3


From 3ce123f16ce19f67dde4a0f3f2874a2678649907 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 20 Feb 2018 16:03:57 +0100
Subject: Remove 8.5 compatibility support.

---
 test-suite/bugs/closed/4785.v | 11 -----------
 test-suite/bugs/closed/4873.v |  1 -
 2 files changed, 12 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v
index c3c97d3f59..0d347b262d 100644
--- a/test-suite/bugs/closed/4785.v
+++ b/test-suite/bugs/closed/4785.v
@@ -1,5 +1,4 @@
 Require Coq.Lists.List Coq.Vectors.Vector.
-Require Coq.Compat.Coq85.
 
 Module A.
 Import Coq.Lists.List Coq.Vectors.Vector.
@@ -21,12 +20,10 @@ Delimit Scope mylist_scope with mylist.
 Bind Scope mylist_scope with mylist.
 Arguments mynil {_}, _.
 Arguments mycons {_} _ _.
-Notation " [] " := mynil (compat "8.5") : mylist_scope.
 Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
 Notation " [ x ] " := (mycons x nil) : mylist_scope.
 Notation " [ x ; y ; .. ; z ] " :=  (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope.
 
-Import Coq.Compat.Coq85.
 Locate Module VectorNotations.
 Import VectorDef.VectorNotations.
 
@@ -35,11 +32,3 @@ Check []%mylist : mylist _.
 Check [ ]%mylist : mylist _.
 Check [ ]%list : list _.
 End A.
-
-Module B.
-Import Coq.Compat.Coq85.
-
-Goal True.
-  idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *)
-Abort.
-End B.
diff --git a/test-suite/bugs/closed/4873.v b/test-suite/bugs/closed/4873.v
index 3be36d8475..39299883ad 100644
--- a/test-suite/bugs/closed/4873.v
+++ b/test-suite/bugs/closed/4873.v
@@ -1,6 +1,5 @@
 Require Import Coq.Classes.Morphisms.
 Require Import Relation_Definitions.
-Require Import Coq.Compat.Coq85.
 
 Fixpoint tuple' T n : Type :=
   match n with
-- 
cgit v1.2.3