From 42347ebd180f10b738f628bae904b5773a0150ac Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Mon, 2 Nov 2015 16:15:38 +0100
Subject: COMMENT: to do

---
 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 cc69355d4a..8f03cafd14 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -760,7 +760,9 @@ $\begin{array}{@{} l}
 
 \subsection{Well-formed inductive definitions}
 We cannot accept any inductive declaration because some of them lead
-to inconsistent systems. We restrict ourselves to definitions which
+to inconsistent systems.
+% TODO: The statement above deserves explanation.
+We restrict ourselves to definitions which
 satisfy a syntactic criterion of positivity. Before giving the formal
 rules, we need a few definitions:
 
-- 
cgit v1.2.3