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/safe_typing.ml | |
| parent | e4ebe14337743eba09b93c6f5bff1e1d78083741 (diff) | |
generate variance data for section universes (not yet used)
preparation for direct discharge
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ee101400d6..b732ef5900 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -911,7 +911,9 @@ let check_mind mie lab = let add_mind l mie senv = let () = check_mind mie l in let kn = MutInd.make2 senv.modpath l in - let mib = Indtypes.check_inductive senv.env kn mie in + let sec_univs = Option.map Section.all_poly_univs senv.sections + in + let mib = Indtypes.check_inductive senv.env ~sec_univs kn mie in let mib = match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib in |