diff options
Diffstat (limited to 'plugins/extraction/miniml.mli')
| -rw-r--r-- | plugins/extraction/miniml.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 104a4c865..5aaef254e 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -149,7 +149,7 @@ type ml_specif = and ml_module_type = | MTident of module_path - | MTfunsig of mod_bound_id * ml_module_type * ml_module_type + | MTfunsig of MBId.t * ml_module_type * ml_module_type | MTsig of module_path * ml_module_sig | MTwith of ml_module_type * ml_with_declaration @@ -166,7 +166,7 @@ type ml_structure_elem = and ml_module_expr = | MEident of module_path - | MEfunctor of mod_bound_id * ml_module_type * ml_module_expr + | MEfunctor of MBId.t * ml_module_type * ml_module_expr | MEstruct of module_path * ml_module_structure | MEapply of ml_module_expr * ml_module_expr |