From f427a920e6fa31b145578c53d8853266cd215a26 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 5 Nov 2015 16:43:58 +0100
Subject: COMMENT: note

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

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 79756eb2fd..7c38a54ea6 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1396,6 +1396,7 @@ $I$.
 \end{description}
 % QUESTION: What kind of value is represented by "x" in the "numerator"?
 %           There, "x" is unbound. Isn't it?
+% NOTE: Above, "Set" is subsumed in "Type(0)" so, strictly speaking, we wouldn't need to mention in explicitely.
 
 The case of Inductive definitions of sort \Prop{} is a bit more
 complicated, because of our interpretation of this sort. The only
-- 
cgit v1.2.3