diff options
Diffstat (limited to 'kernel/mod_typing.mli')
| -rw-r--r-- | kernel/mod_typing.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index 80db12b0d..0c3fb2ba7 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -36,6 +36,9 @@ val translate_mse : env -> module_path option -> inline -> module_struct_entry -> module_alg_expr translation +(** [translate_mse_incl] translate the mse of a real module (no + module type here) given to an Include *) + val translate_mse_incl : env -> module_path -> inline -> module_struct_entry -> module_alg_expr translation |