From 09cbae6c995c3e94ac8f0e53e6857da8e491a2fe Mon Sep 17 00:00:00 2001
From: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
Date: Thu, 8 Jun 2017 14:54:39 +0200
Subject: Adding a test case as requested in bug 5205.

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

(limited to 'test-suite/bugs/closed/5205.v')

diff --git a/test-suite/bugs/closed/5205.v b/test-suite/bugs/closed/5205.v
new file mode 100644
index 000000000..406f37a4b
--- /dev/null
+++ b/test-suite/bugs/closed/5205.v
@@ -0,0 +1,6 @@
+Definition foo (n : nat) (m : nat) : nat := m.
+
+Arguments foo {_} _, _ _.
+
+Check foo 1 1.
+Check foo (n:=1) 1.
-- 
cgit v1.2.3