aboutsummaryrefslogtreecommitdiff
path: root/API/API.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2017-07-27 15:09:14 +0200
committerEmilio Jesus Gallego Arias2017-10-05 12:42:24 +0200
commit8fa1d224dafde29f5b527d380c069f196a042c60 (patch)
tree380c705def5e901aa6bc03dba9c33e5dc33493ed /API/API.ml
parent8b5f7ad0722e5ed1b87589ae103a1c4c5974416f (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/API.ml')
0 files changed, 0 insertions, 0 deletions