diff options
Diffstat (limited to 'plugins/extraction/extract_env.mli')
| -rw-r--r-- | plugins/extraction/extract_env.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 90f4f911b7..4f0ed953c6 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -8,6 +8,7 @@ (*s This module declares the extraction commands. *) +open API open Names open Libnames open Globnames @@ -20,12 +21,12 @@ val extraction_library : bool -> Id.t -> unit (* For debug / external output via coqtop.byte + Drop : *) val mono_environment : - global_reference list -> module_path list -> Miniml.ml_structure + global_reference list -> ModPath.t list -> Miniml.ml_structure (* Used by the Relation Extraction plugin *) val print_one_decl : - Miniml.ml_structure -> module_path -> Miniml.ml_decl -> Pp.std_ppcmds + Miniml.ml_structure -> ModPath.t -> Miniml.ml_decl -> Pp.std_ppcmds (* Used by Extraction Compute *) |