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/classes.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/classes.mli')
| -rw-r--r-- | vernac/classes.mli | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/vernac/classes.mli b/vernac/classes.mli index ace9096469..36c2d22c1d 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -14,12 +14,6 @@ open Constrexpr open Typeclasses open Libnames -(** Errors *) - -val mismatched_params : env -> constr_expr list -> Constr.rel_context -> 'a - -val mismatched_props : env -> constr_expr list -> Constr.rel_context -> 'a - (** Instance declaration *) val declare_instance : ?warn:bool -> env -> Evd.evar_map -> |