From d15d8cc0ce584a6d80d878faf84314c6712ccf69 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 17 Feb 2014 14:32:50 +0100 Subject: 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 --- plugins/extraction/common.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'plugins/extraction/common.mli') 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 -- cgit v1.2.3