From 0ea2d0ff4ed84e1cc544c958b8f6e98f6ba2e9b6 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 3 Feb 2020 18:19:42 +0100
Subject: 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>
---
 doc/stdlib/hidden-files             | 1 +
 doc/stdlib/index-list.html.template | 7 +++++++
 2 files changed, 8 insertions(+)

(limited to 'doc/stdlib')

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>
-- 
cgit v1.2.3