diff options
| author | herbelin | 2001-10-17 16:53:50 +0000 |
|---|---|---|
| committer | herbelin | 2001-10-17 16:53:50 +0000 |
| commit | 8af1c9d641bd5456a8704ce195956ceb18c04e12 (patch) | |
| tree | a462f61da0e69c21deab0c08f957628ea0aa9855 | |
| parent | 2aee2d75aa422d0e535ca9696475c81d1c3340ba (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-x | doc/RefMan-cic.tex | 4 |
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} |
