diff options
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 4c18ed2752..859f83e052 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -35,6 +35,7 @@ type signature_mismatch_error = | NotConvertibleConstructorField of Id.t | NotConvertibleBodyField | NotConvertibleTypeField of env * types * types + | PolymorphicStatusExpected of bool | NotSameConstructorNamesField | NotSameInductiveNameInBlockField | FiniteInductiveFieldExpected of bool @@ -44,6 +45,10 @@ type signature_mismatch_error = | RecordProjectionsExpected of Name.t list | NotEqualInductiveAliases | NoTypeConstraintExpected + | IncompatibleInstances + | IncompatibleUniverses of Univ.univ_inconsistency + | IncompatiblePolymorphism of env * types * types + | IncompatibleConstraints of Univ.constraints type module_typing_error = | SignatureMismatch of |