From 6176c2879dd989029a83642caec7cd66a2a4f527 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Jul 2019 10:34:47 +0200
Subject: Move cumulativity inference to the kernel.

This is not quite pretty, but it is needed by the section mechanism to rebuild
an inductive when closing a section. Hopefully this can be moved back at some
point.
---
 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 59c1d5890f..66bac15e9a 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -43,6 +43,7 @@ Inductive
 Typeops
 IndTyping
 Indtypes
+InferCumulativity
 Cooking
 Term_typing
 Subtyping
-- 
cgit v1.2.3