aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-09-21 13:35:42 +0200
committerGaëtan Gilbert2020-10-09 11:48:46 +0200
commitcada5caf9c739efc7a2d932af4498b61f7fc9608 (patch)
tree112cfdc602f5607a15027761ea7c4409e81296ca /dev
parentf53f84d32dff2820043df92e743234e3fdaa3520 (diff)
No bidirectionality when expected type for lambda is an evar.
This fixes #12623 (bidirectionality breaks impredicativity).
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions