diff options
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.ml | 5 | ||||
| -rw-r--r-- | API/API.mli | 7 |
2 files changed, 12 insertions, 0 deletions
diff --git a/API/API.ml b/API/API.ml index 32c664d7b1..08efdfa871 100644 --- a/API/API.ml +++ b/API/API.ml @@ -201,4 +201,9 @@ module Entries = | 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 diff --git a/API/API.mli b/API/API.mli index b1a746e028..c52c305853 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1299,12 +1299,19 @@ 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 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 |