aboutsummaryrefslogtreecommitdiff
path: root/lib/pp_diff.ml
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 /lib/pp_diff.ml
parentf53f84d32dff2820043df92e743234e3fdaa3520 (diff)
No bidirectionality when expected type for lambda is an evar.
This fixes #12623 (bidirectionality breaks impredicativity).
Diffstat (limited to 'lib/pp_diff.ml')
0 files changed, 0 insertions, 0 deletions