A temporary fix of #13018 and #12775 for branch 8.2.

We arbitrarily use max_int as higher level of custom entries in
printing, which should be ok since only < and <= are used to decide
when to use coercions.

2 files changed, 44 insertions, 0 deletions

diff --git a/test-suite/output/bug_13018.out b/test-suite/output/bug_13018.out
new file mode 100644
index 0000000000..2f60409e23
--- /dev/null
+++ b/test-suite/output/bug_13018.out
@@ -0,0 +1,14 @@
+gargs:( (!) )
+     : list nat
+gargs:( (!, !, !) )
+     : list nat
+OnlyGargs[ (!) ]
+     : list nat
+gargs999:( (!) )
+     : list nat
+gargs999:( (!, !, !) )
+     : list nat
+OnlyGargs[ (!) ]
+     : list nat
+OnlyGargs999[ (!) ]
+     : list nat
diff --git a/test-suite/output/bug_13018.v b/test-suite/output/bug_13018.v
new file mode 100644
index 0000000000..3fb8b7f905
--- /dev/null
+++ b/test-suite/output/bug_13018.v
@@ -0,0 +1,30 @@
+Undelimit Scope list_scope.
+Declare Custom Entry gnat.
+Declare Custom Entry gargs.
+
+Notation "!" := 42 (in custom gnat).
+Notation "gargs:( e  )" := e (e custom gargs).
+Notation "( x )" := (cons x (@nil nat)) (in custom gargs, x custom gnat).
+Notation "( x , y , .. , z )" := (cons x (cons y .. (cons z nil) ..))
+  (in custom gargs, x custom gnat, y custom gnat, z custom gnat).
+
+Check gargs:( (!) ). (* cons 42 nil *)
+Check gargs:( (!, !, !) ). (* cons 42 (42 :: 42 :: nil) *)
+
+Definition OnlyGargs {T} (x:T) := x.
+Notation "OnlyGargs[ x  ]" := (OnlyGargs x) (at level 10, x custom gargs).
+Check OnlyGargs[ (!) ]. (* OnlyGargs[ cons 42 nil] *)
+
+Declare Custom Entry gargs999.
+Notation "gargs999:( e  )" := e (e custom gargs999 at level 999).
+Notation "( x )" := (cons x (@nil nat)) (in custom gargs999, x custom gnat at level 999).
+Notation "( x , y , .. , z )" := (cons x (cons y .. (cons z nil) ..))
+  (in custom gargs999, x custom gnat at level 999, y custom gnat at level 999, z custom gnat at level 999).
+
+Check gargs999:( (!) ). (* gargs999:( (!)) *)
+Check gargs999:( (!, !, !) ). (* gargs999:( (!, !, !)) *)
+Check OnlyGargs[ (!) ]. (* OnlyGargs[ gargs999:( (!))] *)
+
+Definition OnlyGargs999 {T} (x:T) := x.
+Notation "OnlyGargs999[ x  ]" := (OnlyGargs999 x) (at level 10, x custom gargs999 at level 999).
+Check OnlyGargs999[ (!) ]. (* OnlyGargs999[ (!)] *)