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/constr.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/constr.mli')
0 files changed, 0 insertions, 0 deletions