diff options
Diffstat (limited to 'kernel/modops.mli')
| -rw-r--r-- | kernel/modops.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/modops.mli b/kernel/modops.mli index 9c00b8194..f34fa88c4 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -39,8 +39,8 @@ val check_modpath_equiv : env -> module_path -> module_path -> unit val strengthen : env -> module_type_body -> module_path -> module_type_body -val complete_inline_delta_resolver : - env -> module_path -> mod_bound_id -> module_type_body -> +val inline_delta_resolver : + env -> inline -> module_path -> mod_bound_id -> module_type_body -> delta_resolver -> delta_resolver val strengthen_and_subst_mb : module_body -> module_path -> env -> bool |