diff options
| author | Pierre-Marie Pédrot | 2018-11-22 17:02:12 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-04-02 10:41:19 +0200 |
| commit | 99362197a42fdbf8d39f1cde0723389b5114dd98 (patch) | |
| tree | 2ef1bf9c28253a7d3f7d12230a4e7db832cff456 /lib/control.ml | |
| parent | 19757d0cc64b221a3a333b12db14454a447dd7ee (diff) | |
Fast name generation in detyping.
We provide a flag that allows for a dumber but O(log n) algorithm generating
fresh names in detyping.
Diffstat (limited to 'lib/control.ml')
0 files changed, 0 insertions, 0 deletions