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/indTyping.ml | |
| parent | e4ebe14337743eba09b93c6f5bff1e1d78083741 (diff) | |
generate variance data for section universes (not yet used)
preparation for direct discharge
Diffstat (limited to 'kernel/indTyping.ml')
| -rw-r--r-- | kernel/indTyping.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 3f2f9f4fc0..591cd050a5 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -276,7 +276,7 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp let kelim = allowed_sorts univ_info in (arity,lc), (indices,splayed_lc), kelim -let typecheck_inductive env (mie:mutual_inductive_entry) = +let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = let () = match mie.mind_entry_inds with | [] -> CErrors.anomaly Pp.(str "empty inductive types declaration.") | _ -> () @@ -341,7 +341,12 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = CErrors.user_err Pp.(str "Inductive cannot be both monomorphic and universe cumulative.") | Polymorphic_entry (_,uctx) -> let univs = Instance.to_array @@ UContext.instance uctx in - Some (InferCumulativity.infer_inductive ~env_params univs mie.mind_entry_inds) + let univs = match sec_univs with + | None -> univs + | Some sec_univs -> Array.append sec_univs univs + in + let variances = InferCumulativity.infer_inductive ~env_params univs mie.mind_entry_inds in + Some variances in (* Abstract universes *) |