diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-08 15:11:04 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-09 22:37:35 +0200 |
| commit | 1daa026d3e822bae54b771b526394dcd23389e0b (patch) | |
| tree | bf9c91ffb2a7ffe7daf429a635fa1fc65c32c7f0 /doc/sphinx/addendum | |
| parent | 372737ba74baa2af8ee798df1b2768a5d827a179 (diff) | |
[sphinx] Improvements around the Show commands, including missing indices and indentation.
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index e80cfb6bb..6e7ccba63 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -412,7 +412,7 @@ end of a definition or proof, we check that the only remaining universes are the ones declared. In the term and in general in proof mode, introduced universe names can be referred to in terms. Note that local universe names shadow global universe names. During a proof, one -can use :ref:`Show Universes <ShowUniverses>` to display the current context of universes. +can use :cmd:`Show Universes` to display the current context of universes. Definitions can also be instantiated explicitly, giving their full instance: |