diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index e507f1215de09a5fc47eba5602e1e9ffc44483da..d5285609c6715589e117913281f6f5672e487cfd 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -306,7 +306,7 @@ $$\TACTIC{\Delta\models\,G}{%
 \end{array}} $$
 
 \paragraph{Definition} Unfold predicate and logic function definition\\
-The user simply select a term $f(e_1,\ldots,e_n)$ or a predicate $P(e_1,\ldots,e_n)$ which is replaced by its definition, when available.
+The user simply select a term $f(e_1,\ldots,e_n)$ or a predicate $P(e_1,\ldots,e_n)$ which is replaced with its definition, when available.
 
 \paragraph{Filter} Erase Hypotheses \\
 The tactic is always applicable. It removes hypotheses from the goal on a variable used basis. When variables are compounds (record and arrays) a finer heuristics is used to detect which parts of the variable is relevant. A transitive closure of dependencies is also used. However, it is always possible that too many hypotheses are removed.