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 66d72abbb..de8d89166 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -95,7 +95,7 @@ type manual_implicits = manual_explicitation list
val compute_implicits_with_manual : env -> types -> bool ->
manual_implicits -> implicit_status list
-val compute_implicits_names : env -> types -> name list
+val compute_implicits_names : env -> types -> Name.t list
(** {6 Computation of implicits (done using the global environment). } *)