From 701a69732ef2abfc7384296e090a3e9bd7604bbd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 11 Nov 2015 18:45:32 +0100
Subject: Fixing bug #3554: Anomaly: Anonymous implicit argument.

We just handle unnamed implicits using a dummy name. Note that the implicit
argument logic should still output warnings whenever the user writes implicit
arguments that won't be taken into account, but I'll leave that for another
time.
---
 test-suite/bugs/closed/3554.v | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 test-suite/bugs/closed/3554.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3554.v b/test-suite/bugs/closed/3554.v
new file mode 100644
index 0000000000..13a79cc840
--- /dev/null
+++ b/test-suite/bugs/closed/3554.v
@@ -0,0 +1 @@
+Example foo (f : forall {_ : Type}, Type) : Type.
-- 
cgit v1.2.3