diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-11-10 14:55:39 +0100 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:19 +0100 |
| commit | 48431e5f7583f9fec3b776b07fac0f84f021a69e (patch) | |
| tree | 37f277830d0f8356195f877d7aab278f2ec7c213 /doc | |
| parent | e90a1be62b9d26b1982e48d7bbd2a73b5bc54b0a (diff) | |
PROPOSITION: the side-condition was made more specific.
Diffstat (limited to 'doc')
| -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 dd194d4eb..dd9284e60 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} |