diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-11-06 11:38:51 +0100 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:16 +0100 |
| commit | c372f60433da664431a394153eaf8dbcd6f15f07 (patch) | |
| tree | 9dcdb799a1b686670811bafdb22a2eac2269744a /doc/refman/RefMan-cic.tex | |
| parent | 0e7a91379a49be9874ce1669f3058fa0ae1194bb (diff) | |
CLEANUP: removing a superfluous index
Diffstat (limited to 'doc/refman/RefMan-cic.tex')
| -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 6cd84cfc6..23d86cbbc 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1524,7 +1524,7 @@ We define a new type \CI{c:C}{P} which represents the type of the branch corresponding to the $c:C$ constructor. \[ \begin{array}{ll} -\CI{c:(I_i~p_1\ldots p_r\ t_1 \ldots t_p)}{P} &\equiv (P~t_1\ldots ~t_p~c) \\[2mm] +\CI{c:(I~p_1\ldots p_r\ t_1 \ldots t_p)}{P} &\equiv (P~t_1\ldots ~t_p~c) \\[2mm] \CI{c:\forall~x:T,C}{P} &\equiv \forall~x:T,\CI{(c~x):C}{P} \end{array} \] |