From 02be0f4e071c12800177eecdb067949dcce3b174 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Sat, 7 Nov 2015 18:06:41 +0100
Subject: COMMENT: question

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

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 8c8537cfb2..1a17f3f35f 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1764,7 +1764,9 @@ $\forall p_1:P_1,\ldots \forall p_r:P_r,
 \forall x_1:T_1, \ldots \forall x_r:T_r, (I_j~p_1\ldots 
 p_r~t_1\ldots  t_s)$ the recursive arguments will correspond to $T_i$ in
 which one of the $I_l$ occurs.
-
+% QUESTION: The last sentence above really fully make sense.
+%           Isn't some word missing?
+%           Maybe "if"?
 
 The main rules for being structurally smaller are the following:\\
 Given a variable $y$ of type an inductive
-- 
cgit v1.2.3