From ff8bac52149f8a32498f765bd579e00fcbd4f080 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 5 Apr 2014 16:22:59 -0400
Subject: Test case for bug 3037

Closed in 4a8950ec7a0d9f2b216e67e69b446c064590a8e9
---
 test-suite/bugs/closed/3037.v | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test-suite/bugs/closed/3037.v

diff --git a/test-suite/bugs/closed/3037.v b/test-suite/bugs/closed/3037.v
new file mode 100644
index 0000000000..baa7eff549
--- /dev/null
+++ b/test-suite/bugs/closed/3037.v
@@ -0,0 +1,11 @@
+(* Anomaly before 4a8950ec7a0d9f2b216e67e69b446c064590a8e9 *)
+
+Require Import Recdef.
+
+Function f_R (a: nat) {wf (fun x y: nat => False)  a}:Prop:=
+  match a:nat with
+    | 0 => True
+    | (S y') => f_R y'
+  end.
+(* Anomaly: File "plugins/funind/recdef.ml", line 916, characters 13-19: Assertion failed.
+Please report. *)
-- 
cgit v1.2.3