From 48431e5f7583f9fec3b776b07fac0f84f021a69e Mon Sep 17 00:00:00 2001
From: Matej Kosik <m4tej.kosik@gmail.com>
Date: Tue, 10 Nov 2015 14:55:39 +0100
Subject: PROPOSITION: the side-condition was made more specific.

---
 doc/refman/RefMan-cic.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

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}
-- 
cgit v1.2.3