From 55fe005b2141a69ffd9589568f8b854075174d56 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Sat, 7 Nov 2015 18:49:37 +0100
Subject: COMMENT: question

---
 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 736affe940..29e4f256bb 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1858,6 +1858,7 @@ reflexivity.
 \begin{coq_eval}
 Abort.
 \end{coq_eval}
+% QUESTION: What are we trying to say with the above examples?
 
 % La disparition de Program devrait rendre la construction Match obsolete
 % \subsubsection{The {\tt Match \ldots with \ldots end} expression}
-- 
cgit v1.2.3