diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-02-17 14:32:50 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-01-11 09:49:32 +0100 |
| commit | d15d8cc0ce584a6d80d878faf84314c6712ccf69 (patch) | |
| tree | 0042925526cfd801451cdbe5472f44cd2169a57c /plugins/extraction/common.mli | |
| parent | b858f939f33dc4bc4c8e470ed62310ef15c59a99 (diff) | |
Extraction: minor tweaks to ease ongoing experiments about Lambda
- Common.get_native_char instead of just a pp function of this char
- Enrich the record projection table
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 |