Fix conflicts with latest master.

4 files changed, 112 insertions, 24 deletions

diff --git a/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst b/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst
new file mode 100644
index 0000000000..e1fcfb78c4
--- /dev/null
+++ b/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  Abbreviations support arguments occurring both in term and binder position
+  (`#8808 <https://github.com/coq/coq/pull/8808>`_,
+  by Hugo Herbelin).
diff --git a/doc/changelog/08-tools/11851-coqc-flags-fix.rst b/doc/changelog/08-tools/11851-coqc-flags-fix.rst
index a07e48d2d8..ff736641b4 100644
--- a/doc/changelog/08-tools/11851-coqc-flags-fix.rst
+++ b/doc/changelog/08-tools/11851-coqc-flags-fix.rst
@@ -1,6 +1,9 @@
 - **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>`_,
+  The order in which the require flags `-ri`, `-re`, `-rfrom`, etc.
+  and the option flags `-set`, `-unset` are given now matters.  In
+  particular, it is now possible to interleave the loading of plugins
+  and the setting of options by choosing the right order for these
+  flags.  The load flags `-l` and `-lv` are still processed afterward
+  for now (`#11851 <https://github.com/coq/coq/pull/11851>`_ and
+  `#12097 <https://github.com/coq/coq/pull/12097>`_,
   by Lasse Blaauwbroek).
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 58fd49c390..d4ceffac9f 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -151,7 +151,7 @@ and ``coqtop``, unless stated otherwise:
   while processing options such as -R and -Q. By default, only the
   conventional version control management directories named CVS
   and_darcs are excluded.
-:-nois: Start from an empty state instead of loading the Init.Prelude
+:-nois, -noinit: Start from an empty state instead of loading the `Init.Prelude`
   module.
 :-init-file *file*: Load *file* as the resource file instead of
   loading the default resource file from the standard configuration
@@ -163,26 +163,53 @@ and ``coqtop``, unless stated otherwise:
   |Coq| script from *file.v*. Write its contents to the standard output as
   it is executed.
 :-load-vernac-object *qualid*: Load |Coq| compiled library :n:`@qualid`. This
-  is equivalent to running :cmd:`Require` :n:`qualid`.
+  is equivalent to running :cmd:`Require` :n:`@qualid`.
+
+  .. _interleave-command-line:
+
+  .. note::
+
+     Note that the relative order of this command-line option and its
+     variants (`-rfrom`, `-ri`, `-re`, etc.)  and of the `-set` and
+     `-unset` options matters since the various :cmd:`Require`,
+     :cmd:`Require Import`, :cmd:`Require Export`, :cmd:`Set` and
+     :cmd:`Unset` commands will be executed in the order specified on
+     the command-line.
+
 :-rfrom *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid`.
-  This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`.
+  This is equivalent to running :cmd:`From <From ... Require>`
+  :n:`@dirpath` :cmd:`Require <From ... Require>` :n:`@qualid`.
+  See the :ref:`note above <interleave-command-line>` regarding the order
+  of command-line options.
 :-ri *qualid*, -require-import *qualid*: Load |Coq| compiled library :n:`@qualid` and import it.
   This is equivalent to running :cmd:`Require Import` :n:`@qualid`.
+  See the :ref:`note above <interleave-command-line>` regarding the order
+  of command-line options.
 :-re *qualid*, -require-export *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it.
   This is equivalent to running :cmd:`Require Export` :n:`@qualid`.
