From bfb28c7720d9101e2caedff0c1f1f2cdbf0bad65 Mon Sep 17 00:00:00 2001
From: Xavier Leroy
Date: Mon, 24 Jun 2019 17:08:11 +0200
Subject: Support extraction of Coq's string type to OCaml's string type

Instead of the default extraction to OCaml's "char list" type.
---
 plugins/extraction/common.mli | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'plugins/extraction/common.mli')

diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index e4e9c4c527..d13ac7926a 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -81,3 +81,11 @@ val mk_ind : string -> string -> MutInd.t
 val is_native_char : ml_ast -> bool
 val get_native_char : ml_ast -> char
 val pp_native_char : ml_ast -> Pp.t
+
+(** Special hack for constants of type String.string : if an
+    [Extract Inductive string => string] has been declared, then
+    the constants are directly turned into string literals *)
+
+val is_native_string : ml_ast -> bool
+val get_native_string : ml_ast -> string
+val pp_native_string : ml_ast -> Pp.t
-- 
cgit v1.2.3