diff options
| author | Jim Fehrle | 2020-04-01 13:18:03 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-06-08 16:50:53 -0700 |
| commit | 27d6686f399f40904ff6005a84677907d53c5bbf (patch) | |
| tree | 5a27b8acdab8ce79b9a7d10685c8979cda82416b /doc/sphinx/practical-tools | |
| parent | 6a76e4394876cb08b02d8e7ea185049147f9cd2b (diff) | |
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. |