From d459c4b237e764740fdcfba71ac92a79e426f1de Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 19 Feb 2014 14:51:10 +0100 Subject: Extraction : minor support stuff for the new Extraction Compute plugin See https://github.com/letouzey/extraction-compute for more details --- plugins/extraction/table.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'plugins/extraction/table.mli') diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 7e47d0bc8..cc93f294b 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -165,6 +165,9 @@ val modular : unit -> bool val set_library : bool -> unit val library : unit -> bool +val set_extrcompute : bool -> unit +val is_extrcompute : unit -> bool + (*s Table for custom inlining *) val to_inline : global_reference -> bool -- cgit v1.2.3