From 21327e39ef6c6e04569bf8f138d242819139964d Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 4 Jul 2017 23:15:38 +0200 Subject: Extraction TestCompile foo : a new command for extraction + ocamlc Extraction TestCompile foo is equivalent to: Extraction "/tmp/testextraction1234.ml" foo ocamlfind ocamlc -I /tmp -c /tmp/testextraction1234.mli /tmp/testextraction1234.ml This command isn't meant for the end user, but rather as an helper for test-suite scripts. It only works with extraction to OCaml, and the generated code should be standalone. --- plugins/extraction/extract_env.mli | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'plugins/extraction/extract_env.mli') diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 0629a84a0..276c4099d 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -18,6 +18,10 @@ val full_extraction : string option -> reference list -> unit val separate_extraction : reference list -> unit val extraction_library : bool -> Id.t -> unit +(* For the test-suite : extraction to a temporary file + ocamlc on it *) + +val extract_and_compile : reference list -> unit + (* For debug / external output via coqtop.byte + Drop : *) val mono_environment : -- cgit v1.2.3