diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 3d67f6c07..5d1c98de5 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -73,7 +73,7 @@ val add_module : Label.t -> Entries.module_entry -> Declarations.inline -> (module_path * Mod_subst.delta_resolver) safe_transformer val add_modtype : - Label.t -> Entries.module_struct_entry -> Declarations.inline -> + Label.t -> Entries.module_type_entry -> Declarations.inline -> module_path safe_transformer (** Adding universe constraints *) @@ -94,6 +94,8 @@ val add_module_parameter : MBId.t -> Entries.module_struct_entry -> Declarations.inline -> Mod_subst.delta_resolver safe_transformer +(** The optional result type is given without its functorial part *) + val end_module : Label.t -> (Entries.module_struct_entry * Declarations.inline) option -> (module_path * MBId.t list * Mod_subst.delta_resolver) safe_transformer |