Merge PR #10486: [extraction] Support extraction of Coq's string type to OCaml's string type

Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: herbelin
Ack-by: maximedenes
Reviewed-by: pi8027

3 files changed, 19 insertions, 3 deletions

diff --git a/doc/changelog/12-misc/10486-native-string-extraction.rst b/doc/changelog/12-misc/10486-native-string-extraction.rst
new file mode 100644
index 0000000000..c6778403d4
--- /dev/null
+++ b/doc/changelog/12-misc/10486-native-string-extraction.rst
@@ -0,0 +1,7 @@
+- **Added:**
+  Support for better extraction of strings in OCaml and Haskell:
+  `ExtOcamlNativeString` provides bindings from the Coq `String` type to
+  the OCaml `string` type, and string literals can be extracted to literals,
+  both in OCaml and Haskell. (`#10486
+  <https://github.com/coq/coq/pull/10486>`_, by Xavier Leroy, with help from
+  Maxime Dénès, review by Hugo Herbelin).
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 7136cc28d1..d909f98956 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -313,14 +313,21 @@ The system also provides a mechanism to specify ML terms for inductive
 types and constructors. For instance, the user may want to use the ML
 native boolean type instead of the |Coq| one. The syntax is the following:
 
-.. cmd:: Extract Inductive @qualid => @string [ {+ @string } ]
+.. cmd:: Extract Inductive @qualid => @string__1 [ {+ @string } ]
 
    Give an ML extraction for the given inductive type. You must specify
-   extractions for the type itself (first :token:`string`) and all its
-   constructors (all the :token:`string` between square brackets). In this form,
+   extractions for the type itself (:n:`@string__1`) and all its
+   constructors (all the :n:`@string` between square brackets). In this form,
    the ML extraction must be an ML inductive datatype, and the native
    pattern matching of the language will be used.
 
+   When :n:`@string__1` matches the name of the type of characters or strings
+   (``char`` and ``string`` for OCaml, ``Prelude.Char`` and ``Prelude.String``
+   for Haskell), extraction of literals is handled in a specialized way, so as
+   to generate literals in the target language. This feature requires the type
+   designated by :n:`@qualid` to be registered as the standard char or string type,
+   using the :cmd:`Register` command.
+
 .. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string
 
    Same as before, with a final extra :token:`string` that indicates how to
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index b816ef6210..dbc3a42ee9 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -12,12 +12,14 @@ plugins/extraction/ExtrHaskellZInteger.v
 plugins/extraction/ExtrHaskellZNum.v
 plugins/extraction/ExtrOcamlBasic.v
 plugins/extraction/ExtrOcamlBigIntConv.v
+plugins/extraction/ExtrOcamlChar.v
 plugins/extraction/ExtrOCamlInt63.v
 plugins/extraction/ExtrOCamlFloats.v
 plugins/extraction/ExtrOcamlIntConv.v
 plugins/extraction/ExtrOcamlNatBigInt.v
 plugins/extraction/ExtrOcamlNatInt.v
 plugins/extraction/ExtrOcamlString.v
+plugins/extraction/ExtrOcamlNativeString.v
 plugins/extraction/ExtrOcamlZBigInt.v
 plugins/extraction/ExtrOcamlZInt.v
 plugins/extraction/Extraction.v