diff options
Diffstat (limited to 'library/global.mli')
| -rw-r--r-- | library/global.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/global.mli b/library/global.mli index 4a215167a..72d3731df 100644 --- a/library/global.mli +++ b/library/global.mli @@ -57,7 +57,7 @@ val add_constraints : constraints -> unit of the started module / module type *) val start_module : - dir_path -> identifier -> (mod_bound_id * module_type_entry) list + identifier -> (mod_bound_id * module_type_entry) list -> module_type_entry option -> module_path @@ -65,7 +65,7 @@ val end_module : identifier -> module_path val start_modtype : - dir_path -> identifier -> (mod_bound_id * module_type_entry) list + identifier -> (mod_bound_id * module_type_entry) list -> module_path val end_modtype : |