From 58a9de2acacb05291d87fe2b656728ae05d59df4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Jul 2019 10:48:28 +0200
Subject: 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.
---
 kernel/kernel.mllib | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/kernel.mllib')

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
-- 
cgit v1.2.3