aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Matej Kosik <m4tej.kosik@gmail.com>2015-11-04 19:23:40 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-12-10 09:35:14 +0100
commit1200468d82136ab3279bbe18da8fa0ba4e4cc8c4 (patch)
tree98ba1ae121bda86c42a0db28604f4a0958eb7664 /doc
parent70e705a47f435e1453d889177a426d89dacda07b (diff)
FIX: removing a reference to \Gamma, because it is undefined
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/RefMan-cic.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 101308470..51a0068b0 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -994,7 +994,7 @@ provided that the following side conditions hold:
\item $p$ is the number of parameters of \NInd{}{\Gamma_I}{\Gamma_C}
and $\Gamma_P$ is the context of parameters,
\item for $j=1\ldots k$ we have that $A_j$ is an arity of sort $s_j$ and $I_j
- \notin \Gamma \cup E$,
+ \notin E$,
\item for $i=1\ldots n$ we have that $C_i$ is a type of constructor of
$I_{q_i}$ which satisfies the positivity condition for $I_1 \ldots I_k$
and $c_i \notin \Gamma \cup E$.