diff options
| author | Hugo Herbelin | 2015-10-23 17:51:06 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:07 +0100 |
| commit | 5330263aaccb3ba9e7fcb8fada0737491fd99645 (patch) | |
| tree | 76a97360a8b9a44d382d99e9e986f5a9e828bb95 | |
| parent | 899b701462fa056a22f997ae22c5ef7c1d247673 (diff) | |
Removing note on shifting the hierarchy by 1 in 8.4, which makes things more complicated than needed.
| -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 |