diff options
| author | Pierre-Marie Pédrot | 2016-08-04 18:46:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-08-04 19:16:16 +0200 |
| commit | 118572b57a6f15ad4342e8a75ca0836e7896d465 (patch) | |
| tree | 284037cb9a195fa04c061ff7f4957c7c1ff43b66 /kernel/nativecode.ml | |
| parent | 62d5ef53da153394c69b52cc707b72d53eaeac44 (diff) | |
Use sets instead of lists for names to avoid in evar generation.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions