From 3f5f5cf07de6eb804e52da8213a0f1a75cb0cdbe Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 9 Nov 2020 16:34:39 +0100
Subject: Fix #5226: Add index entry for ::=.

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

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index ae3a252570..d9a0178cce 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1730,6 +1730,8 @@ Defining |Ltac| symbols
 
 |Ltac| toplevel definitions are made as follows:
 
+.. index:: ::=
+
 .. cmd:: Ltac @tacdef_body {* with @tacdef_body }
    :name: Ltac
 
-- 
cgit v1.2.3