diff options
| author | Hugo Herbelin | 2014-06-21 14:44:25 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-06-21 16:21:19 +0200 |
| commit | 2f2b62e202c4585e2b23e1050c7a67f9ef01ad27 (patch) | |
| tree | a5265805f71e9104fc853373cefaf0c37d98d9a8 | |
| parent | 7d7b5eb7f6ae9c13415d2de4c3f96fc39e67b0c8 (diff) | |
Fixing grammar in doc of Opaque as proposed by Jason (#3389).
| -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 |