From c5b3e7ff66e1675aaec7be5e0ee6772e88250991 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Fri, 30 Oct 2015 16:50:00 +0100
Subject: ENH: the concept of 'inductive declaration' was added to the 'Global
 Index'

---
 doc/refman/RefMan-cic.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 764f1189ba..7fd5b23039 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -519,7 +519,7 @@ reductions or any combination of those can also be defined.
 A (possibly mutual) inductive definition is specified by giving the
 names and types of the inductive types to be
 defined and the names and types of the constructors of the inductive types.
-An inductive declaration in the global environment can
+An {\em inductive declaration\index{declaration!inductive}} in the global environment can
 consequently be represented with two local contexts, one for the types
 one for the constructors.
 
-- 
cgit v1.2.3