diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-11-05 14:09:54 +0100 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:15 +0100 |
| commit | cd60731dae4e7627588027fe1c1aa60a2ae44594 (patch) | |
| tree | ea34807535fb5d20536c59a45f4c616dde5eb3cb | |
| parent | 3600dbb0546a910cda3996b5226bd7a6800d3040 (diff) | |
FIX: removing references to Γ which is not defined in a given context
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 001ce54f8..37ca23417 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1075,7 +1075,7 @@ The following typing rule is added to the theory. {\left\{\begin{array}{l} \Ind{}{p}{\Gamma_I}{\Gamma_C} \in E\\ (E[] \vdash q_l : P'_l)_{l=1\ldots r}\\ -(\WTEGLECONV{P'_l}{\subst{P_l}{p_u}{q_u}_{u=1\ldots l-1}})_{l=1\ldots r}\\ +(\WTELECONV{}{P'_l}{\subst{P_l}{p_u}{q_u}_{u=1\ldots l-1}})_{l=1\ldots r}\\ 1 \leq j \leq k \end{array} \right.} @@ -1087,7 +1087,7 @@ provided that the following side conditions hold: \begin{itemize} \item $\Gamma_{P'}$ is the context obtained from $\Gamma_P$ by replacing each $P_l$ that is an arity with $P'_l$ for $1\leq l \leq r$ (notice that -$P_l$ arity implies $P'_l$ arity since $\WTEGLECONV{P'_l}{ \subst{P_l}{p_u}{q_u}_{u=1\ldots l-1}}$); +$P_l$ arity implies $P'_l$ arity since $\WTELECONV{}{P'_l}{ \subst{P_l}{p_u}{q_u}_{u=1\ldots l-1}}$); \item there are sorts $s_i$, for $1 \leq i \leq k$ such that, for $\Gamma_{I'} = [I_1:\forall \Gamma_{P'},(A_1)_{/s_1};\ldots;I_k:\forall \Gamma_{P'},(A_k)_{/s_k}]$ |