Merge PR #12683: Fixes #12682: printing bug with recursive notations for n-ary applications used with applied references

Reviewed-by: ejgallego

2 files changed, 28 insertions, 3 deletions

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 53ad8a9612..90a6a2ad96 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -80,6 +80,12 @@ NIL : list nat
      : Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool))
 fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|} : Z
      : (Z -> Z -> Z -> Z) -> Z
+{|fun x : Z => x + x; 0|}
+     : Z
+{|op; 0; 1|}
+     : Z
+false = 0
+     : Prop
 Init.Nat.add
      : nat -> nat -> nat
 S
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 7d2f1e9ba8..d0b2f40f9c 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -216,13 +216,32 @@ Check [|0*(1,2,3);(4,5,6)*false|].
 
 (**********************************************************************)
 (* Test recursive notations involving applications                    *)
-(* Caveat: does not work for applied constant because constants are   *)
-(* classified as notations for the particular constant while this     *)
-(* generic application notation is classified as generic              *)
+
+Module Application.
 
 Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y).
+
+(* Application to a variable *)
+
 Check fun f => {| f; 0; 1; 2 |} : Z.
 
+(* Application to a fun *)
+
+Check {| (fun x => x+x); 0 |}.
+
+(* Application to a reference *)
+
+Axiom op : Z -> Z -> Z.
+Check {| op; 0; 1 |}.
+
+(* Interaction with coercion *)
+
+Axiom c : Z -> bool.
+Coercion c : Z >-> bool.
+Check false = {| c; 0 |}.
+
+End Application.
+
 (**********************************************************************)
 (* Check printing of notations from other modules *)