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/index-list.html.template | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'doc/stdlib/index-list.html.template')

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