diff options
| author | Pierre-Marie Pédrot | 2020-07-06 16:18:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-07-06 16:18:33 +0200 |
| commit | 8907a5b7d2b91bff0b573956a05e4679b5238161 (patch) | |
| tree | 2fff532e687a8e82543044352aeaf3168434aac1 /doc/stdlib | |
| parent | 3244b9c6e4159042bae0cd2ad48aba77928d7b2d (diff) | |
| parent | 0ea2d0ff4ed84e1cc544c958b8f6e98f6ba2e9b6 (diff) | |
Merge PR #11604: Primitive persistent arrays
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
Ack-by: proux01
Ack-by: silene
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> |