| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-10-08 | Reroot primitive arrays on access (fix #12947). | Guillaume Melquiond | |
| 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. | |||
| 2020-07-06 | Primitive persistent arrays | Maxime Dénès | |
| Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |