diff options
| author | Pierre-Marie Pédrot | 2018-11-19 13:51:59 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 13:51:59 +0100 |
| commit | f9a890aa9ff9d199bd6c98ee33274894fd5d8972 (patch) | |
| tree | cabbb7c9767a7c6b12862fbf36a54c3cc6077f47 /kernel/modops.ml | |
| parent | 1ca5089ebc8250073575ba0b63242a36e66a803e (diff) | |
| parent | 3d49ce63bd1aa35ef2e8abc9cc359ad6031c21bb (diff) | |
Merge PR #8894: Print full binders in subtyping incompatible polymorphism error.
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index bab2eae3df..0dde1c7e75 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -47,10 +47,9 @@ type signature_mismatch_error = | RecordFieldExpected of bool | RecordProjectionsExpected of Name.t list | NotEqualInductiveAliases - | IncompatibleInstances | IncompatibleUniverses of Univ.univ_inconsistency | IncompatiblePolymorphism of env * types * types - | IncompatibleConstraints of Univ.AUContext.t + | IncompatibleConstraints of { got : Univ.AUContext.t; expect : Univ.AUContext.t } type module_typing_error = | SignatureMismatch of |