From 5d32732cdf110e44a51cf6a23a8972f015e3fc88 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 5 Nov 2015 15:05:47 +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 1781d96fe5..9e5f18f52a 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1258,6 +1258,11 @@ But this operator is rather tedious to implement and use. We choose in
 this version of {\Coq} to factorize the operator for primitive recursion
 into two more primitive operations as was first suggested by Th. Coquand
 in~\cite{Coq92}.  One is the definition by pattern-matching. The second one is a definition by guarded fixpoints. 
+% QUESTION: Shouldn't we, instead, include a more straightforward argument:
+%
+%             http://matej-kosik.github.io/www/doc/coq/notes/24__match_and_fix.html
+%
+%           ?
 
 \subsubsection[The {\tt match\ldots with \ldots end} construction.]{The {\tt match\ldots with \ldots end} construction.\label{Caseexpr}
 \index{match@{\tt match\ldots with\ldots end}}}
-- 
cgit v1.2.3