From 2cb48a3fe5a8cd435e4e0ad6990e5ee5e6079fa5 Mon Sep 17 00:00:00 2001
From: Matej Kosik <m4tej.kosik@gmail.com>
Date: Sat, 7 Nov 2015 16:17:44 +0100
Subject: COMMENT: to do

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

(limited to 'doc/refman/RefMan-cic.tex')

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 092dba46b..3d56dcac6 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1745,6 +1745,8 @@ Each $A_i$ should be a type (reducible to a term) starting with at least
 $k_i$ products $\forall y_1:B_1,\ldots \forall y_{k_i}:B_{k_i}, A'_i$ 
 and $B_{k_i}$
 being an instance of an inductive definition.
+% TODO: We should probably define somewhere explicitely, what we mean by
+%       "x is an instance of an inductive type I".
 
 Now in the definition $t_i$, if $f_j$ occurs then it should be applied
 to at least $k_j$ arguments and the $k_j$-th argument should be
-- 
cgit v1.2.3

