aboutsummaryrefslogtreecommitdiff
path: root/doc/stdlib
diff options
context:
space:
mode:
Diffstat (limited to 'doc/stdlib')
-rw-r--r--doc/stdlib/hidden-files1
-rw-r--r--doc/stdlib/index-list.html.template7
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>