From 5a155b13b6a6820a1c0417025c67170a3e22fedc Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Tue, 3 Nov 2015 13:32:59 +0100
Subject: COMMENT: question

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

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index c3dc80b1a6..c15ee9ffdd 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -820,6 +820,9 @@ in one of the following two cases:
   \item $T$ is $(I~t_1\ldots ~t_n)$
   \item $T$ is $\forall x:U,T^\prime$ where $T^\prime$ is also a type of constructor of $I$
 \end{itemize}
+% QUESTION: Are we above sufficiently precise?
+%           Shouldn't we say also what is "n"?
+%           "n" couldn't be "0", could it?
 
 \paragraph[Examples]{Examples}
 $\nat$ and $\nat\ra\nat$ are types of constructors of $\nat$.\\
-- 
cgit v1.2.3