diff options
Diffstat (limited to 'plugins/extraction/common.mli')
| -rw-r--r-- | plugins/extraction/common.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 3058b91b6..ffb6029b2 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -79,4 +79,5 @@ val mk_ind : string -> string -> mutual_inductive the constants are directly turned into chars *) val is_native_char : ml_ast -> bool +val get_native_char : ml_ast -> char val pp_native_char : ml_ast -> std_ppcmds |