diff options
| author | Gaëtan Gilbert | 2019-10-05 12:06:35 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-12-07 22:02:52 +0100 |
| commit | 88dfc41e23964cb452092deaa67d2ff975ee2b65 (patch) | |
| tree | a87e121ba83290634a513e87a4dec845e4173365 /kernel/safe_typing.mli | |
| parent | 756d2f4db5eae51c8c01a40550b8c4553bd30f53 (diff) | |
Section.t is never empty
This approach using `type t = { sec_prev: t option; sec_... }` makes
it easy to update sections using the record update syntax, but
impossible to statically ensure that an operation only affects the
current section.
We may instead consider using `type t = section * section list` which
needs some boilerplate to update.
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 *) |