1 files changed, 43 insertions, 1 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index dbe714c388..8bfcab0f4e 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -163,6 +163,10 @@ Grammar constr` is at level 100. To avoid ``x : A`` being parsed as a type cast,
 it is necessary to put ``x`` at a level below 100, typically 99. Hence, a correct
 definition is the following:
 
+.. coqtop:: none
+
+   Reset Initial.
+
 .. coqtop:: all
 
    Notation "{ x : A | P }" := (sig A (fun x => P)) (x at level 99).
@@ -350,6 +354,11 @@ Reserving notations
       This command declares an infix parsing rule without giving its
       interpretation.
 
+   When a format is attached to a reserved notation, it is used by
+   default by all subsequent interpretations of the corresponding
+   notation. A specific interpretation can provide its own format
+   overriding the default format though.
+
 Simultaneous definition of terms and notations
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -408,6 +417,27 @@ identifiers or tokens starting with a single quote are dropped.
    Locate "exists".
    Locate "exists _ .. _ , _".
 
+Inheritance of the properties of arguments of constants bound to a notation
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+If the right-hand side of a notation is a partially applied constant,
+the notation inherits the implicit arguments (see
+:ref:`ImplicitArguments`) and interpretation scopes (see
+:ref:`Scopes`) of the constant. For instance:
+
+.. coqtop:: in reset
+
+   Record R := {dom : Type; op : forall {A}, A -> dom}.
+   Notation "# x" := (@op x) (at level 8).
+
+.. coqtop:: all
+
+   Check fun x:R => # x 3.
+
+As an exception, if the right-hand side is just of the form
+:n:`@@qualid`, this conventionally stops the inheritance of implicit
+arguments (but not of interpretation scopes).
+
 Notations and binders
 ~~~~~~~~~~~~~~~~~~~~~
 
@@ -798,7 +828,13 @@ associated to the custom entry ``expr``. The level can be omitted, as in
 
    Notation "[ e ]" := e (e custom expr).
 
-in which case Coq tries to infer it.
+in which case Coq infer it. If the sub-expression is at a border of
+the notation (as e.g. ``x`` and ``y`` in ``x + y``), the level is
+determined by the associativity. If the sub-expression is not at the
+border of the notation (as e.g. ``e`` in ``"[ e ]``), the level is
+inferred to be the highest level used for the entry. In particular,
+this level depends on the highest level existing in the entry at the
+time of use of the notation.
 
 In the absence of an explicit entry for parsing or printing a
 sub-expression of a notation in a custom entry, the default is to
@@ -1400,6 +1436,12 @@ Abbreviations
    denoted expression is performed at definition time. Type checking is
    done only at the time of use of the abbreviation.
 
+   Like for notations, if the right-hand side of an abbreviation is a
+   partially applied constant, the abbreviation inherits the implicit
+   arguments and interpretation scopes of the constant. As an
+   exception, if the right-hand side is just of the form :n:`@@qualid`,
+   this conventionally stops the inheritance of implicit arguments.
+
 .. _numeral-notations:
 
 Numeral notations