1 files changed, 36 insertions, 0 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index a8d5ac610f..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
 ~~~~~~~~~~~~~~~~~~~~~
 
@@ -1406,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