From f5c43cab2e974245ca3bba8d7fc082dffdd5c282 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 7 Sep 2014 13:36:40 +0200
Subject: Little fix in documentation of inversion.

---
 doc/refman/RefMan-tac.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3