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