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, 1 insertions, 1 deletions
diff --git a/library/impargs.mli b/library/impargs.mli
index 1670a2385..e0e362369 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -36,7 +36,7 @@ type implicit_status
type implicits_list = implicit_status list
val is_status_implicit : implicit_status -> bool
-val is_inferable_implicit : int -> implicit_status -> bool
+val is_inferable_implicit : bool -> int -> implicit_status -> bool
val positions_of_implicits : implicits_list -> int list
(* Computation of the positions of arguments automatically inferable