diff options
| author | Pierre-Marie Pédrot | 2016-06-22 21:14:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-23 17:38:34 +0200 |
| commit | 9165bd2489842af64dbe098ed5906fe69e687bfe (patch) | |
| tree | 4b6882db70bad500d1177c9d5c8aa73bfab510c8 /kernel/nativelambda.ml | |
| parent | 861f385008d6c7f4a1a03f66589d34e974f0a341 (diff) | |
Better algorithm for variable deambiguation in term printing.
We do not recompute shortest name identifier for global references that were
already traversed. Furthermore, we share the computation of identifiers
between invokations of the name generating function.
This drastically speeds up detyping for huge goals, further mitigating the
shortcomings of the fix for bug #4777.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions