From c3973cc972cd1474fb4bad308197d64634a518dc Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 5 Nov 2015 17:23:45 +0100
Subject: COMMENT: question

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

(limited to 'doc')

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 611782b4f6..9e11d66ab5 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1464,6 +1464,7 @@ predicate $P$ of type $I\ra \Type$ leads to a paradox when applied to
 impredicative inductive definition like the second-order existential
 quantifier \texttt{exProp} defined above, because it give access to
 the two projections on this type.
+% QUESTION: I did not get the point of the paragraph above.
 
 %\paragraph{Warning: strong elimination}
 %\index{Elimination!Strong elimination}
-- 
cgit v1.2.3