diff options
| author | coqbot-app[bot] | 2021-03-08 20:22:04 +0000 |
|---|---|---|
| committer | GitHub | 2021-03-08 20:22:04 +0000 |
| commit | b55216ab3509f48e45aac035f1b799529d068f51 (patch) | |
| tree | 56deddf678f024309b084951b8f6997d7e303d3d /doc/sphinx/practical-tools | |
| parent | 4a0cf0f3fb4a1a57627f22897030771b2921ce85 (diff) | |
| parent | 0d33024ff79c38d52fde49e23d0e45d9c22eefbe (diff) | |
Merge PR #13707: Convert 2nd part of rewriting chapter to prodn
Reviewed-by: Zimmi48
Ack-by: JasonGross
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index a10312972e..464af37fde 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -499,7 +499,7 @@ wrong. In the current version, it does not modify the compiled libraries to mark them as successfully checked. Note that non-logical information is not checked. By logical -information, we mean the type and optional body associated with names. +information, we mean the type and optional :term:`body` associated with names. It excludes for instance anything related to the concrete syntax of objects (customized syntax rules, association between short and long names), implicit arguments, etc. @@ -521,7 +521,7 @@ relative paths in object files ``-Q`` and ``-R`` have exactly the same meaning. :-admit *module*: Do not check *module* and any of its dependencies, unless explicitly required. :-o: At exit, print a summary about the context. List the names of all - assumptions and variables (constants without body). + assumptions and variables (constants without a :term:`body`). :-silent: Do not write progress information to the standard output. Environment variable ``$COQLIB`` can be set to override the location of |