diff options
Diffstat (limited to 'contrib/extraction/table.mli')
| -rw-r--r-- | contrib/extraction/table.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index fc29e871c..608eb6771 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -141,6 +141,13 @@ val extract_constant_inline : bool -> reference -> string list -> string -> unit val extract_inductive : reference -> string * string list -> unit +(*s Table of blacklisted filenames *) + +val is_blacklisted : string -> bool + +val extraction_blacklist : identifier list -> unit +val reset_extraction_blacklist : unit -> unit +val print_extraction_blacklist : unit -> unit |