From 2aee2d75aa422d0e535ca9696475c81d1c3340ba Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 17 Oct 2001 16:48:10 +0000
Subject: Oubli de cas pour le sous-typage

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

diff --git a/doc/RefMan-cic.tex b/doc/RefMan-cic.tex
index 4fd12e0f2d..278d6d1a73 100755
--- a/doc/RefMan-cic.tex
+++ b/doc/RefMan-cic.tex
@@ -394,6 +394,8 @@ 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$, $\Prop\WTEGLECONV\Type(i)$,
+\item for any $i$, $\Set\WTEGLECONV\Type(i)$,
 \item if $\WTEGCONV{T}{U}$ and $\WTELECONV{\Gamma::(x:T)}{T'}{U'}$ then $\WTEGLECONV{(x:T)T'}{(x:U)U'}$.
 \end{enumerate}
 
-- 
cgit v1.2.3