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/entries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/entries.ml')

diff --git a/kernel/entries.ml b/kernel/entries.ml
index b50c3ebbc3..8d930b521c 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -50,7 +50,7 @@ type mutual_inductive_entry = {
   mind_entry_params : Constr.rel_context;
   mind_entry_inds : one_inductive_entry list;
   mind_entry_universes : universes_entry;
-  mind_entry_variance : Univ.Variance.t array option;
+  mind_entry_cumulative : bool;
   (* universe constraints and the constraints for subtyping of
      inductive types in the block. *)
   mind_entry_private : bool option;
-- 
cgit v1.2.3