diff options
Diffstat (limited to 'plugins/extraction/common.mli')
| -rw-r--r-- | plugins/extraction/common.mli | 3 |
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 |