From 73563c2ff4a4214a3b6aa2333c3f413086500a0e Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 2 Apr 2020 15:37:24 +0200 Subject: Remove deprecated -require option. This option is confusing because it does Require Import, not Require. It was deprecated in 8.11. We remove it in 8.12 in order to reintroduce it in 8.13 as a replacement for -load-vernac-object, which is the option that does Require without Import as of today. --- doc/sphinx/practical-tools/coq-commands.rst | 1 - 1 file changed, 1 deletion(-) (limited to 'doc') diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index aa4b6edd7d..85ed0112ae 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -172,7 +172,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 -- cgit v1.2.3 From cb1e693d84013b56c9a8e6154e101245c950f85f Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 2 Apr 2020 15:59:53 +0200 Subject: Add changelog entry for #12005. --- doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst (limited to 'doc') 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..e38f2f337a --- /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 `-require-import` instead + (`#12005 `_, + by Théo Zimmermann). -- cgit v1.2.3 From e3e1133fe5685213460a6cc3f761283815223e3d Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 2 Apr 2020 22:23:02 +0200 Subject: Document -rfrom option in reference manual. So far it was only documented in coqtop --help. --- doc/sphinx/practical-tools/coq-commands.rst | 2 ++ 1 file changed, 2 insertions(+) (limited to 'doc') diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 85ed0112ae..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. -- cgit v1.2.3 From 8ac8f5aa327ca8de66e90bb33d1950d9a4749177 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 3 Apr 2020 10:27:15 +0200 Subject: Update doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst Co-Authored-By: Gaëtan Gilbert --- doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst b/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst index e38f2f337a..affb685fcb 100644 --- a/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst +++ b/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst @@ -1,5 +1,5 @@ - **Removed:** Confusingly-named and deprecated since 8.11 `-require` option. - Use `-require-import` instead + Use the equivalent `-require-import` instead (`#12005 `_, by Théo Zimmermann). -- cgit v1.2.3