1 files changed, 16 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_12566_1.v b/test-suite/bugs/closed/bug_12566_1.v
new file mode 100644
index 0000000000..22d95949bb
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12566_1.v
@@ -0,0 +1,16 @@
+
+Class C (n:nat) := c{}.
+
+Instance c0 : C 0 := {}.
+
+Definition x := 0.
+
+Opaque x.
+
+Type _ : C x.
+(* this is maybe wrong behaviour, if it changes just update the test *)
+
+Hint Opaque x : typeclass_instances.
+Transparent x.
+
+Fail Type _ : C x.