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 /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/typeclasses_errors.ml | 4 | ||||
| -rw-r--r-- | pretyping/typeclasses_errors.mli | 2 |
2 files changed, 0 insertions, 6 deletions
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index af5b3016c9..90ecab1608 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -8,13 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(*i*) open Names open EConstr open Environ -(*i*) - -type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr 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 *) |