From 43869b4e05824244e666c60e0b740a80e8b09d0c Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Tue, 28 Jun 2016 12:37:00 -0400
Subject: no-refold patch

Add a boolean for refolding during reduction, and an option
that is off by default in 8.6, to turn refolding on in all reduction
functions, as in 8.5.
---
 test-suite/bugs/closed/3424.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3424.v b/test-suite/bugs/closed/3424.v
index f9b2c38611..ee8cabf171 100644
--- a/test-suite/bugs/closed/3424.v
+++ b/test-suite/bugs/closed/3424.v
@@ -13,6 +13,7 @@ Notation "0" := (trunc_S minus_one) : trunc_scope.
 Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A.
 Notation IsHProp := (IsTrunc minus_one).
 Notation IsHSet := (IsTrunc 0).
+Set Refolding Reduction.
 Goal forall (A : Type) (a b : A) (H' : IsHSet A), { x : Type & IsHProp x }.
 Proof.
 intros.
-- 
cgit v1.2.3


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/bugs')

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 650550fc95d5ba41da84e2003371522221e27734 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 18 Jun 2016 19:07:42 -0400
Subject: Add a test for 4836

This required improving the machinery of the test-suite Makefile to
support -compile.
---
 test-suite/bugs/closed/PLACEHOLDER.v        | 0
 test-suite/bugs/closed/bug_4836.v           | 1 +
 test-suite/bugs/closed/bug_4836/PLACEHOLDER | 0
 3 files changed, 1 insertion(+)
 create mode 100644 test-suite/bugs/closed/PLACEHOLDER.v
 create mode 100644 test-suite/bugs/closed/bug_4836.v
 create mode 100644 test-suite/bugs/closed/bug_4836/PLACEHOLDER

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/PLACEHOLDER.v b/test-suite/bugs/closed/PLACEHOLDER.v
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/test-suite/bugs/closed/bug_4836.v b/test-suite/bugs/closed/bug_4836.v
new file mode 100644
index 0000000000..5838dcd8a7
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4836.v
@@ -0,0 +1 @@
+(* -*- coq-prog-args: ("-compile" "bugs/closed/PLACEHOLDER.v") -*- *)
diff --git a/test-suite/bugs/closed/bug_4836/PLACEHOLDER b/test-suite/bugs/closed/bug_4836/PLACEHOLDER
new file mode 100644
index 0000000000..e69de29bb2
-- 
cgit v1.2.3