diff options
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 39cf10843..e33d2259d 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 |