diff options
Diffstat (limited to 'doc/refman/RefMan-com.tex')
| -rw-r--r-- | doc/refman/RefMan-com.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 5a3c91404..cf4774285 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -320,7 +320,7 @@ This tool can be used for several purposes. One is to check that a compiled library provided by a third-party has not been forged and that loading it cannot introduce inconsistencies.\footnote{Ill-formed non-logical information might for instance bind {\tt - Coq.Init.Logic.True} to short name {\tt False}, so apprently {\tt + Coq.Init.Logic.True} to short name {\tt False}, so apparently {\tt False} is inhabited, but using fully qualified names, {\tt Coq.Init.Logic.False} will always refer to the absurd proposition, what we guarantee is that there is no proof of this latter @@ -341,7 +341,7 @@ same meaning as for {\tt coqtop}. Extra options are: \item[{\tt -admit} $module$] \ Do not check $module$ and any of its dependencies, unless - explicitely required. + explicitly required. \item[{\tt -o}]\ At exit, print a summary about the context. List the names of all |