diff options
| author | Hugo Herbelin | 2019-05-27 17:30:19 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-06-08 12:02:25 +0200 |
| commit | 08a32f04b77b29ad17db75f7ba98c122c31b96aa (patch) | |
| tree | 977aad6b764a7bbdb7d364ea2b8c0220f84d41d2 | |
| parent | 5261067a906c190c20d571086692dfb04bc4d0de (diff) | |
Mini fix documentation coqtop in passing.
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 3729dcd974..48d5f4075e 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -200,7 +200,7 @@ and ``coqtop``, unless stated otherwise: :-emacs, -ide-slave: Start a special toplevel to communicate with a specific IDE. :-impredicative-set: Change the logical theory of |Coq| by declaring the - sort Set impredicative. + sort :g:`Set` impredicative. .. warning:: |