From 80a95afb14fce55781bf7ded5a65233a3f3192b0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 27 Jul 2020 22:15:07 +0200
Subject: Fixing a coercion entry transitivity bug.

---
 interp/notation.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation.ml')

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 :=
-- 
cgit v1.2.3