Merge PR #11851: Process command line load vernaculars before command line Goptions

Reviewed-by: Zimmi48
Reviewed-by: ejgallego

2 files changed, 10 insertions, 1 deletions

diff --git a/doc/changelog/08-tools/11851-coqc-flags-fix.rst b/doc/changelog/08-tools/11851-coqc-flags-fix.rst
new file mode 100644
index 0000000000..a07e48d2d8
--- /dev/null
+++ b/doc/changelog/08-tools/11851-coqc-flags-fix.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+  The order in which the require/load flags `-l`, `-ri`, `-re`, `-rfrom`, etc.
+  and the option set flags `-set`, `-unset` are processed have been reversed.
+  In the new behavior, require/load flags are processed before option flags.
+  (`#11851 <https://github.com/coq/coq/pull/11851>`_,
+  by Lasse Blaauwbroek).
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 98d222e317..aa4b6edd7d 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -227,7 +227,10 @@ and ``coqtop``, unless stated otherwise:
    type of the option. For flags ``Option Name`` is equivalent to
    ``Option Name=true``. For instance ``-set "Universe Polymorphism"``
    will enable :flag:`Universe Polymorphism`. Note that the quotes are
-   shell syntax, Coq does not see them.
+   shell syntax, Coq does not see them. Flags are processed after initialization
+   of the document. This includes the `Prelude` if loaded and any libraries loaded
+   through the `-l`, `-lv`, `-r`, `-re`, `-ri`, `rfrom`, `-refrom` and `-rifrom`
+   options.
 :-unset *string*: As ``-set`` but used to disable options and flags.
 :-compat *version*: Attempt to maintain some backward-compatibility
   with a previous version.