From 1daa026d3e822bae54b771b526394dcd23389e0b Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 8 May 2018 15:11:04 +0200 Subject: [sphinx] Improvements around the Show commands, including missing indices and indentation. --- doc/sphinx/addendum/universe-polymorphism.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/sphinx/addendum') diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index e80cfb6bb5..6e7ccba63c 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 ` 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: -- cgit v1.2.3