diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/notation.ml | 2 |
1 files changed, 1 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 := |