aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2001-10-17 16:53:50 +0000
committerherbelin2001-10-17 16:53:50 +0000
commit8af1c9d641bd5456a8704ce195956ceb18c04e12 (patch)
treea462f61da0e69c21deab0c08f957628ea0aa9855
parent2aee2d75aa422d0e535ca9696475c81d1c3340ba (diff)
Oubli de cas pour le sous-typage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8252 85f007b7-540e-0410-9357-904b9bb8a0f7
-rwxr-xr-xdoc/RefMan-cic.tex4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/RefMan-cic.tex b/doc/RefMan-cic.tex
index 278d6d1a73..08cfe30efd 100755
--- a/doc/RefMan-cic.tex
+++ b/doc/RefMan-cic.tex
@@ -394,8 +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 for any $i$, $\WTEGLECONV{\Prop}{\Type(i)}$,
+\item for any $i$, $\WTEGLECONV{\Set}{\Type(i)}$,
\item if $\WTEGCONV{T}{U}$ and $\WTELECONV{\Gamma::(x:T)}{T'}{U'}$ then $\WTEGLECONV{(x:T)T'}{(x:U)U'}$.
\end{enumerate}