From 4f1d657f42957d0c2d115424564eedf599584cbc Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 29 Oct 2019 13:50:47 +0100
Subject: Remove variance info from inductive entries, infer in indtyping

It gets thrown away if the inductive is declared in a section anyway,
and there is no user syntax to specify it.
---
 kernel/kernel.mllib | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/kernel.mllib')

diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 2b83c2d868..f1e994b337 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -42,9 +42,9 @@ Type_errors
 Modops
 Inductive
 Typeops
+InferCumulativity
 IndTyping
 Indtypes
-InferCumulativity
 Cooking
 Term_typing
 Subtyping
-- 
cgit v1.2.3