diff options
| author | Clément Pit-Claudel | 2019-09-05 02:48:36 +0200 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-09-05 02:48:36 +0200 |
| commit | 0f5f1b22db69fcb179dbcd656a7cb0e62b24dd6e (patch) | |
| tree | a577673dbe33d22c15e458b056aa71cdbacc8633 | |
| parent | a37b34723778679203af09f5f63476ea2204ceb0 (diff) | |
| parent | a391bf2fdd24b14a09493cbeebbe71fb83b32f6e (diff) | |
Merge PR #10730: Add missing index for From ... Require ...
Reviewed-by: cpitclaudel
| -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` |