aboutsummaryrefslogtreecommitdiff
path: root/API
diff options
context:
space:
mode:
Diffstat (limited to 'API')
-rw-r--r--API/API.mli7
1 files changed, 4 insertions, 3 deletions
diff --git a/API/API.mli b/API/API.mli
index d1774afe54..aa7f93bb25 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1280,9 +1280,9 @@ sig
| Algebraic of module_expression
| Struct of module_signature
| FullStruct
- and module_body =
+ and 'a generic_module_body =
{ mod_mp : Names.ModPath.t;
- mod_expr : module_implementation;
+ mod_expr : 'a;
mod_type : module_signature;
mod_type_alg : module_expression option;
mod_constraints : Univ.ContextSet.t;
@@ -1290,7 +1290,8 @@ sig
mod_retroknowledge : Retroknowledge.action list
}
and module_signature = (module_type_body,structure_body) functorize
- and module_type_body = module_body
+ and module_body = module_implementation generic_module_body
+ and module_type_body = unit generic_module_body
and structure_body = (Names.Label.t * structure_field_body) list
and structure_field_body =
| SFBconst of constant_body