From f3a6d9dce4d1c291dbaa03bd0e4ed5f33646bff0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 30 Dec 2019 12:15:21 +0100
Subject: generate variance data for section universes (not yet used)

preparation for direct discharge
---
 kernel/declarations.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 9fd10b32e6..948f52884e 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -223,6 +223,9 @@ type mutual_inductive_body = {
 
     mind_variance : Univ.Variance.t array option; (** Variance info, [None] when non-cumulative. *)
 
+    mind_sec_variance : Univ.Variance.t array option;
+    (** Variance info for section polymorphic universes. [None] outside sections. *)
+
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
 
     mind_typing_flags : typing_flags; (** typing flags at the time of the inductive creation *)
-- 
cgit v1.2.3