From 4beb1ee596afaf4ab4ebea9a89bb3ade7bbbe13d Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 29 Oct 2015 17:32:36 +0100
Subject: COMMENT: question

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

(limited to 'doc/refman/RefMan-cic.tex')

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index db26568c5a..fe32cb7266 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -354,6 +354,7 @@ be derived from the following rules.
 well-typed without having $((\lb x:T\mto u)~t)$ well-typed (where
 $T$ is a type of $t$). This is because the value $t$ associated to $x$
 may be used in a conversion rule (see Section~\ref{conv-rules}).
+% QUESTION: I do not understand. How would that be possible?
 
 \section[Conversion rules]{Conversion rules\index{Conversion rules}
 \label{conv-rules}}
-- 
cgit v1.2.3

