diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-01-30 10:01:50 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-30 10:01:50 +0100 |
commit | 879ebad4d0b39fda275a72ba44c1f4dfbb9282e5 (patch) | |
tree | b2775e675b9b82acd5fd8a34b99b7b33af782d91 /pretyping/retyping.ml | |
parent | ae2429e6cf0e4faa0e57bd3b1393efc3b532920a (diff) | |
parent | 4be607ec6c0b89e85566b4a6952bdf41e40fae7b (diff) |
Merge PR #6666: Fix reduction of primitive projections on coinductive records for cbv and native_compute
Diffstat (limited to 'pretyping/retyping.ml')
0 files changed, 0 insertions, 0 deletions