diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-29 15:44:39 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-29 15:44:39 +0000 |
| commit | 06bde04218ed4e616514534023cfb6f2599398c5 (patch) | |
| tree | 8eac87c71173fe5a1172b764dfae06a270692ac8 | |
| parent | 61a782cfa0eb5399f59933de6b8244295f9ec6e7 (diff) | |
Fix minor spelling error
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12300 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/refman/RefMan-com.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 1bd3d148e..5a3c91404 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -308,7 +308,7 @@ of all these libraries is then type-checked. The effect of {\tt and with positive exit code if an error has been found. Error messages are not deemed to help the user understand what is wrong. In the current version, it does not modify the compiled libraries to mark -them as succesfully checked. +them as successfully checked. Note that non-logical information is not checked. By logical information, we mean the type and optional body associated to names. |