diff options
Diffstat (limited to 'plugins/extraction/common.mli')
| -rw-r--r-- | plugins/extraction/common.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index a6351fc4c..b8e95afb3 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -36,9 +36,6 @@ 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 |