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.
---
 pretyping/typeclasses_errors.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'pretyping/typeclasses_errors.mli')

diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index fd75781ed5..21bb5f8443 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -12,8 +12,6 @@ open Names
 open EConstr
 open Environ
 
-type contexts = Parameters | Properties
-
 type typeclass_error =
   | NotAClass of constr
   | UnboundMethod of GlobRef.t * lident (** Class name, method *)
-- 
cgit v1.2.3