diff options
Diffstat (limited to 'contrib/extraction/extract_env.mli')
| -rw-r--r-- | contrib/extraction/extract_env.mli | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli index 18b106da2..baf79573f 100644 --- a/contrib/extraction/extract_env.mli +++ b/contrib/extraction/extract_env.mli @@ -13,8 +13,6 @@ open Names open Libnames -val extraction : reference -> unit -val extraction_rec : reference list -> unit -val extraction_file : string -> reference list -> unit -val extraction_module : reference -> unit +val simple_extraction : reference -> unit +val full_extraction : string option -> reference list -> unit val extraction_library : bool -> identifier -> unit |