From 91597060c0919489a29c31bc60b6ae0d754ef09b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 10 Feb 2018 11:38:13 +0100
Subject: inferCumulativity: add comment to explain [if not is_arity].

---
 pretyping/inferCumulativity.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index 43d2aa75e3..a0a8276c5c 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 =
-- 
cgit v1.2.3