diff options
Diffstat (limited to 'library/global.mli')
| -rw-r--r-- | library/global.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/library/global.mli b/library/global.mli index f8edf3165..b1184da11 100644 --- a/library/global.mli +++ b/library/global.mli @@ -75,7 +75,6 @@ val add_module_parameter : val start_modtype : Id.t -> module_path val end_modtype : Summary.frozen -> Id.t -> module_path -val pack_module : unit -> module_body (** Queries *) |