diff options
| author | charguer | 2019-12-12 10:48:50 +0100 |
|---|---|---|
| committer | charguer | 2019-12-12 13:57:18 +0100 |
| commit | 797eb524853e361f84c9c776024c142107f0c282 (patch) | |
| tree | 410a97bd2904fc790a6191cddb18de76ce77791f /doc/sphinx/practical-tools | |
| parent | 4a7a5c36802701d0e1b47956bb14cfc9cab99baa (diff) | |
Fix #11195 and add other improvements: try loading .vio (and not just .vo) if the .vos file is empty, rename -quick to -vio, dump empty .vos when producing .vio, dump empty .vos and .vok files when producing .vo from .vio.
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index d4a61425e1..ba43128bdc 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -253,6 +253,7 @@ and ``coqtop``, unless stated otherwise: :-h, --help: Print a short usage and exit. +.. _compiled-interfaces: Compiled interfaces (produced using ``-vos``) ---------------------------------------------- |