Merge PR #11090: Printing of coercions to which a notation is associated: a refined version of #8890 which prevents #11033.

Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares

2 files changed, 16 insertions, 0 deletions

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index ba4ac5a8f9..32120a9674 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -59,3 +59,5 @@ where
       |- Type] (pat, p0, p cannot be used)
 fun '{| |} => true
      : R -> bool
+b = a
+     : Prop
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 4b9d0abd95..d3433949d1 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -140,3 +140,17 @@ Record R := { n : nat }.
 Check fun '{|n:=x|} => true.
 
 End EmptyRecordSyntax.
+
+Module L.
+
+(* Testing regression #11053 *)
+
+Section Test.
+Variables (A B : Type) (a : A) (b : B).
+Variable c : A -> B.
+Coercion c : A >-> B.
+Notation COERCION := (c).
+Check b = a.
+End Test.
+
+End L.