From 760765859cb74930ac8fd14fc1a241aa8ae20aa0 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Wed, 4 Nov 2015 19:41:25 +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 b862db3204..9e49481e23 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1007,6 +1007,7 @@ constructors which will always be satisfied for the impredicative sort
 {\Prop} but may fail to define inductive definition 
 on sort \Set{} and generate constraints between universes for
 inductive definitions in the {\Type} hierarchy.
+% QUESTION: which 'constraint' are we above referring to?
 
 \paragraph{Examples.}
 It is well known that existential quantifier can be encoded as an
-- 
cgit v1.2.3