diff options
Diffstat (limited to 'kernel/modops.mli')
| -rw-r--r-- | kernel/modops.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/modops.mli b/kernel/modops.mli index 0acd09fb12..119ce2b359 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -57,6 +57,8 @@ val add_linked_module : module_body -> link_info -> env -> env (** same, for a module type *) val add_module_type : ModPath.t -> module_type_body -> env -> env +val add_retroknowledge : module_implementation module_retroknowledge -> env -> env + (** {6 Strengthening } *) val strengthen : module_type_body -> ModPath.t -> module_type_body @@ -109,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 |