From d95fd157ac6600f4784de44ef558c4880aed624b Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 5 Nov 2015 15:25:50 +0100
Subject: COMMENT: question

---
 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 9e5f18f52a..f69b402783 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1246,6 +1246,11 @@ same as proving:
 $(\haslengthA~(\Nil~A)~\nO)$ and $\forall a:A, \forall l:\ListA, 
 (\haslengthA~l~(\length~l)) \ra
 (\haslengthA~(\cons~A~a~l)~(\nS~(\length~l)))$.
+% QUESTION: Wouldn't something like:
+%
+%             http://matej-kosik.github.io/www/doc/coq/notes/25__has_length.html
+%
+%           be more comprehensible?
 
 One conceptually simple way to do that, following the basic scheme
 proposed by Martin-L\"of in his Intuitionistic Type Theory, is to
-- 
cgit v1.2.3