Merge PR #8808: Extending support for mixing binders and terms in abbreviations

Ack-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: mattam82

2 files changed, 50 insertions, 0 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/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index ea5ad79a80..c5ec636d5f 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).
+
 .. _numeral-notations:
 
 Numeral notations