diff options
| author | Pierre-Marie Pédrot | 2020-09-11 16:10:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-17 16:12:33 +0200 |
| commit | 60a55b1525cd02eb8fccae82d8dc2c2cd231664d (patch) | |
| tree | 626f1e372a666aec2e9fa5c4c41cbf23f16d4931 /kernel/float64.mli | |
| parent | 1be09366e6d2dcf8b1257348c928727a66928760 (diff) | |
Be more efficient when generating the merge of ltle maps in AcyclicGraph.
We try to avoid reallocating the map in two different ways.
- We only add a value when actually needed.
- We compute the union of maps with the first element as a starting point.
Diffstat (limited to 'kernel/float64.mli')
0 files changed, 0 insertions, 0 deletions