diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index fe9f24c1f0..214e750bc1 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2285,7 +2285,7 @@ several times. See Section~\ref{Derive-Inversion}. equalities that {\tt inversion} introduces in the context of the goal corresponding to the $i^{th}$ constructor, if it exists, get their names from the list $p_{i1}$ \ldots $p_{in_i}$ in order. If - there are not enough names, {\tt induction} invents names for the + there are not enough names, {\tt inversion} invents names for the remaining variables to introduce. In case an equation splits into several equations (because {\tt inversion} applies {\tt injection} on the equalities it generates), the corresponding name $p_{ij}$ in |