From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- plugins/extraction/extract_env.mli | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'plugins/extraction/extract_env.mli') diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 591d3bb8..54fde2ca 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -12,21 +12,20 @@ open Names open Libnames -open Globnames -val simple_extraction : reference -> unit -val full_extraction : string option -> reference list -> unit -val separate_extraction : reference list -> unit +val simple_extraction : qualid -> unit +val full_extraction : string option -> qualid list -> unit +val separate_extraction : qualid 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 +val extract_and_compile : qualid list -> unit (* For debug / external output via coqtop.byte + Drop : *) val mono_environment : - global_reference list -> ModPath.t list -> Miniml.ml_structure + GlobRef.t list -> ModPath.t list -> Miniml.ml_structure (* Used by the Relation Extraction plugin *) -- cgit v1.2.3