diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-11-07 18:08:01 +0100 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:19 +0100 |
| commit | 0f97c5d4429e1f191b89125caa1ed652b0f19c79 (patch) | |
| tree | 026b552d7b1c426d8ba4ba58959b2bd8ea83b787 | |
| parent | 02be0f4e071c12800177eecdb067949dcce3b174 (diff) | |
TYPOGRAPHY
| -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 1a17f3f35..66111fa70 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1776,7 +1776,7 @@ where $\Gamma_I$ is $[I_1:A_1;\ldots;I_k:A_k]$, and $\Gamma_C$ is $[c_1:C_1;\ldots;c_n:C_n]$. The terms structurally smaller than $y$ are: \begin{itemize} -\item $(t~u), \lb x:u \mto t$ when $t$ is structurally smaller than $y$ . +\item $(t~u)$ and $\lb x:u \mto t$ when $t$ is structurally smaller than $y$. \item \Case{P}{c}{f_1\ldots f_n} when each $f_i$ is structurally smaller than $y$. \\ If $c$ is $y$ or is structurally smaller than $y$, its type is an inductive |