diff options
| author | Matthieu Sozeau | 2014-07-03 18:51:13 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-03 18:53:17 +0200 |
| commit | e7ba2a9be24823503495e959f0dffc131e99801b (patch) | |
| tree | db0a3979974c88e101804438cfb89c1ddc70742d /kernel/type_errors.ml | |
| parent | f2327aa3c69f1695f99e2ccbfe00c4e54e56e7d2 (diff) | |
Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanly when called
on partially applied constructors. Also protect evar_conv from that case.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions