diff options
Diffstat (limited to 'plugins/extraction/table.mli')
| -rw-r--r-- | plugins/extraction/table.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 04d90b881..b215e373e 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -149,7 +149,10 @@ val extract_constant_inline : bool -> reference -> string list -> string -> unit val extract_inductive : reference -> string -> string list -> string option -> unit -val extraction_implicit : reference -> int list -> unit + + +type int_or_id = ArgInt of int | ArgId of identifier +val extraction_implicit : reference -> int_or_id list -> unit (*s Table of blacklisted filenames *) |