aboutsummaryrefslogtreecommitdiff
path: root/kernel/entries.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-12-18 16:52:10 +0100
committerPierre-Marie Pédrot2019-12-18 16:52:10 +0100
commitdfdfa9eeedebb0aec2cd72be9c1eee27ca9b2fab (patch)
treec6e4c772dae91a047c488f20fb3b03afd384300a /kernel/entries.ml
parent6b9f6c365ec5b478e79f70cf2a1ae4faed809b74 (diff)
parent467d4f28802bf07bb0cdb748c78f0936219ceb8d (diff)
Merge PR #11027: Cleanup post #10647 (expose comind universe handling)
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/entries.ml')
-rw-r--r--kernel/entries.ml2
1 files changed, 1 insertions, 1 deletions
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;