From 1c5e2508d6a9604ffd77eff3140a86eafbc672a9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 23 May 2019 10:54:14 +0200
Subject: 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.
---
 test-suite/bugs/closed/bug_10225.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_10225.v

(limited to 'test-suite')

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