Merge branch 'v8.5' into trunk

4 files changed, 8 insertions, 2 deletions

diff --git a/test-suite/bugs/closed/2406.v b/test-suite/bugs/closed/2406.v
index 1bd66ffccb..3766e795a0 100644
--- a/test-suite/bugs/closed/2406.v
+++ b/test-suite/bugs/closed/2406.v
@@ -1,6 +1,6 @@
 (* Check correct handling of unsupported notations *)
 Notation "'’'" := (fun x => x) (at level 20).
 
-(* This fails with a syntax error but it is not catched by Fail
+(* This fails with a syntax error but it is not caught by Fail
 Fail Definition crash_the_rooster f := ’.
 *)
diff --git a/test-suite/bugs/closed/2830.v b/test-suite/bugs/closed/2830.v
index b72c821dfd..bb607b785b 100644
--- a/test-suite/bugs/closed/2830.v
+++ b/test-suite/bugs/closed/2830.v
@@ -123,6 +123,7 @@ Module C.
 
 Reserved Notation "a ~> b" (at level 70, right associativity).
 Reserved Notation "a ≈ b" (at level 54).
+Reserved Notation "a ∘ b" (at level 50, left associativity).
 Generalizable All Variables.
 
 Class Category (Object:Type) (Hom:Object -> Object -> Type) := {
diff --git a/test-suite/bugs/closed/3071.v b/test-suite/bugs/closed/3071.v
index 611ac60655..53c2ef7b71 100644
--- a/test-suite/bugs/closed/3071.v
+++ b/test-suite/bugs/closed/3071.v
@@ -2,4 +2,4 @@ Definition foo := True.
 
 Section foo.
   Global Arguments foo / .
-Fail End foo.
+End foo.
diff --git a/test-suite/bugs/closed/3953.v b/test-suite/bugs/closed/3953.v
new file mode 100644
index 0000000000..167cecea8e
--- /dev/null
+++ b/test-suite/bugs/closed/3953.v
@@ -0,0 +1,5 @@
+(* Checking subst on instances of evars (was bugged in 8.5 beta 1) *)
+Goal forall (a b : unit), a = b -> exists c, b = c.
+  intros.
+  eexists.
+  subst.