diff options
| author | Théo Zimmermann | 2020-06-09 12:42:36 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-06-09 12:42:36 +0200 |
| commit | 4642ce1c5924cbfa93d6a8e96cf86839e614623b (patch) | |
| tree | 4993e6de8cd61b655733feb5efce2e9c85f57cef /doc/sphinx/practical-tools | |
| parent | 10e126ba3232dac847ce5c7a62ff97d9ddfaa620 (diff) | |
| parent | 27d6686f399f40904ff6005a84677907d53c5bbf (diff) | |
Merge PR #12103: Convert Ltac chapter to prodn
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index d4ceffac9f..058b8ccd5c 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -177,8 +177,8 @@ and ``coqtop``, unless stated otherwise: the command-line. :-rfrom *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid`. - This is equivalent to running :cmd:`From <From ... Require>` - :n:`@dirpath` :cmd:`Require <From ... Require>` :n:`@qualid`. + This is equivalent to running :cmd:`From <From … Require>` + :n:`@dirpath` :cmd:`Require <From … Require>` :n:`@qualid`. See the :ref:`note above <interleave-command-line>` regarding the order of command-line options. :-ri *qualid*, -require-import *qualid*: Load |Coq| compiled library :n:`@qualid` and import it. @@ -191,14 +191,14 @@ and ``coqtop``, unless stated otherwise: of command-line options. :-rifrom *dirpath* *qualid*, -require-import-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and import it. This is - equivalent to running :cmd:`From <From ... Require>` :n:`@dirpath` - :cmd:`Require Import <From ... Require>` :n:`@qualid`. See the + equivalent to running :cmd:`From <From … Require>` :n:`@dirpath` + :cmd:`Require Import <From … Require>` :n:`@qualid`. See the :ref:`note above <interleave-command-line>` regarding the order of command-line options. :-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it. - This is equivalent to running :cmd:`From <From ... Require>` - :n:`@dirpath` :cmd:`Require Export <From ... Require>` :n:`@qualid`. + This is equivalent to running :cmd:`From <From … Require>` + :n:`@dirpath` :cmd:`Require Export <From … Require>` :n:`@qualid`. See the :ref:`note above <interleave-command-line>` regarding the order of command-line options. :-batch: Exit just after argument parsing. Available for ``coqtop`` only. |