diff options
| author | Emilio Jesus Gallego Arias | 2020-03-07 04:40:06 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-22 18:54:00 -0400 |
| commit | a0820546c0f21ba43bcdfa1041e826f33c81804d (patch) | |
| tree | 3b154eb8afb81d23628d5f2a2f593d7649be182f /kernel/nativelib.ml | |
| parent | a011d14500b4ac69370c77e225ead51c347675c1 (diff) | |
[obligations] Don't allocate libobjects for obligation info.
Obligations/Program currently allocates a libobject object just to
check that there are no obligations pending at the end of a section.
I think this is not the right use case for libobject, thus we turn the
check into an explicit one at the vernac level.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions