diff options
Diffstat (limited to 'library/global.mli')
| -rw-r--r-- | library/global.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/library/global.mli b/library/global.mli index d0bd556d70..9ac6b1f53c 100644 --- a/library/global.mli +++ b/library/global.mli @@ -71,6 +71,11 @@ val add_include : Entries.module_struct_entry -> bool -> Declarations.inline -> Mod_subst.delta_resolver +(** Sections *) + +val open_section : poly:bool -> unit +val close_section : Summary.frozen -> unit + (** Interactive modules and module types *) val start_module : Id.t -> ModPath.t |