aboutsummaryrefslogtreecommitdiff
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 04251f332e..57f1ac71e6 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -87,7 +87,7 @@ val positions_of_implicits : implicits_list -> int list
(** A [manual_explicitation] is a tuple of a positional or named explicitation with
maximal insertion, force inference and force usage flags. Forcing usage makes
the argument implicit even if the automatic inference considers it not inferable. *)
-type manual_explicitation = Topconstr.explicitation *
+type manual_explicitation = Constrexpr.explicitation *
(maximal_insertion * force_inference * bool)
type manual_implicits = manual_explicitation list