diff options
| author | Hugo Herbelin | 2014-11-03 15:00:32 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-03 15:27:04 +0100 |
| commit | 7af811e5100839484cbed0126b5c37a972487ec3 (patch) | |
| tree | 4a377904b91723805366bfc89bdcf2954037cbe5 /stm/asyncTaskQueue.ml | |
| parent | 7d01d46ce0f9267446b474755762db1ccca5fd78 (diff) | |
Fix to 844431761 on improving elimination with indices, getting rid of
intrusive residual local definitions + more conservative strategy for
which variables are not generalized (point 2 of 4df1ddc6d6bd07073).
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions