From 27d6686f399f40904ff6005a84677907d53c5bbf Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Wed, 1 Apr 2020 13:18:03 -0700 Subject: Convert Ltac chapter to prodn --- doc/sphinx/practical-tools/coq-commands.rst | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'doc/sphinx/practical-tools') 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 ` - :n:`@dirpath` :cmd:`Require ` :n:`@qualid`. + This is equivalent to running :cmd:`From ` + :n:`@dirpath` :cmd:`Require ` :n:`@qualid`. See the :ref:`note above ` 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 ` :n:`@dirpath` - :cmd:`Require Import ` :n:`@qualid`. See the + equivalent to running :cmd:`From ` :n:`@dirpath` + :cmd:`Require Import ` :n:`@qualid`. See the :ref:`note above ` 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 ` - :n:`@dirpath` :cmd:`Require Export ` :n:`@qualid`. + This is equivalent to running :cmd:`From ` + :n:`@dirpath` :cmd:`Require Export ` :n:`@qualid`. See the :ref:`note above ` regarding the order of command-line options. :-batch: Exit just after argument parsing. Available for ``coqtop`` only. -- cgit v1.2.3