diff options
| author | coqbot-app[bot] | 2020-08-25 13:03:36 +0000 |
|---|---|---|
| committer | GitHub | 2020-08-25 13:03:36 +0000 |
| commit | af5e7d44a2a685fe72a65df3daae577938eaa989 (patch) | |
| tree | cd4d0e3e88dd8ddaf223b32cf4d197734c2e558e /interp | |
| parent | 83da5d4f27eb1ebc3eeb89343433fb77b6fccacf (diff) | |
| parent | 80a95afb14fce55781bf7ded5a65233a3f3192b0 (diff) | |
Merge PR #12758: Fixing a coercion entry transitivity bug.
Reviewed-by: SkySkimmer
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 := |