diff options
| author | Théo Zimmermann | 2019-09-03 18:36:23 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-09-03 18:36:23 +0200 |
| commit | a391bf2fdd24b14a09493cbeebbe71fb83b32f6e (patch) | |
| tree | 70fab15621c1aa65bb2bf71debbabc2a6515a1da | |
| parent | bcf2dae1e39c6ff27c574a82c4451323a673b15f (diff) | |
Add missing index for From ... Require ...
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 1 |
1 files changed, 1 insertions, 0 deletions
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` |