diff options
author | Matej Kosik <m4tej.kosik@gmail.com> | 2015-10-29 11:54:58 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:09 +0100 |
commit | 5fbc2c5148fb6c4e77bf4c1c1a3854ed2fc0ed01 (patch) | |
tree | 296adaafe9d51d99e514f1e3238c67d968941328 /doc/refman | |
parent | 4be3e5df62d42daf38d48d24d8917eff4ba64928 (diff) |
ENH: a new anchor for an existing 'Global Index' keyword 'products' was added
Diffstat (limited to 'doc/refman')
-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 |