diff options
Diffstat (limited to 'plugins/extraction/extract_env.mli')
| -rw-r--r-- | plugins/extraction/extract_env.mli | 11 |
1 files changed, 5 insertions, 6 deletions
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 *) |