diff options
| author | Gaëtan Gilbert | 2019-12-30 12:15:21 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-15 13:43:24 +0100 |
| commit | f3a6d9dce4d1c291dbaa03bd0e4ed5f33646bff0 (patch) | |
| tree | 5253356704c6db77afc0af218815bbf5b38ffad2 /kernel/declarations.ml | |
| parent | e4ebe14337743eba09b93c6f5bff1e1d78083741 (diff) | |
generate variance data for section universes (not yet used)
preparation for direct discharge
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 3 |
1 files changed, 3 insertions, 0 deletions
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 *) |