diff options
Diffstat (limited to 'kernel/modops.mli')
| -rw-r--r-- | kernel/modops.mli | 46 |
1 files changed, 18 insertions, 28 deletions
diff --git a/kernel/modops.mli b/kernel/modops.mli index 4cd72a2ef..44d29ee3e 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -20,46 +20,38 @@ open Mod_subst (* Various operations on modules and module types *) -(* make the environment entry out of type *) -val module_body_of_type : module_type_body -> module_body -val module_type_of_module : module_path option -> module_body -> +val module_body_of_type : module_path -> module_type_body -> module_body + +val module_type_of_module : env -> module_path option -> module_body -> module_type_body val destr_functor : env -> struct_expr_body -> mod_bound_id * module_type_body * struct_expr_body -val subst_modtype : substitution -> module_type_body -> module_type_body -val subst_structure : substitution -> structure_body -> structure_body - val subst_struct_expr : substitution -> struct_expr_body -> struct_expr_body -val subst_signature_msid : - mod_self_id -> module_path -> - structure_body -> structure_body - -val subst_structure : substitution -> structure_body -> structure_body - -(* Evaluation functions *) -val eval_struct : env -> struct_expr_body -> struct_expr_body - -val type_of_mb : env -> module_body -> struct_expr_body +val subst_signature : substitution -> structure_body -> structure_body -(* [add_signature mp sign env] assumes that the substitution [msid] - $\mapsto$ [mp] has already been performed (or is not necessary, like - when [mp = MPself msid]) *) val add_signature : - module_path -> structure_body -> env -> env + module_path -> structure_body -> delta_resolver -> env -> env (* adds a module and its components, but not the constraints *) -val add_module : - module_path -> module_body -> env -> env +val add_module : module_body -> env -> env val check_modpath_equiv : env -> module_path -> module_path -> unit -val strengthen : env -> struct_expr_body -> module_path -> struct_expr_body +val strengthen : env -> module_type_body -> module_path -> module_type_body -val update_subst : env -> module_body -> module_path -> bool * substitution +val complete_inline_delta_resolver : + env -> module_path -> mod_bound_id -> module_type_body -> + delta_resolver -> delta_resolver + +val strengthen_and_subst_mb : module_body -> module_path -> env -> bool + -> module_body + +val subst_modtype_and_resolver : module_type_body -> module_path -> env -> + module_type_body val error_existing_label : label -> 'a @@ -102,9 +94,7 @@ val error_a_generative_module_expected : label -> 'a val error_local_context : label option -> 'a -val error_no_such_label_sub : label->string->string->'a +val error_no_such_label_sub : label->string->'a + -val resolver_of_environment : - mod_bound_id -> module_type_body -> module_path -> substitution - -> env -> resolver |