aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_12970.v
AgeCommit message (Collapse)Author
2020-10-14Fix algebraic on the right when using bidi hintsGaƫtan Gilbert
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.