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/extract_env.mli | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'plugins/extraction/extract_env.mli') diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 5769ff1176..7bbb825b10 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -34,5 +34,4 @@ val print_one_decl : (* Used by Extraction Compute *) val structure_for_compute : - Term.constr -> - Miniml.ml_flat_structure * Miniml.ml_ast * Miniml.ml_type + Term.constr -> (Miniml.ml_decl list) * Miniml.ml_ast * Miniml.ml_type -- cgit v1.2.3