From d62af5e39af63387f60dd0a92d9fbfd65974fcae Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Wed, 4 Nov 2015 19:24:41 +0100
Subject: COMMENT: to do

---
 doc/refman/RefMan-cic.tex | 1 +
 1 file changed, 1 insertion(+)

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 51a0068b03..bacd62b776 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -999,6 +999,7 @@ provided that the following side conditions hold:
   $I_{q_i}$ which satisfies the positivity condition for $I_1 \ldots  I_k$
   and $c_i \notin \Gamma \cup E$.
 \end{itemize}
+% TODO: justify the above constraints
 \end{description}
 One can remark that there is a constraint between the sort of the
 arity of the inductive type and the sort of the type of its
-- 
cgit v1.2.3