diff options
| author | Emilio Jesus Gallego Arias | 2020-04-08 01:48:18 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-08 01:48:18 -0400 |
| commit | b26d1f477990d88e235ffda0f23f494456ce5862 (patch) | |
| tree | 948efae33b55943290a7d6bfe4976eba85caf4c4 /doc | |
| parent | 847a42618bc0ff267e5912c6c8f8365f29b158b4 (diff) | |
| parent | 8ac8f5aa327ca8de66e90bb33d1950d9a4749177 (diff) | |
Merge PR #12005: Remove deprecated coqtop options
Ack-by: SkySkimmer
Ack-by: ejgallego
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 3 |
2 files changed, 7 insertions, 1 deletions
diff --git a/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst b/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst new file mode 100644 index 0000000000..affb685fcb --- /dev/null +++ b/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst @@ -0,0 +1,5 @@ +- **Removed:** + Confusingly-named and deprecated since 8.11 `-require` option. + Use the equivalent `-require-import` instead + (`#12005 <https://github.com/coq/coq/pull/12005>`_, + by Théo Zimmermann). diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index aa4b6edd7d..958d295219 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -164,6 +164,8 @@ and ``coqtop``, unless stated otherwise: it is executed. :-load-vernac-object *qualid*: Load |Coq| compiled library :n:`@qualid`. This is equivalent to running :cmd:`Require` :n:`qualid`. +:-rfrom *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid`. + This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`. :-ri *qualid*, -require-import *qualid*: Load |Coq| compiled library :n:`@qualid` and import it. This is equivalent to running :cmd:`Require Import` :n:`@qualid`. :-re *qualid*, -require-export *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it. @@ -172,7 +174,6 @@ and ``coqtop``, unless stated otherwise: This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`. :-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it. This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Export` :n:`@qualid`. -:-require *qualid*: Deprecated; use ``-ri`` *qualid*. :-batch: Exit just after argument parsing. Available for ``coqtop`` only. :-compile *file.v*: Deprecated; use ``coqc`` instead. Compile file *file.v* into *file.vo*. This option implies -batch (exit just after argument parsing). It is available only |