Fix some broken Coq scripts in the documentation.

1 files changed, 3 insertions, 3 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 8f9ba1ec60..cc262708ab 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3129,7 +3129,7 @@ follows: \comindex{Arguments}
 A constant can be marked to be never unfolded by \texttt{cbn} or
 \texttt{simpl}:
 \begin{coq_example*}
-Arguments minus x y : simpl never.
+Arguments minus n m : simpl never.
 \end{coq_example*}
 After that command an expression like \texttt{(minus (S x) y)} is left
 untouched by the tactics \texttt{cbn} and \texttt{simpl}.
@@ -3156,7 +3156,7 @@ A constant can be marked to be unfolded only if an entire set of arguments
 evaluates to a constructor. The {\tt !} symbol can be used to mark such
 arguments.
 \begin{coq_example*}
-Arguments minus !x !y.
+Arguments minus !n !m.
 \end{coq_example*}
 After that command, the expression {\tt (minus (S x) y)} is left untouched by
 {\tt simpl}, while {\tt (minus (S x) (S y))} is reduced to {\tt (minus x y)}.
@@ -3164,7 +3164,7 @@ After that command, the expression {\tt (minus (S x) y)} is left untouched by
 A special heuristic to determine if a constant has to be unfolded can be
 activated with the following command:
 \begin{coq_example*}
-Arguments minus x y : simpl nomatch.
+Arguments minus n m : simpl nomatch.
 \end{coq_example*}
 The heuristic avoids to perform a simplification step that would
 expose a {\tt match} construct in head position. For example the