diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-10 11:38:13 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-11 22:28:39 +0100 |
| commit | 91597060c0919489a29c31bc60b6ae0d754ef09b (patch) | |
| tree | 5af8bc9d64e3baca71f7861f7ac2b273290685ac /pretyping | |
| parent | d3253a01da1f76e4317f9cf218976c765e0df858 (diff) | |
inferCumulativity: add comment to explain [if not is_arity].
Diffstat (limited to 'pretyping')
| -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 = |