diff options
| author | Pierre-Marie Pédrot | 2019-12-18 16:52:10 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-18 16:52:10 +0100 |
| commit | dfdfa9eeedebb0aec2cd72be9c1eee27ca9b2fab (patch) | |
| tree | c6e4c772dae91a047c488f20fb3b03afd384300a /kernel/entries.ml | |
| parent | 6b9f6c365ec5b478e79f70cf2a1ae4faed809b74 (diff) | |
| parent | 467d4f28802bf07bb0cdb748c78f0936219ceb8d (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.ml | 2 |
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; |
