diff options
Diffstat (limited to 'kernel/modops.mli')
| -rw-r--r-- | kernel/modops.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/modops.mli b/kernel/modops.mli index bb97f0171e..119ce2b359 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -111,6 +111,7 @@ type signature_mismatch_error = | IncompatibleUniverses of Univ.univ_inconsistency | IncompatiblePolymorphism of env * types * types | IncompatibleConstraints of { got : Univ.AUContext.t; expect : Univ.AUContext.t } + | IncompatibleVariance type module_typing_error = | SignatureMismatch of |