Merge PR #13265: Add support for general non-necessarily-recursive binders in notations

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

2 files changed, 30 insertions, 0 deletions

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 86c4b3cccc..df64ae2af3 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -197,3 +197,15 @@ Found an inductive type while a pattern was expected.
      : nat * nat
 %%%
      : Type
+## (x, _) (x = 0)
+     : Prop
+The command has indeed failed with message:
+Unexpected type constraint in notation already providing a type constraint.
+## '(x, y) (x + y = 0)
+     : Prop
+## x (x = 0)
+     : Prop
+## '(x, y) (x = 0)
+     : Prop
+fun f : ## a (a = 0) => f 1 eq_refl
+     : ## a (a = 0) -> 1 = 0
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 6af192ea82..ebc1426fc8 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -487,3 +487,21 @@ Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
 Check %%%.
 
 End MorePrecise3.
+
+Module TypedPattern.
+
+Notation "## x P" := (forall x:nat*nat, P) (x pattern, at level 0).
+Check ## (x,y) (x=0).
+Fail Check ## ((x,y):bool*bool) (x=y).
+
+End TypedPattern.
+
+Module SingleBinder.
+
+Notation "## x P" := (forall x, x = x -> P) (x binder, at level 0).
+Check ## '(x,y) (x+y=0).
+Check ## (x:nat) (x=0).
+Check ## '((x,y):nat*nat) (x=0).
+Check fun (f : ## {a} (a=0)) => f (a:=1) eq_refl.
+
+End SingleBinder.