Merge PR#375: Deprecation

7 files changed, 0 insertions, 171 deletions

diff --git a/test-suite/bugs/closed/4394.v b/test-suite/bugs/closed/4394.v
deleted file mode 100644
index 1ad81345d..000000000
--- a/test-suite/bugs/closed/4394.v
+++ /dev/null
@@ -1,19 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-
-Require Import Equality List.
-Inductive Foo (I : Type -> Type) (A : Type) : Type :=
-| foo (B : Type) : A -> I B -> Foo I A.
-Definition Family := Type -> Type.
-Definition FooToo : Family -> Family := Foo.
-Definition optionize (I : Type -> Type) (A : Type) := option (I A).
-Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo (optionize I) A := foo (optionize I) A A.
-Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }.
-Definition barRec : Rec (optionize id) := {| rec := bar id |}.
-Inductive Empty {T} : T -> Prop := .
-Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family) nil)) (b : unit) :
-  Empty (a, b) -> False.
-Proof.
-  intro e.
-  dependent induction e.
-Qed.
-
diff --git a/test-suite/bugs/closed/4400.v b/test-suite/bugs/closed/4400.v
deleted file mode 100644
index a89cf0cbc..000000000
--- a/test-suite/bugs/closed/4400.v
+++ /dev/null
@@ -1,19 +0,0 @@
-(* -*- coq-prog-args: ("-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *)
-Require Import Coq.Lists.List Coq.Logic.JMeq Program.Equality.
-Set Printing Universes.
-Inductive Foo (I : Type -> Type) (A : Type) : Type :=
-| foo (B : Type) : A -> I B -> Foo I A.
-Definition Family := Type -> Type.
-Definition FooToo : Family -> Family := Foo.
-Definition optionize (I : Type -> Type) (A : Type) := option (I A).
-Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo(optionize I) A := foo (optionize I) A A.
-Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }.
-Definition barRec : Rec (optionize id) := {| rec := bar id |}.
-Inductive Empty {T} : T -> Prop := .
-Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family)
-nil)) (b : unit) :
-  Empty (a, b) -> False.
-Proof.
-  intro e.
-  dependent induction e.
-Qed.
diff --git a/test-suite/bugs/closed/4656.v b/test-suite/bugs/closed/4656.v
deleted file mode 100644
index a59eed2c8..000000000
--- a/test-suite/bugs/closed/4656.v
+++ /dev/null
@@ -1,4 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-Goal True.
-  constructor 1.
-Qed.
diff --git a/test-suite/bugs/closed/4727.v b/test-suite/bugs/closed/4727.v
deleted file mode 100644
index cfb4548d2..000000000
--- a/test-suite/bugs/closed/4727.v
+++ /dev/null
@@ -1,10 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-Goal forall (P : Set) (l : P) (P0 : Set) (w w0 : P0) (T : Type) (a : P * T) (o : P -> option P0),
-    (forall (l1 l2 : P) (w1 : P0), o l1 = Some w1 -> o l2 = Some w1 -> l1 = l2) ->
-    o l = Some w -> o (fst a) = Some w0 -> {w = w0} + {w <> w0} -> False.
-Proof.
-  clear; intros ???????? inj H0 H1 H2.
-  destruct H2; intuition subst.
-  eapply inj in H1; [ | eauto ].
-  progress subst. (* should succeed, used to not succeed *)
-Abort.
diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v
deleted file mode 100644
index a90abd71c..000000000
--- a/test-suite/bugs/closed/4733.v
+++ /dev/null
@@ -1,52 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5.  If they use*)
-Require Import Coq.Lists.List.
-Require Import Coq.Vectors.Vector.
-Import ListNotations.
-Import VectorNotations.
-Set Implicit Arguments.
-Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T).
-Arguments mynil {_}, _.
-
-Delimit Scope mylist_scope with mylist.
-Bind Scope mylist_scope with mylist.
-Delimit Scope vector_scope with vector.
-
-Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
-Notation " [ x ] " := (mycons x mynil) : mylist_scope.
-Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope.
-
-(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4.  There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *)
-Check [ ]%mylist : mylist _.
-Check [ ]%list : list _.
-Check []%vector : Vector.t _ _.
-Check [ _ ]%mylist : mylist _.
-Check [ _ ]%list : list _.
-Check [ _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%list : list _.
-Check [ _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
-
-Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope.
-(* Now these all work, but not so in 8.4.  If we get the ability to remove notations, this section can also just be removed. *)
-Check [ ]%mylist : mylist _.
-Check [ ]%list : list _.
-Check []%vector : Vector.t _ _.
-Check [ _ ]%mylist : mylist _.
-Check [ _ ]%list : list _.
-Check [ _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%list : list _.
-Check [ _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v
deleted file mode 100644
index 4541f13d0..000000000
--- a/test-suite/bugs/opened/4803.v
+++ /dev/null
@@ -1,48 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5.  If they use*)
-Require Import Coq.Lists.List.
-Require Import Coq.Vectors.Vector.
-Import ListNotations.
-Import VectorNotations.
-Set Implicit Arguments.
-Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T).
-Arguments mynil {_}, _.
-
-Delimit Scope mylist_scope with mylist.
-Bind Scope mylist_scope with mylist.
-Delimit Scope vector_scope with vector.
-
-Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
-Notation " [ x ] " := (mycons x mynil) : mylist_scope.
-Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope.
-
-(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4.  There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *)
-Check [ ]%mylist : mylist _.
-Check [ ]%list : list _.
-Check []%vector : Vector.t _ _.
-Check [ _ ]%mylist : mylist _.
-Check [ _ ]%list : list _.
-Check [ _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%list : list _.
-Check [ _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
-
-(** Now check that we can add and then remove notations from the parser *)
-(* We should be able to stick some vernacular here to remove [] from the parser *)
-Fail Remove Notation "[]".
-Goal True.
-  (* This should not be a syntax error; before moving this file to closed, uncomment this line. *)
-  (* idtac; []. *)
-  constructor.
-Qed.
-
-Check { _ : _ & _ }.
-Reserved Infix "&" (at level 0).
-Fail Remove Infix "&".
-(* Check { _ : _ & _ }. *)
diff --git a/test-suite/success/Compat84.v b/test-suite/success/Compat84.v
deleted file mode 100644
index 732a024fc..000000000
--- a/test-suite/success/Compat84.v
+++ /dev/null
@@ -1,19 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-
-Goal True.
-  solve [ constructor 1 ]. Undo.
-  solve [ econstructor 1 ]. Undo.
-  solve [ constructor ]. Undo.
-  solve [ econstructor ]. Undo.
-  solve [ constructor (fail) ]. Undo.
-  solve [ econstructor (fail) ]. Undo.
-  split.
-Qed.
-
-Goal False \/ True.
-  solve [ constructor (constructor) ]. Undo.
-  solve [ econstructor (econstructor) ]. Undo.
-  solve [ constructor 2; constructor ]. Undo.
-  solve [ econstructor 2; econstructor ]. Undo.
-  right; esplit.
-Qed.