aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorMatej Kosik2015-11-05 10:09:01 +0100
committerHugo Herbelin2015-12-10 09:35:15 +0100
commit02b64e2d6c69996f95fa7bbcaf228e4848ad69f4 (patch)
treec7b3c4927798a24eecd1d83b48ff9a7cc36b7f12 /doc
parent90ae0897e80106194795e179d580da0d1118aaf2 (diff)
CLEANUP PROPOSITION: superfluous parentheses were removed
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 6f0e952ce6..a5832450ce 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1079,7 +1079,7 @@ The following typing rule is added to the theory.
1 \leq j \leq k
\end{array}
\right.}
-{E[] \vdash (I_j\,q_1\,\ldots\,q_r:\forall [p_{r+1}:P_{r+1};\ldots;p_{p}:P_{p}], (A_j)_{/s_j})}
+{E[] \vdash I_j\,q_1\,\ldots\,q_r:\forall [p_{r+1}:P_{r+1};\ldots;p_{p}:P_{p}], (A_j)_{/s_j}}
}
provided that the following side conditions hold: