diff options
| author | Maxime Dénès | 2018-05-11 15:01:06 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-05-11 15:01:06 +0200 |
| commit | c3d719caf951e0c3716c85c8e3cf45f636d059eb (patch) | |
| tree | 288ccb6e7e7d6828ecdd4e46e322b41e7ad98e5a /doc/sphinx/addendum | |
| parent | 9368a1572f55dea66aa21edf140b84d883c5fccc (diff) | |
| parent | 762051a96fa149d8f83c77cc84cfb74545a8aab0 (diff) | |
Merge PR #7461: [sphinx] Improve the proof handling chapter.
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 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 <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: |