coq/test-suite/primitive/arrays, branch master The formal proof system Be more thorough when testing PArray.set. 2021-03-26T14:18:28+00:00 Guillaume Melquiond 2021-03-25T13:59:06+00:00 8325738669b591c295848fb8d366ac838273bf75 






Remove occurrences of Parray.reroot.
2020-10-08T09:16:48+00:00

Guillaume Melquiond

2020-08-31T06:52:05+00:00

e3764e1e857fce9b6d4cb018db676db3612c00a0












Primitive persistent arrays
2020-07-06T09:22:43+00:00

Maxime Dénès

2020-02-03T17:19:42+00:00

0ea2d0ff4ed84e1cc544c958b8f6e98f6ba2e9b6

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>





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>