aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/common.mli
diff options
context:
space:
mode:
authorPierre Letouzey2017-02-05 01:46:41 +0100
committerPierre Letouzey2017-02-07 22:56:56 +0100
commit69c4e7cfa0271f024b2178082e4be2e3ca3be263 (patch)
tree011f39f68dcc1da8c622adf32931ca084a2f8c15 /plugins/extraction/common.mli
parent8ef3bc0e8a65b3a0338da39aa54cd75b1c2c1bb7 (diff)
Extraction: avoid deprecated functions of module String
- A few tweaks of string are now done via the Bytes module - lots of String.capitalize_ascii and co
Diffstat (limited to 'plugins/extraction/common.mli')
-rw-r--r--plugins/extraction/common.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index b8e95afb38..a6351fc4c4 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -36,6 +36,9 @@ val pr_binding : Id.t list -> std_ppcmds
val rename_id : Id.t -> Id.Set.t -> Id.t
+(** For Scheme extraction, replace the ['] by [~] *)
+val unquote : string -> string
+
type env = Id.t list * Id.Set.t
val empty_env : unit -> env