diff options
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 5002b905c7..08e962ebe2 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -94,13 +94,14 @@ Formally, we call {\Sort} the set of sorts which is defined by: \index{Prop@{\Prop}} \index{Set@{\Set}} -The sorts enjoy the following properties\footnote{In the Reference +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 + in the implementation.}% +: {\Prop:\Type$(1)$}, {\Set:\Type$(1)$} and {\Type$(i)$:\Type$(i+1)$}. The user does not have to mention explicitly the index $i$ when referring to |