-:-rifrom *dirpath* *qualid*, -require-import-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and import it.
-  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`.
+  See the :ref:`note above <interleave-command-line>` regarding the order
+  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 <From ... Require>` :n:`@dirpath`
+  :cmd:`Require Import <From ... Require>` :n:`@qualid`.  See the
+  :ref:`note above <interleave-command-line>` 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 <From ... Require>`
+  :n:`@dirpath` :cmd:`Require Export <From ... Require>` :n:`@qualid`.
+  See the :ref:`note above <interleave-command-line>` regarding the
+  order of command-line options.
 :-batch: Exit just after argument parsing. Available for ``coqtop`` only.
 :-verbose: Output the content of the input file as it is compiled.
   This option is available for ``coqc`` only.
 :-vos: Indicate |Coq| to skip the processing of opaque proofs
-  (i.e., proofs ending with ``Qed`` or ``Admitted``), output a ``.vos`` files
+  (i.e., proofs ending with :cmd:`Qed` or :cmd:`Admitted`), output a ``.vos`` files
   instead of a ``.vo`` file, and to load ``.vos`` files instead of ``.vo`` files
-  when interpreting ``Require`` commands.
+  when interpreting :cmd:`Require` commands.
 :-vok: Indicate |Coq| to check a file completely, to load ``.vos`` files instead
-  of ``.vo`` files when interpreting ``Require`` commands, and to output an empty
+  of ``.vo`` files when interpreting :cmd:`Require` commands, and to output an empty
   ``.vok`` files upon success instead of writing a ``.vo`` file.
 :-w (all|none|w₁,…,wₙ): Configure the display of warnings. This
   option expects all, none or a comma-separated list of warning names or
@@ -192,7 +219,7 @@ and ``coqtop``, unless stated otherwise:
   the output channel supports ANSI escape sequences.
 :-diffs (on|off|removed): *Coqtop only*.  Controls highlighting of differences
   between proof steps.  ``on`` highlights added tokens, ``removed`` highlights both added and
-  removed tokens.  Requires that ``–color`` is enabled.  (see Section
+  removed tokens.  Requires that ``-color`` is enabled.  (see Section
   :ref:`showing_diffs`).
 :-beautify: Pretty-print each command to *file.beautified* when
   compiling *file.v*, in order to get old-fashioned
@@ -218,17 +245,25 @@ and ``coqtop``, unless stated otherwise:
   changes in the auto-generated name scheme. The options are provided to
   facilitate tracking down problems.
 :-set *string*: Enable flags and set options. *string* should be
-   ``Option Name=value``, the value is interpreted according to the
-   type of the option. For flags ``Option Name`` is equivalent to
-   ``Option Name=true``. For instance ``-set "Universe Polymorphism"``
+   :n:`@setting_name=value`, the value is interpreted according to the
+   type of the option. For flags :n:`@setting_name` is equivalent to
+   :n:`@setting_name=true`. For instance ``-set "Universe Polymorphism"``
    will enable :flag:`Universe Polymorphism`. Note that the quotes are
-   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.
+   shell syntax, Coq does not see them.
+   See the :ref:`note above <interleave-command-line>` regarding the order
+   of command-line options.
 :-unset *string*: As ``-set`` but used to disable options and flags.
-:-compat *version*: Attempt to maintain some backward-compatibility
-  with a previous version.
+  *string* must be :n:`"@setting_name"`.
+  See the :ref:`note above <interleave-command-line>` regarding the order
+  of command-line options.
+:-compat *version*: Load a file that sets a few options to maintain
+  partial backward-compatibility with a previous version.  This is
+  equivalent to :cmd:`Require Import` `Coq.Compat.CoqXXX` with `XXX`
+  one of the last three released versions (including the current
+  version).  Note that the :ref:`explanations above
+  <interleave-command-line>` regarding the order of command-line
+  options apply, and this could be relevant if you are resetting some
+  of the compatibility options.
 :-dump-glob *file*: Dump references for global names in file *file*
   (to be used by coqdoc, see :ref:`coqdoc`). By default, if *file.v* is being
   compiled, *file.glob* is used.
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 8d1d46676c..976f79d7b7 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -618,6 +618,41 @@ the next command fails because p does not bind in the instance of n.
    Notation "[> a , .. , b <]" :=
      (cons a .. (cons b nil) .., cons b .. (cons a nil) ..).
 
+Notations with expressions used both as binder and term
++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+
+It is possible to use parameters of the notation both in term and
+binding position. Here is an example:
+
+.. coqtop:: in
+
+   Definition force n (P:nat -> Prop) := forall n', n' >= n -> P n'.
+   Notation "▢_ n P" := (force n (fun n => P))
+     (at level 0, n ident, P at level 9, format "▢_ n  P").
+
+.. coqtop:: all
+
+   Check exists p, ▢_p (p >= 1).
+
+More generally, the parameter can be a pattern, as in the following
+variant:
+
+.. coqtop:: in reset
+
+   Definition force2 q (P:nat*nat -> Prop) :=
+     (forall n', n' >= fst q -> forall p', p' >= snd q -> P q).
+
+   Notation "▢_ p P" := (force2 p (fun p => P))
+     (at level 0, p pattern at level 0, P at level 9, format "▢_ p  P").
+
+.. coqtop:: all
+
+   Check exists x y, ▢_(x,y) (x >= 1 /\ y >= 2).
+
+This support is experimental. For instance, the notation is used for
+printing only if the occurrence of the parameter in term position
+comes in the right-hand side before the occurrence in binding position.
+
 .. _RecursiveNotations:
 
 Notations with recursive patterns
@@ -1383,6 +1418,17 @@ Abbreviations
    exception, if the right-hand side is just of the form :n:`@@qualid`,
    this conventionally stops the inheritance of implicit arguments.
 
+   Like for notations, it is possible to bind binders in
+   abbreviations. Here is an example:
+
+   .. coqtop:: in reset
+
+      Definition force2 q (P:nat*nat -> Prop) :=
+        (forall n', n' >= fst q -> forall p', p' >= snd q -> P q).
+
+      Notation F p P := (force2 p (fun p => P)).
+      Check exists x y, F (x,y) (x >= 1 /\ y >= 2).
+
 .. extracted from Gallina chapter
 
 Numerals and strings