diff options
| -rw-r--r-- | pretyping/inferCumulativity.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index 43d2aa75e..a0a8276c5 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -184,6 +184,8 @@ let infer_arity_constructor env variances arcn is_arity params = let arcn' = Term.it_mkProd_or_LetIn arcn params in let typs, codom = Reduction.dest_prod env arcn' in let env, variances = Context.Rel.fold_outside infer_typ typs ~init:(env, variances) in + (* If we have Inductive foo@{i j} : ... -> Type@{i} := C : ... -> foo Type@{j} + i is irrelevant, j is invariant. *) if not is_arity then basic_check env variances codom else variances let infer_inductive env mie = |