diff options
| author | Gaëtan Gilbert | 2019-12-30 11:30:56 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-14 14:56:03 +0100 |
| commit | e4ebe14337743eba09b93c6f5bff1e1d78083741 (patch) | |
| tree | 11463c41539dd6a1af8d3c989a90892c4bc8193d /kernel/indTyping.ml | |
| parent | 8b4f78ded7269139c7e9c222c6382a788c48039a (diff) | |
infercumulativity: take less arguments
Diffstat (limited to 'kernel/indTyping.ml')
| -rw-r--r-- | kernel/indTyping.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index b19472dc99..3f2f9f4fc0 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -335,8 +335,14 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = data, Some None in - (* TODO pass only the needed bits *) - let variance = InferCumulativity.infer_inductive env mie in + let variance = if not mie.mind_entry_cumulative then None + else match mie.mind_entry_universes with + | Monomorphic_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) + in (* Abstract universes *) let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in |