diff options
| author | Emilio Jesus Gallego Arias | 2017-07-27 15:09:14 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-10-05 12:42:24 +0200 |
| commit | 8fa1d224dafde29f5b527d380c069f196a042c60 (patch) | |
| tree | 380c705def5e901aa6bc03dba9c33e5dc33493ed /API | |
| parent | 8b5f7ad0722e5ed1b87589ae103a1c4c5974416f (diff) | |
[pp] Minor optimization in `Pp.t` construction and gluing.
The typical Coq `Pp.t` document contains a lot of "gluing" which
produces efficient structures but it is quite painful in
serialization.
We optimize a common document building case so we don't create as much
glue nodes as with the "naive" strategy, and without incurring in the
large performance cost full flattening would produce.
This is a temporal fixup, see #505 for more context on the discussion
and medium-term plans.
Diffstat (limited to 'API')
0 files changed, 0 insertions, 0 deletions
