Merge PR #12758: Fixing a coercion entry transitivity bug.

Reviewed-by: SkySkimmer

3 files changed, 18 insertions, 1 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index c4e9496b95..0bd5da5729 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1429,7 +1429,7 @@ let declare_entry_coercion (scope,(entry,key)) lev entry' =
   let toaddright =
     EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
         List.fold_right (fun ((lev'',lev'''),path) l ->
-        if entry' = entry'' && level_ord lev' lev'' && entry <> entry'''
+        if entry' = entry'' && level_ord lev'' lev' && entry <> entry'''
         then ((entry,entry'''),((lev,lev'''),path@[(scope,(entry,key))]))::l else l) paths l)
       !entry_coercion_map [] in
   entry_coercion_map :=
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index fa03ec8193..ce51acac95 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -123,3 +123,5 @@ File "stdin", line 297, characters 0-30:
 Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing]
 0 :=: 0
      : Prop
+fun x : nat => <{ x; (S x) }>
+     : nat -> nat
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 90d8da2bec..73445bad12 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -298,3 +298,18 @@ Notation "x :=: y" := (x = y).
 Check (0 :=: 0).
 
 End Bug12691.
+
+Module CoercionEntryTransitivity.
+
+Declare Custom Entry com.
+Declare Custom Entry com_top.
+Notation "<{ e }>" := e (at level 0, e custom com_top at level 99).
+Notation "x ; y" :=
+         (x + y)
+           (in custom com_top at level 90, x custom com at level 90, right associativity).
+Notation "x" := x (in custom com at level 0, x constr at level 0).
+Notation "x" := x (in custom com_top at level 90, x custom com at level 90).
+
+Check fun x => <{ x ; (S x) }>.
+
+End CoercionEntryTransitivity.