diff options
| author | Pierre-Marie Pédrot | 2019-12-09 15:17:29 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-09 15:17:29 +0100 |
| commit | e176cec9cd3c9264919c8f2e773b608ec3ef2d07 (patch) | |
| tree | b1d40cbd6ee8fe2885f8af8eb44d87b0a6294ac2 /kernel/safe_typing.mli | |
| parent | d7f493c25a3b1135a4b5b50d85b1d1b4b5ab1b21 (diff) | |
| parent | 88dfc41e23964cb452092deaa67d2ff975ee2b65 (diff) | |
Merge PR #10829: Section.t is never empty
Ack-by: ejgallego
Reviewed-by: ppedrot
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 ae6993b0e2..0b7ca26e09 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -35,7 +35,7 @@ val is_initial : safe_environment -> bool val env_of_safe_env : safe_environment -> Environ.env -val sections_of_safe_env : safe_environment -> section_data Section.t +val sections_of_safe_env : safe_environment -> section_data Section.t option (** The safe_environment state monad *) |