aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/table.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/table.mli')
-rw-r--r--plugins/extraction/table.mli5
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 *)