diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index fa53fa33fa..4eef43b193 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -140,6 +140,12 @@ val set_allow_sprop : bool -> safe_transformer0 val check_engagement : Environ.env -> Declarations.set_predicativity -> unit +(** {6 Interactive section functions } *) + +val open_section : poly:bool -> safe_transformer0 + +val close_section : safe_transformer0 + (** {6 Interactive module functions } *) val start_module : Label.t -> ModPath.t safe_transformer |