diff options
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/API/API.mli b/API/API.mli index 309719539..5160ca3c2 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1222,6 +1222,10 @@ sig | DefinitionEntry of 'a definition_entry | ParameterEntry of parameter_entry | ProjectionEntry of projection_entry + type module_struct_entry = Declarations.module_alg_expr + type module_params_entry = + (Names.MBId.t * module_struct_entry) list + type module_type_entry = module_params_entry * module_struct_entry end module Environ : @@ -1380,6 +1384,9 @@ module Mod_typing : sig type 'alg translation = Declarations.module_signature * 'alg * Mod_subst.delta_resolver * Univ.ContextSet.t + val translate_modtype : + Environ.env -> Names.ModPath.t -> Entries.inline -> + Entries.module_type_entry -> Declarations.module_type_body val translate_mse : Environ.env -> Names.ModPath.t option -> Entries.inline -> Declarations.module_alg_expr -> Declarations.module_alg_expr translation |