diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index d3ca642a89..d97d61a72f 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -134,7 +134,7 @@ val check_engagement : Environ.env -> Declarations.set_predicativity -> unit (** {6 Interactive section functions } *) -val open_section : poly:bool -> safe_transformer0 +val open_section : safe_transformer0 val close_section : safe_transformer0 |