Fixes coq#18223: wrong printing coercions order for transitive closur…

…e on the right.

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) ->

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

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.