diff options
| -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 20893dc4e1..20ead7cceb 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -1034,8 +1034,8 @@ $\delta$-conversion (unfolding a constant is replacing it by its definition). {\tt Opaque} has also on effect on the conversion algorithm of {\Coq}, -telling to delay the unfolding of a constant as later as possible in -case {\Coq} has to check the conversion (see Section~\ref{conv-rules}) +telling it to delay the unfolding of a constant as mush as possible when +{\Coq} has to check the conversion (see Section~\ref{conv-rules}) of two distinct applied constants. The scope of {\tt Opaque} is limited to the current section, or |