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 bea0079a5c..34f55fa004 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1284,7 +1284,7 @@ In this expression, if $m$ eventually happens to evaluate to $(c_i~u_1\ldots u_{p_i})$ then the expression will behave as specified in its $i$-th branch and it will reduce to $f_i$ where the $x_{i1}$\ldots $x_{ip_i}$ are replaced -by the $u_1\ldots u_p$ according to the $\iota$-reduction. +by the $u_1\ldots u_{p_i}$ according to the $\iota$-reduction. Actually, for type-checking a \kw{match\ldots with\ldots end} expression we also need to know the predicate $P$ to be proved by case |