Merge branch 'v8.5' into trunk

6 files changed, 28 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.
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 21b829aa19..a4ed76c5a0 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -536,3 +536,13 @@ Goal forall f:nat->nat, (forall P x, P (f x)) -> let x:=f 0 in x = 0.
 intros f H x.
 apply H.
 Qed.
+
+(* Test that occur-check is not too restrictive (see comments of #3141) *)
+Lemma bar (X: nat -> nat -> Prop) (foo:forall x, X x x) (a: unit) (H: tt = a):
+  exists x, exists y, X x y.
+Proof.
+intros; eexists; eexists; case H.
+apply (foo ?y).
+Grab Existential Variables.
+exact 0.
+Qed.
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 6dcd6592b5..62249666b3 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -148,3 +148,13 @@ eexists. intro H.
 rewrite H.
 reflexivity.
 Abort.
+
+(* Check that rewriting within evars still work (was broken in 8.5beta1) *)
+
+
+Goal forall (a: unit) (H: a = tt), exists x y:nat, x = y.
+intros; eexists; eexists.
+rewrite H.
+Undo.
+subst.
+Abort.