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.
---
 interp/constrintern.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'interp/constrintern.mli')

diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 0d4bc91f57..2e4d7479a9 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -189,3 +189,7 @@ val for_grammar : ('a -> 'b) -> 'a -> 'b
 
 (** Placeholder for global option, should be moved to a parameter *)
 val get_asymmetric_patterns : unit -> bool
+
+val check_duplicate : ?loc:Loc.t -> (qualid * constr_expr) list -> unit
+(** Check that a list of record field definitions doesn't contain
+    duplicates. *)
-- 
cgit v1.2.3