diff options
| author | Pierre-Marie Pédrot | 2019-07-29 10:48:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-25 22:14:34 +0200 |
| commit | 58a9de2acacb05291d87fe2b656728ae05d59df4 (patch) | |
| tree | 6472556f7796bf6b8364b61ddcadd942ae6f2763 /kernel/kernel.mllib | |
| parent | 6176c2879dd989029a83642caec7cd66a2a4f527 (diff) | |
Move the Lib section data into the kernel.
Due to the redundancy with some other declaration-specific data from the
kernel, we also seize the opportunity to clean it up. Note also that
discharging is still performed outside of the kernel for now.
Diffstat (limited to 'kernel/kernel.mllib')
| -rw-r--r-- | kernel/kernel.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 66bac15e9a..20e742d7f8 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -49,4 +49,5 @@ Term_typing Subtyping Mod_typing Nativelibrary +Section Safe_typing |