From 0117f54f3e3678f348f8ed84c8444dc614ce8298 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 29 Oct 2015 10:03:30 +0100
Subject: COMMENT: to do

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

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 834c8273a5..505587988c 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -62,6 +62,11 @@ Formally, we call {\Sort} the set of sorts which is defined by:
 \index{Set@{\Set}}
 Their properties are defined in Section~\ref{subtyping-rules}.
 
+% TODO: Somewhere in the document we should explain:
+% - what concrete actions (in *.v files) cause creation of new universes
+% - different kinds of relationships between universes (i.e. "max" and "succ")
+% - what are all the actions (in *.v files) from which those relationships arise
+
 The user does not have to mention explicitly the index $i$ when referring to
 the universe \Type$(i)$. One only writes \Type. The
 system itself generates for each instance of \Type\ a new
-- 
cgit v1.2.3