From 2b7368ae43fefb6f151b7032b351f0da796f6cc3 Mon Sep 17 00:00:00 2001
From: Matej Kosik <m4tej.kosik@gmail.com>
Date: Wed, 4 Nov 2015 19:26:26 +0100
Subject: COMMENT: to do

---
 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 bacd62b77..ddd9f075e 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1024,6 +1024,7 @@ The same definition on \Set{} is not allowed and fails:
 Fail Inductive exSet (P:Set->Prop) : Set
   := exS_intro : forall X:Set, P X -> exSet P.
 \end{coq_example}
+% TODO: add the description of the 'Fail' command to the reference manual
 It is possible to declare the same inductive definition in the
 universe \Type. 
 The \texttt{exType} inductive definition has type  $(\Type_i \ra\Prop)\ra
-- 
cgit v1.2.3