Adding a test-suite for bug #3416.

1 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3416.v b/test-suite/bugs/closed/3416.v
new file mode 100644
index 000000000..5cfb8f1ff
--- /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.