1 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5012.v b/test-suite/bugs/closed/5012.v
new file mode 100644
index 00000000..5326c0fb
--- /dev/null
+++ b/test-suite/bugs/closed/5012.v
@@ -0,0 +1,17 @@
+Class Foo := { foo : Set }.
+
+Axiom admit : forall {T}, T.
+
+Global Instance Foo0 : Foo
+  := {| foo := admit |}.
+
+Global Instance Foo1 : Foo
+  := { foo := admit }.
+
+Existing Class Foo.
+
+Global Instance Foo2 : Foo
+  := { foo := admit }. (* Error: Unbound method name foo of class Foo. *)
+
+Set Warnings "+already-existing-class".
+Fail Existing Class Foo.