diff options
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 |