Partial fix to #4592 (notation requiring alpha-conversion for printing).

2 files changed, 19 insertions, 0 deletions

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 64317a9f83..6b2177830a 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -32,3 +32,9 @@ fun f : forall x : nat * (bool * unit), ?T => CURRY (x : nat) (y : bool), f
        forall (x : nat) (y : bool), ?T@{x:=(x, (y, tt))}
 where
 ?T : [x : nat * (bool * unit) |- Type] 
+forall n : nat, {#n | 1 > n}
+     : Prop
+forall x : nat, {|x | x > 0|}
+     : Prop
+exists2 x : nat, x = 1 & x = 2
+     : Prop
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 655a01c2d2..f6e0d2d9dd 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -36,3 +36,16 @@ Check ETA x y, le_S.
 
 Notation "'CURRY' x .. y , f" := (fun x => .. (fun y => f (x, .. (y,tt) ..)) ..) (at level 200, x binder, y binder).
 Check fun f => CURRY (x:nat) (y:bool), f.
+
+(**********************************************************************)
+(* Notations with variables bound both as a term and as a binder      *)
+(* This is #4592 *)
+
+Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)).
+Check forall n:nat, {# n | 1 > n}.
+
+Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop.
+Notation "{| x | P |}" := (foo x (fun x => P)).
+Check forall x:nat, {| x | x > 0 |}.
+
+Check ex2 (fun x => x=1) (fun x0 => x0=2).