aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/stdlib/hidden-files2
-rw-r--r--plugins/extraction/ExtrOcamlNativeString.v (renamed from plugins/extraction/ExtrOcamlStringPlus.v)0
2 files changed, 1 insertions, 1 deletions
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index 97ff84dd8e..3e53c05439 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -18,7 +18,7 @@ plugins/extraction/ExtrOcamlIntConv.v
plugins/extraction/ExtrOcamlNatBigInt.v
plugins/extraction/ExtrOcamlNatInt.v
plugins/extraction/ExtrOcamlString.v
-plugins/extraction/ExtrOcamlStringPlus.v
+plugins/extraction/ExtrOcamlNativeString.v
plugins/extraction/ExtrOcamlZBigInt.v
plugins/extraction/ExtrOcamlZInt.v
plugins/extraction/Extraction.v
diff --git a/plugins/extraction/ExtrOcamlStringPlus.v b/plugins/extraction/ExtrOcamlNativeString.v
index 45d3ef3d3c..45d3ef3d3c 100644
--- a/plugins/extraction/ExtrOcamlStringPlus.v
+++ b/plugins/extraction/ExtrOcamlNativeString.v