Merge PR #11120: Refactoring code for application printing + fixing #11091 (inconsistencies in parsing/printing notations to partial applications)

Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: jfehrle

1 files changed, 27 insertions, 0 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 7c628e534b..8bfcab0f4e 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -417,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
 ~~~~~~~~~~~~~~~~~~~~~
 
@@ -1415,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