diff options
| author | Gaëtan Gilbert | 2020-10-14 17:20:41 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-10-14 17:21:02 +0200 |
| commit | 276ad0f2f2db5e4ddc569da606a6db8873fdec00 (patch) | |
| tree | 1c3c8f190217456824cb3a414791303a86576b2a /dev/include_printers | |
| parent | 411025844a4c005ce03d77c6c640807c28269d4a (diff) | |
Fix algebraic on the right when using bidi hints
Fix #12970
We can't recover the expected type of the post bidi argument by
retyping because the hole may be filled by something in which case
retyping can produce algebraic universes.
Diffstat (limited to 'dev/include_printers')
0 files changed, 0 insertions, 0 deletions