From 1ed9605dd20aedeeec01f308e24a69663808dcc6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 8 May 2012 10:13:30 +0000
Subject: Ref. man., ch. CIC: clarifying the redundancy coming from having both
 Prop <= Type(i) and the conjunction of Prop <= Set and Set <= Type(i).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15283 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-cic.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 901969703f..0b454a8fcd 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -420,9 +420,9 @@ convertibility into an order inductively defined by:
 \begin{enumerate}
 \item if $\WTEGCONV{t}{u}$ then $\WTEGLECONV{t}{u}$,
 \item if $i \leq j$ then $\WTEGLECONV{\Type(i)}{\Type(j)}$,
-\item for any $i$, $\WTEGLECONV{\Prop}{\Type(i)}$,
 \item for any $i$, $\WTEGLECONV{\Set}{\Type(i)}$,
-\item $\WTEGLECONV{\Prop}{\Set}$,
+\item $\WTEGLECONV{\Prop}{\Set}$, hence, by transitivity,
+  $\WTEGLECONV{\Prop}{\Type(i)}$, for any $i$
 \item if $\WTEGCONV{T}{U}$ and $\WTELECONV{\Gamma::(x:T)}{T'}{U'}$ then $\WTEGLECONV{\forall~x:T,T'}{\forall~x:U,U'}$.
 \end{enumerate}
 
-- 
cgit v1.2.3