diff options
| author | Hugo Herbelin | 2014-11-14 12:54:39 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-14 13:17:20 +0100 |
| commit | 194ad253a24ce542d9b1bb4c13ad0d2f64a0aa48 (patch) | |
| tree | 99f09e19a060d0f6bc812265221b2046aa7012ba /dev | |
| parent | 1414ab30f9d030a4421da766121accb03276d827 (diff) | |
Preserving the good effect of 014e5ac92a on not leaving dangling local
definitions while keeping some compatibility on when to generalize
when an index also occur in a parameter (effect on PersistentUnionFind
for instance).
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions