From 293a84d36f7f2610efa4451d965684708cc6b8f3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 16 Jul 2014 18:08:22 +0200
Subject: Adding a test-suite for bug #3416.

---
 test-suite/bugs/closed/3416.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 test-suite/bugs/closed/3416.v

diff --git a/test-suite/bugs/closed/3416.v b/test-suite/bugs/closed/3416.v
new file mode 100644
index 0000000000..5cfb8f1ff4
--- /dev/null
+++ b/test-suite/bugs/closed/3416.v
@@ -0,0 +1,12 @@
+Inductive list A := Node : node A -> list A
+with node A := Nil | Cons : A -> list A -> node A.
+
+Fixpoint app {A} (l1 l2 : list A) {struct l1} : list A
+with app_node {A} (n1 : node A) (l2 : list A) {struct n1} : node A.
+Proof.
++ destruct l1 as [n]; constructor.
+  exact (app_node _ n l2).
++ destruct n1 as [|x l1].
+  - destruct l2 as [n2]; exact n2.
+  - exact (Cons _ x (app _ l1 l2)).
+Qed.
-- 
cgit v1.2.3