aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/impargs.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/impargs.mli')
-rw-r--r--library/impargs.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/library/impargs.mli b/library/impargs.mli
index e0e362369..83ca8dfb9 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -37,6 +37,8 @@ type implicits_list = implicit_status list
val is_status_implicit : implicit_status -> bool
val is_inferable_implicit : bool -> int -> implicit_status -> bool
+val name_of_implicit : implicit_status -> identifier
+
val positions_of_implicits : implicits_list -> int list
(* Computation of the positions of arguments automatically inferable