diff options
| -rw-r--r-- | contrib/extraction/extract_env.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli index baf79573fb..bf470d0968 100644 --- a/contrib/extraction/extract_env.mli +++ b/contrib/extraction/extract_env.mli @@ -16,3 +16,8 @@ open Libnames val simple_extraction : reference -> unit val full_extraction : string option -> reference list -> unit val extraction_library : bool -> identifier -> unit + +(* For debug / external output via coqtop.byte + Drop : *) + +val mono_environment : + global_reference list -> module_path list -> Miniml.ml_structure |