From d35d3ec3d3da592e4d2f8d69119ef0f47e21f0d0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 23 Feb 2015 11:51:11 +0100
Subject: Fixing test for bug #3071.

---
 test-suite/bugs/closed/3071.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3


From 865c8cd9c3d6cd5dd91a86a26b81efe53bdf444a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 23 Feb 2015 11:54:33 +0100
Subject: Fixing test #2830.

---
 test-suite/bugs/closed/2830.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'test-suite')

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) := {
-- 
cgit v1.2.3


From 71def2f885989376c8c2940d37f7fc407ed0a4c5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 23 Feb 2015 11:59:04 +0100
Subject: Fixing occur-check which was too strong in unification.ml.

---
 test-suite/success/apply.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3


From 06ad2a73251f38c59c43c03a0edca34d5ef3dd8e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 23 Feb 2015 12:43:01 +0100
Subject: Fixing rewrite/subst when the subterm to rewrite is argument of an
 Evar.

This was broken by the attempt to use the same algorithm for rewriting
closed subterms than for rewriting subterms with evars: the algorithm
to find subterms (w_unify_to_subterm) did not go through evars. But
what to do when looking say, for a pattern "S ?n" in a goal "S ?x[a:=S ?y]"?
Should we unify ?x[a:=S ?y] with ?n or consider ?x as rigid and look
in the instance? If we adopt the first approach, then, what to do when
looking for "S ?n" in a goal "?x[a:=S ?y]"? Failing? Looking in the
instance? Is it normal that an evar behaves as a rigid constant when
it cannot be unified with the pattern?
---
 test-suite/success/rewrite.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3


From 705bf896bfc552e95403d097fe9b8031c598d88b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 23 Feb 2015 13:24:24 +0100
Subject: Test for #3953 (subst in evar instances).

---
 test-suite/bugs/closed/3953.v | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 test-suite/bugs/closed/3953.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3


From df2f50db3703b4f7f88f00ac382c7f3f1efaceb3 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 23 Feb 2015 11:26:51 +0100
Subject: Fix some typos in comments.

---
 test-suite/bugs/closed/2406.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

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 := ’.
 *)
-- 
cgit v1.2.3