diff options
| author | Gaëtan Gilbert | 2019-12-30 19:19:32 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-15 13:43:35 +0100 |
| commit | 73c3b874633d6f6f8af831d4a37d0c1ae52575bc (patch) | |
| tree | 3ca8004e6f295b6812b1f585d12f64fde01ef909 /kernel/declarations.ml | |
| parent | f3a6d9dce4d1c291dbaa03bd0e4ed5f33646bff0 (diff) | |
Discharge inductive types without rechecking them
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 948f52884e..0b6e59bd5e 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -224,7 +224,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. *) + (** Variance info for section polymorphic universes. [None] + outside sections. The final variance once all sections are + discharged is [mind_sec_variance ++ mind_variance]. *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) |