diff options
| author | Emilio Jesus Gallego Arias | 2020-03-22 00:31:28 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-22 00:31:28 -0400 |
| commit | b048ecb6d874e1eb2e33c1fa3a15d3a508500285 (patch) | |
| tree | 5ab0bb6e675b72b39302ec581962f40e1eaec77d /doc/sphinx | |
| parent | ec4b889aa4e837bd82a7d0a059d0c967cde1ac46 (diff) | |
| parent | 3e98d9bd37d629f90e0a5702f6deb5b835815b5a (diff) | |
Merge PR #11851: Process command line load vernaculars before command line Goptions
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 5 |
1 files changed, 4 insertions, 1 deletions
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. |