From 5fbc2c5148fb6c4e77bf4c1c1a3854ed2fc0ed01 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 29 Oct 2015 11:54:58 +0100
Subject: ENH: a new anchor for an existing 'Global Index' keyword 'products'
 was added

---
 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 39cf108439..e33d2259d3 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -152,7 +152,7 @@ More precisely the language of the {\em Calculus of Inductive
 \item constants, hereafter ranged over by letters $c$, $d$, etc.,  are terms.
 %\item constructors, hereafter ranged over by letter $C$, are terms.
 %\item inductive types, hereafter ranged over by letter $I$, are terms.
-\item if $x$ is a variable and $T$, $U$ are terms then $\forall~x:T,U$
+\item\index{products} if $x$ is a variable and $T$, $U$ are terms then $\forall~x:T,U$
   ($\kw{forall}~x:T,~U$ in \Coq{} concrete syntax) is a term. If $x$
   occurs in $U$, $\forall~x:T,U$ reads as {\it ``for all x of type T,
     U''}. As $U$ depends on $x$, one says that $\forall~x:T,U$ is a
-- 
cgit v1.2.3