aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/language')
-rw-r--r--doc/sphinx/language/gallina-extensions.rst1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 695dea222f..5308330820 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2244,6 +2244,7 @@ Printing universes
unspecified if `string` doesn’t end in ``.dot`` or ``.gv``.
.. cmdv:: Print Universes Subgraph(@names)
+ :name: Print Universes Subgraph
Prints the graph restricted to the requested names (adjusting
constraints to preserve the implied transitive constraints between