From c7f1470c69bf5e8e823550fe94c28fc5fa33e712 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 21 May 2019 14:18:51 +0200
Subject: Adding test for old bug fixed in 8.5 (wrong implicit arguments in
 fixpoint).

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

diff --git a/test-suite/bugs/closed/bug_3810.v b/test-suite/bugs/closed/bug_3810.v
new file mode 100644
index 0000000000..0b2bef8a9b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_3810.v
@@ -0,0 +1,6 @@
+Class Foo.
+
+Fixpoint test (H : Foo) (n : nat) {A : Type} {struct n} : A.
+Admitted.
+
+Check fun (x:Foo) => test x 0.
-- 
cgit v1.2.3