Fix #10225 (Instance := {} accepts duplicate fields)

This replaces the mismatched context error, which occurred when
Instance := {} was used with strictly more fields than declared.

Since we later check that field names match those declared for the
instance, now that we reject duplicates we know that there are no
extra fields.

1 files changed, 7 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_10225.v b/test-suite/bugs/closed/bug_10225.v
new file mode 100644
index 0000000000..6d6bb39a65
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10225.v
@@ -0,0 +1,7 @@
+
+Class Bar := {}.
+Instance bb : Bar := {}.
+
+Class Foo := { xx : Bar; foo : nat }.
+
+Fail Instance bar : Foo := { foo := 1 + 1; foo := 2 + 2 }.