From a3ee82e80083fff971e382f52d9295fda2210e2d Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 16 Apr 2018 21:26:55 +0200
Subject: [Sphinx] Clean-up indices

---
 doc/sphinx/addendum/program.rst | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'doc/sphinx/addendum/program.rst')

diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 1c3fdeb430..be30d1bc4a 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -151,7 +151,7 @@ Program Definition
    obligations. Once solved using the commands shown below, it binds the
    final |Coq| term to the name ``ident`` in the environment.
 
-   .. exn:: ident already exists
+   .. exn:: @ident already exists (Program Definition)
 
    .. cmdv:: Program Definition @ident : @type := @term
 
@@ -276,6 +276,7 @@ obligations (e.g. when defining mutually recursive blocks). The
 optional tactic is replaced by the default one if not specified.
 
 .. cmd:: {? Local|Global} Obligation Tactic := @tactic
+   :name: Obligation Tactic
 
    Sets the default obligation solving tactic applied to all obligations
    automatically, whether to solve them or when starting to prove one,
-- 
cgit v1.2.3