diff options
| author | Hugo Herbelin | 2020-07-27 22:15:07 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-09 02:48:26 +0200 |
| commit | 80a95afb14fce55781bf7ded5a65233a3f3192b0 (patch) | |
| tree | b86f1ac2d9aa25913fd0093af0d57fdac684463e /interp | |
| parent | 9d8efb01fde0f9e24157872213c0595cc72efc0c (diff) | |
Fixing a coercion entry transitivity bug.
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 := |