diff options
| author | Guillaume Melquiond | 2020-08-31 08:05:48 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2020-10-08 11:16:12 +0200 |
| commit | ddd7371dc3b82124c2bb36b93e6c2b185bcc02d2 (patch) | |
| tree | 9c1d5b20547d9f947ee84e9da7460fea4c044bc6 /kernel/float64.ml | |
| parent | 1d4f6609a99212c957a57d18f7d0df69d6be5f99 (diff) | |
Reroot primitive arrays on access (fix #12947).
Semi-persistent arrays are supposed to have amortized O(1) complexity.
This commit ensures it, without forcing the user to litter its functions
with explicit calls to reroot.
This commit also makes rerootk faster by carrying the array along the
dependency chain rather than recomputing it at every step.
Diffstat (limited to 'kernel/float64.ml')
0 files changed, 0 insertions, 0 deletions