diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-26 14:44:00 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-26 14:44:00 +0200 |
| commit | 777751427cbe02ac8a0384d1173f9ef3cce0c8fd (patch) | |
| tree | 0a94ec52799b18061fe9f1ac3a02581e48215121 /API | |
| parent | a0214d53a9a7fa1dc47375c7f048a15bed5dc523 (diff) | |
| parent | d8b78fff7fefd606dae5038b69f220b4f3dd706b (diff) | |
Merge PR #857: Extraction: various fixes related with bug 4720
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 |