From 74f8381ed943f1e786b32c49fb31f14fd488dc9c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 10 Sep 2016 11:37:21 +0200
Subject: Test for #5077.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5077.v b/test-suite/bugs/closed/5077.v
new file mode 100644
index 0000000000..7e7f2c3737
--- /dev/null
+++ b/test-suite/bugs/closed/5077.v
@@ -0,0 +1,8 @@
+(* Testing robustness of typing for a fixpoint with evars in its type *)
+
+Inductive foo (n : nat) : Type := .
+Definition foo_denote {n} (x : foo n) : Type := match x with end.
+
+Definition baz : forall n (x : foo n), foo_denote x.
+refine (fix go n (x : foo n) : foo_denote x := _).
+Abort.  
-- 
cgit v1.2.3


From 90e5945e1666540bc18e7a9b831d136041f4e487 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 12 Sep 2016 17:22:03 +0200
Subject: Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.

---
 test-suite/output/Notations2.out | 2 ++
 test-suite/output/Notations2.v   | 5 +++++
 2 files changed, 7 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 6ff1d38372..13ed7816d8 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -54,3 +54,5 @@ end
      : ∀ x : nat, x <= 0 -> {x0 : nat | x <= x0}
 exist (Q x) y conj
      : {x0 : A | Q x x0}
+{1, 2}
+     : nat -> Prop
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 4e0d135d7d..3f3945052e 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -106,3 +106,8 @@ Check fun x (H:le x 0) => exist (le x) 0 H.
 
 Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y).
 Check (exist (Q x) y conj).
+
+(* Check bug raised on coq-club on Sep 12, 2016 *)
+
+Notation "{ x , y , .. , v }" := (fun a => (or .. (or (a = x) (a = y)) .. (a = v))).
+Check ({1, 2}).
-- 
cgit v1.2.3


From 2aaa58c22e37b05e3637ac7161bb464da7db054a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 14 Sep 2016 10:22:41 +0200
Subject: Fixing test-suite after commit 43104a0b.

---
 test-suite/success/TestRefine.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v
index c8a8b862fa..023cb5f59d 100644
--- a/test-suite/success/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -53,7 +53,7 @@ Abort.
 
 Lemma essai2 : forall x : nat, x = x.
 
-Fail refine (fix f (x : nat) : x = x := _).
+refine (fix f (x : nat) : x = x := _).
 
 Restart.
 
-- 
cgit v1.2.3