diff options
| author | Matthieu Sozeau | 2014-05-08 13:46:48 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-08 19:23:51 +0200 |
| commit | a6c966a23e24be9543b01b6944826ab5479fd784 (patch) | |
| tree | d52888ae805c3782073f8d44e6158e61e88c511b /dev | |
| parent | 18569c5714ae16f867cabebf98327026409e6eaf (diff) | |
Avoid allocations in type_of_inductive
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions