diff options
| -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` |