aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/addendum/universe-polymorphism.rst
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/addendum/universe-polymorphism.rst')
-rw-r--r--doc/sphinx/addendum/universe-polymorphism.rst2
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: