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 /vernac/himsg.mli | |
| 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 'vernac/himsg.mli')
| -rw-r--r-- | vernac/himsg.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/vernac/himsg.mli b/vernac/himsg.mli index d1c1c092e3..09384cb859 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -24,8 +24,6 @@ val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> Pp.t val explain_inductive_error : inductive_error -> Pp.t -val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Constr.rel_context -> Pp.t - val explain_typeclass_error : env -> Evd.evar_map -> typeclass_error -> Pp.t val explain_recursion_scheme_error : env -> recursion_scheme_error -> Pp.t |