aboutsummaryrefslogtreecommitdiff
path: root/doc/stdlib
diff options
context:
space:
mode:
authorXavier Leroy2019-07-11 09:54:45 +0200
committerMaxime Dénès2020-01-08 15:07:15 +0100
commite3640bdbbac76807457d50ac60e93192d137f3f9 (patch)
tree69fcba7094cec7d201d3f91ca9f818601e715df1 /doc/stdlib
parentef7a95e2ca705f0fd72f15e7352eb77bf9c6eaed (diff)
Hide ExtrOcamlStringPlus.v like the other extraction files
Diffstat (limited to 'doc/stdlib')
-rw-r--r--doc/stdlib/hidden-files1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index b816ef6210..97ff84dd8e 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -18,6 +18,7 @@ plugins/extraction/ExtrOcamlIntConv.v
plugins/extraction/ExtrOcamlNatBigInt.v
plugins/extraction/ExtrOcamlNatInt.v
plugins/extraction/ExtrOcamlString.v
+plugins/extraction/ExtrOcamlStringPlus.v
plugins/extraction/ExtrOcamlZBigInt.v
plugins/extraction/ExtrOcamlZInt.v
plugins/extraction/Extraction.v