diff options
| author | Matej Kosik | 2015-10-29 09:50:11 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:07 +0100 |
| commit | b23331eb03f2640e85bd65277c15a4bcc692b90c (patch) | |
| tree | 95fb53b47afa9e91e4619570bf572ae5b1dce5a7 | |
| parent | 41061d0dc42afe19b520059f36a98d4ec870825f (diff) | |
ENH: citation
| -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$. |