1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3010b.v b/test-suite/bugs/closed/3010b.v
new file mode 100644
index 00000000..65fea424
--- /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).