diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -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 4f4c88d01..93ef9233a 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2947,7 +2947,7 @@ command as follows: \item A constant can be marked to be never unfolded by {\tt simpl}: \begin{coq_example*} -Arguments minus x y : simpl never +Arguments minus x y : simpl never. \end{coq_example*} After that command an expression like {\tt (minus (S x) y)} is left untouched by the {\tt simpl} tactic. |