From 8b2a7924b2849d527e8afbcec3e8017e3f3a1429 Mon Sep 17 00:00:00 2001
From: Xavier Clerc
Date: Fri, 26 Sep 2014 11:57:03 +0200
Subject: Test cases for closed bugs.

---
 test-suite/bugs/closed/3010b.v | 5 +++++
 test-suite/bugs/closed/3016.v  | 4 ++++
 2 files changed, 9 insertions(+)
 create mode 100644 test-suite/bugs/closed/3010b.v
 create mode 100644 test-suite/bugs/closed/3016.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3010b.v b/test-suite/bugs/closed/3010b.v
new file mode 100644
index 0000000000..65fea42489
--- /dev/null
+++ b/test-suite/bugs/closed/3010b.v
@@ -0,0 +1,5 @@
+Definition wtf (n : nat) : nat :=
+  (match n with
+       0 => (fun H : n = 0 => 0)
+     | S n' => (fun H : n = S n' => 0)
+   end) (eq_refl n).
diff --git a/test-suite/bugs/closed/3016.v b/test-suite/bugs/closed/3016.v
new file mode 100644
index 0000000000..bd4f1dd805
--- /dev/null
+++ b/test-suite/bugs/closed/3016.v
@@ -0,0 +1,4 @@
+Section foo.
+  Variable C : Type.
+  Goal True.
+    change (eq (A := ?C) ?x ?y) with (eq).
-- 
cgit v1.2.3