diff options
| author | Gaëtan Gilbert | 2019-05-23 10:54:14 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-11 09:55:51 +0200 |
| commit | 1c5e2508d6a9604ffd77eff3140a86eafbc672a9 (patch) | |
| tree | 2a93d48b0dd438db2b936e3cbbfe322f2140604f /interp/implicit_quantifiers.ml | |
| parent | 82663b28a04d82e89bd041efd256c4838312e587 (diff) | |
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.
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index e8d10488b2..32290f0430 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -23,9 +23,6 @@ open Libobject open Nameops open Context.Rel.Declaration -exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *) -let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m)) - module RelDecl = Context.Rel.Declaration (*i*) |