diff options
| -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 |