diff options
| author | Maxime Dénès | 2020-02-03 18:19:42 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2020-07-06 11:22:43 +0200 |
| commit | 0ea2d0ff4ed84e1cc544c958b8f6e98f6ba2e9b6 (patch) | |
| tree | fbad060c3c2e29e81751dea414c898b5cb0fa22d /doc/stdlib | |
| parent | cf388fdb679adb88a7e8b3122f65377552d2fb94 (diff) | |
Primitive persistent arrays
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>
Diffstat (limited to 'doc/stdlib')
| -rw-r--r-- | doc/stdlib/hidden-files | 1 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 7 |
2 files changed, 8 insertions, 0 deletions
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index 4badb20295..f39c50238a 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -15,6 +15,7 @@ theories/extraction/ExtrOcamlBigIntConv.v theories/extraction/ExtrOcamlChar.v theories/extraction/ExtrOCamlInt63.v theories/extraction/ExtrOCamlFloats.v +theories/extraction/ExtrOCamlPArray.v theories/extraction/ExtrOcamlIntConv.v theories/extraction/ExtrOcamlNatBigInt.v theories/extraction/ExtrOcamlNatInt.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index ab615d5f65..7c1328916b 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -709,4 +709,11 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/Coq812.v theories/Compat/Coq813.v </dd> + + <dt> <b>Array</b>: + Persistent native arrays + </dt> + <dd> + theories/Array/PArray.v + </dd> </dl> |