From 12721b071cc76a463135ad74d572444b9d907b62 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 24 Apr 2018 11:59:51 +0200
Subject: Add missing index entries.

In particular, this backports e26b67436d12da63a11f0727c5b5895dfd03d249.
---
 doc/sphinx/proof-engine/ltac.rst | 1 +
 1 file changed, 1 insertion(+)

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

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 70d46e034a..1fc267488c 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -717,6 +717,7 @@ Local definitions
 Local definitions can be done as follows:
 
 .. tacn:: let @ident__1 := @expr__1 {* with @ident__i := @expr__i} in @expr
+   :name: let ... := ...
 
    each :n:`@expr__i` is evaluated to :n:`v__i`, then, :n:`@expr` is evaluated
    by substituting :n:`v__i` to each occurrence of :n:`@ident__i`, for
-- 
cgit v1.2.3