From 482594f4b2c8360a75acf59d756601e3ac4a0046 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 26 Apr 2018 13:15:55 +0200
Subject: [sphinx] Add indices for only, all and par.

---
 doc/sphinx/proof-engine/ltac.rst | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index d81048f075..c5ee724caf 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -245,9 +245,10 @@ focused goals with:
    :name: ... : ... (goal selector)
 
    We can also use selectors as a tactical, which allows to use them nested
-   in a tactic expression, by using the keyword ``only``:
+   in a tactic expression, by using the keyword :tacn:`only`:
 
    .. tacv:: only selector : expr
+      :name: only ... : ...
 
       When selecting several goals, the tactic expr is applied globally to all
       selected goals.
@@ -268,6 +269,7 @@ focused goals with:
       for ``n-n`` when specifying multiple ranges.
 
    .. tacv:: all: @expr
+      :name: all: ...
 
       In this variant, :n:`@expr` is applied to all focused goals. ``all:`` can only
       be used at the toplevel of a tactic expression.
@@ -279,6 +281,7 @@ focused goals with:
       used at the toplevel of a tactic expression.
 
    .. tacv:: par: @expr
+      :name: par: ...
 
       In this variant, :n:`@expr` is applied to all focused goals in parallel.
       The number of workers can be controlled via the command line option
-- 
cgit v1.2.3