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 c481b3adba..2c0f155388 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -44,7 +44,7 @@ function types over these data types. {\Prop} and {\Set} themselves can be manipulated as ordinary terms. Consequently they also have a type. Because assuming simply -that {\Set} has type {\Set} leads to an inconsistent theory, the +that {\Set} has type {\Set} leads to an inconsistent theory~\cite{Coq86}, the language of {\CIC} has infinitely many sorts. There are, in addition to {\Set} and {\Prop} a hierarchy of universes {\Type$(i)$} for any integer $i$. |