From 7b684bac32f05fa76119de11a974aec0e9beade7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Mon, 30 Oct 2023 21:21:47 +0100
Subject: [PATCH] Fixes #18223: wrong printing coercions order for transitive
 closure on the right.

---
 interp/notation.ml              |  2 +-
 test-suite/output/bug_18223.out |  4 ++++
 test-suite/output/bug_18223.v   | 22 ++++++++++++++++++++++
 3 files changed, 27 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/output/bug_18223.out
 create mode 100644 test-suite/output/bug_18223.v

diff --git a/interp/notation.ml b/interp/notation.ml
index d40070b3e86b..66025450c70a 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1590,7 +1590,7 @@ let declare_entry_coercion ntn entry_level entry_relative_level' =
         if included { notation_entry = entry''; notation_level = lev'' } entry_relative_level' &&
            not (included entry_level
                   { notation_subentry = entry'''; notation_relative_level = sublev'''; notation_position = None })
-        then ((entry,entry'''),((lev,sublev'''),path@[ntn]))::l else l) paths l)
+        then ((entry,entry'''),((lev,sublev'''),ntn::path))::l else l) paths l)
       !entry_coercion_map [] in
   entry_coercion_map :=
     List.fold_right (fun (pair,path) ->
diff --git a/test-suite/output/bug_18223.out b/test-suite/output/bug_18223.out
new file mode 100644
index 000000000000..747a1aec11df
--- /dev/null
+++ b/test-suite/output/bug_18223.out
@@ -0,0 +1,4 @@
+fun a b : A => < {| b a |} >
+     : A -> A -> A
+fun a b : A => < {| b a |} >
+     : A -> A -> A
diff --git a/test-suite/output/bug_18223.v b/test-suite/output/bug_18223.v
new file mode 100644
index 000000000000..579f2a7b899d
--- /dev/null
+++ b/test-suite/output/bug_18223.v
@@ -0,0 +1,22 @@
+Declare Custom Entry foo.
+Declare Custom Entry bar.
+
+Parameter (A : Type).
+Parameter (Q : A -> A -> A).
+Parameter (P : A -> A).
+
+Notation "< x >" := (P x) (x custom foo).
+Notation "x y" := (Q x y)  (in custom bar at level 1, right associativity).
+Notation "x" := x (in custom bar at level 0, x global).
+
+Module Order1.
+Notation "| x |" := (x) (x custom bar).
+Notation "{ x }" := (x) (in custom foo, x constr).
+Check (fun a b => < {Q b a} >).
+End Order1.
+
+Module Order2.
+Notation "{ x }" := (x) (in custom foo, x constr).
+Notation "| x |" := (x) (x custom bar).
+Check (fun a b => < {Q b a} >).
+End Order2.