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}