diff options
| author | Matej Kosik | 2015-10-29 17:33:54 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:10 +0100 |
| commit | c56035c2850fe09fc5ef6389e58de28109ad5a93 (patch) | |
| tree | 86b41d89b62f0749166f87a8ec4187400875bdb6 | |
| parent | 4beb1ee596afaf4ab4ebea9a89bb3ade7bbbe13d (diff) | |
TYPOGRAPHY: getting rid of an extra space
| -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 fe32cb7266..a008bd19a5 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -411,7 +411,7 @@ called $\zeta$-reduction and shows as follows. $$\WTEGRED{\kw{let}~x:=u~\kw{in}~t}{\triangleright_{\zeta}}{\subst{t}{x}{u}}$$ -\paragraph{$\eta$-conversion. +\paragraph{$\eta$-conversion.% \label{eta} \index{eta-conversion@$\eta$-conversion} %\index{eta-reduction@$\eta$-reduction} |