diff options
| author | Matej Kosik | 2015-10-29 09:52:53 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:07 +0100 |
| commit | e9db7237481e529f796d603f98965ca01e439386 (patch) | |
| tree | 29c4dbf66af1d84dd9ab31fa63e3c7c9007490f0 | |
| parent | b23331eb03f2640e85bd65277c15a4bcc692b90c (diff) | |
CLEANUP PROPOSITION: Duplicate information was removed and replaced with a reference to the corresponding section.
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 2c0f155388..834c8273a5 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -60,16 +60,7 @@ Formally, we call {\Sort} the set of sorts which is defined by: \index{Type@{\Type}} \index{Prop@{\Prop}} \index{Set@{\Set}} - -The sorts enjoy the following properties%\footnote{In the Reference - %% Manual of versions of {\Coq} prior to 8.4, the level of {\Type} typing - %% {\Prop} and {\Set} was numbered $0$. From {\Coq} 8.4, it started to be - %% numbered $1$ so as to be able to leave room for re-interpreting - %% {\Set} in the hierarchy as {\Type$(0)$}. This change also put the - %% reference manual in accordance with the internal conventions adopted - %% in the implementation.} -: {\Prop:\Type$(1)$}, {\Set:\Type$(1)$} and -{\Type$(i)$:\Type$(i+1)$}. +Their properties are defined in Section~\ref{subtyping-rules}. The user does not have to mention explicitly the index $i$ when referring to the universe \Type$(i)$. One only writes \Type. The |