From 0e7a91379a49be9874ce1669f3058fa0ae1194bb Mon Sep 17 00:00:00 2001
From: Matej Kosik <m4tej.kosik@gmail.com>
Date: Thu, 5 Nov 2015 19:33:33 +0100
Subject: COMMENT: question

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

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 9e11d66ab..6cd84cfc6 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1396,6 +1396,10 @@ $I$.
 \end{description}
 % QUESTION: What kind of value is represented by "x" in the "numerator"?
 %           There, "x" is unbound. Isn't it?
+%           The rule does not fully justify the following (plausible) argument:
+%
+%              http://matej-kosik.github.io/www/doc/coq/notes/26__allowed_elimination_sorts.html
+%
 % 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
-- 
cgit v1.2.3