diff options
Diffstat (limited to 'doc/refman/RefMan-oth.tex')
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 739a89af4..4b2b8660c 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -967,8 +967,8 @@ the constants {\qualid$_1$} {\ldots} {\qualid$_n$} in tactics using $\delta$-conversion (unfolding a constant is replacing it by its definition). -{\tt Opaque} has also on effect on the conversion algorithm of {\Coq}, -telling it to delay the unfolding of a constant as mush as possible when +{\tt Opaque} has also an effect on the conversion algorithm of {\Coq}, +telling it to delay the unfolding of a constant as much as possible when {\Coq} has to check the conversion (see Section~\ref{conv-rules}) of two distinct applied constants. |