From e9db7237481e529f796d603f98965ca01e439386 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 29 Oct 2015 09:52:53 +0100
Subject: CLEANUP PROPOSITION: Duplicate information was removed and replaced
 with a reference to the corresponding section.

---
 doc/refman/RefMan-cic.tex | 11 +----------
 1 file changed, 1 insertion(+), 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
-- 
cgit v1.2.3