diff options
| author | Hugo Herbelin | 2014-09-07 13:36:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-07 13:52:47 +0200 |
| commit | f5c43cab2e974245ca3bba8d7fc082dffdd5c282 (patch) | |
| tree | 41c156f53319fef7f6bf4e4af1020b904a5eb730 /doc/refman | |
| parent | 9df412c81bd3a1729cb9d570c01ef2d255f23fb3 (diff) | |
Little fix in documentation of inversion.
Diffstat (limited to 'doc/refman')
| -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 |