From a391bf2fdd24b14a09493cbeebbe71fb83b32f6e Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 3 Sep 2019 18:36:23 +0200
Subject: Add missing index for From ... Require ...

---
 doc/sphinx/proof-engine/vernacular-commands.rst | 1 +
 1 file changed, 1 insertion(+)

diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index c391cc949d..2885d6dc33 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -627,6 +627,7 @@ file is a particular case of module called *library file*.
       as ``Export``.
 
    .. cmdv:: From @dirpath Require @qualid
+      :name: From ... Require ...
 
       This command acts as :cmd:`Require`, but picks
       any library whose absolute name is of the form :n:`@dirpath.@dirpath’.@qualid`
-- 
cgit v1.2.3