From 61c780ad8138bfa768977d652c25741dad35d448 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 18 Apr 2019 14:26:39 +0200
Subject: First fixing pass, and experiment with dune-style PR number and
 author listing.

---
 doc/sphinx/language/gallina-extensions.rst | 1 +
 1 file changed, 1 insertion(+)

(limited to 'doc/sphinx/language')

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
-- 
cgit v1.2.3