diff options
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index dd194d4eb9..dd9284e606 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1055,7 +1055,7 @@ $P_l$ arity implies $P'_l$ arity since $\WTELECONV{}{P'_l}{ \subst{P_l}{p_u}{q_u $\Gamma_{I'} = [I_1:\forall \Gamma_{P'},(A_1)_{/s_1};\ldots;I_k:\forall \Gamma_{P'},(A_k)_{/s_k}]$ we have $(\WTE{\Gamma_{I'};\Gamma_{P'}}{C_i}{s_{q_i}})_{i=1\ldots n}$; -\item the sorts are such that all eliminations, to {\Prop}, {\Set} and +\item the sorts $s_i$ are such that all eliminations, to {\Prop}, {\Set} and $\Type(j)$, are allowed (see Section~\ref{allowedeleminationofsorts}). \end{itemize} \end{description} |