From 37ba76b1ba6f4f5edcf05d69e6a21a46fef026d9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 23 Jun 2020 14:17:30 +0200
Subject: Hint Opaque/Transparent/Unfold: don't error on opaque constants

Helps with #12566
---
 test-suite/bugs/closed/bug_12566_1.v | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_12566_1.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3