From 8d6e58e16cc53a3198eb4c4afef0a2c39f6a5c56 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 28 Nov 2015 20:02:52 +0100
Subject: Test-suite files for closed bugs

---
 test-suite/bugs/closed/3735.v | 4 ++++
 test-suite/bugs/closed/4284.v | 6 ++++++
 2 files changed, 10 insertions(+)
 create mode 100644 test-suite/bugs/closed/3735.v
 create mode 100644 test-suite/bugs/closed/4284.v

diff --git a/test-suite/bugs/closed/3735.v b/test-suite/bugs/closed/3735.v
new file mode 100644
index 0000000000..a50572ace0
--- /dev/null
+++ b/test-suite/bugs/closed/3735.v
@@ -0,0 +1,4 @@
+Require Import Coq.Program.Tactics.
+Class Foo := { bar : Type }.
+Fail Lemma foo : Foo -> bar. (* 'Command has indeed failed.' in both 8.4 and trunk *)
+Fail Program Lemma foo : Foo -> bar. 
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4284.v b/test-suite/bugs/closed/4284.v
new file mode 100644
index 0000000000..0fff3026ff
--- /dev/null
+++ b/test-suite/bugs/closed/4284.v
@@ -0,0 +1,6 @@
+Set Primitive Projections.
+Record total2 { T: Type } ( P: T -> Type ) := tpair { pr1 : T; pr2 : P pr1 }.
+Theorem onefiber' {X : Type} (P : X -> Type) (x : X) : True.
+Proof.
+set (Q1 := total2 (fun f => pr1 P f = x)).
+set (f1:=fun q1 : Q1 => pr2 _ (pr1 _ q1)).
-- 
cgit v1.2.3