From 3602b909afc6eac0f150c9961a04b0bf50d8bbf0 Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Fri, 10 Mar 2017 11:05:27 -0500
Subject: funind: Ignore missing info for current function

Fixes [Coq bug #5372](https://coq.inria.fr/bugs/show_bug.cgi?id=5372)
"Anomaly: Not a valid information when defining mutual fixpoints that
are not mutual with Function".
---
 test-suite/bugs/closed/5372.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/5372.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5372.v b/test-suite/bugs/closed/5372.v
new file mode 100644
index 0000000000..2dc78d4c7f
--- /dev/null
+++ b/test-suite/bugs/closed/5372.v
@@ -0,0 +1,7 @@
+(* coq bug 5372: https://coq.inria.fr/bugs/show_bug.cgi?id=5372 *)
+Function odd (n:nat) :=
+  match n with
+  | 0 => false
+  | S n => true
+  end
+with even (n:nat) := false.
-- 
cgit v1.2.3