7 files changed, 25 insertions, 61 deletions
diff --git a/test-suite/bugs/closed/2850.v b/test-suite/bugs/closed/2850.v
deleted file mode 100644
index 64a93aeb00..0000000000
--- a/test-suite/bugs/closed/2850.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Definition id {A} (x : A) := x.
-Fail Compute id.
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/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 *)
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
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.
diff --git a/test-suite/success/vm_evars.v b/test-suite/success/vm_evars.v
new file mode 100644
index 0000000000..2c8b099ef0
--- /dev/null
+++ b/test-suite/success/vm_evars.v
@@ -0,0 +1,23 @@
+Fixpoint iter {A} (n : nat) (f : A -> A) (x : A) :=
+match n with
+| 0 => x
+| S n => iter n f (f x)
+end.
+
+Goal nat -> True.
+Proof.
+intros n.
+evar (f : nat -> nat).
+cut (iter 10 f 0 = 0).
+vm_compute.
+intros; constructor.
+instantiate (f := (fun x => x)).
+reflexivity.
+Qed.
+
+Goal exists x, x = 5 + 5.
+Proof.
+  eexists.
+  vm_compute.
+  reflexivity.
+Qed.