aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/impargs.ml2
-rw-r--r--library/impargs.mli2
2 files changed, 2 insertions, 2 deletions
diff --git a/library/impargs.ml b/library/impargs.ml
index db98bb9fd4..bce7a15cbe 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -68,7 +68,7 @@ let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern
let is_contextual_implicit_args () = !implicit_args.contextual
let is_maximal_implicit_args () = !implicit_args.maximal
-let with_implicits f x =
+let with_implicit_protection f x =
let oflags = !implicit_args in
try
let rslt = f x in
diff --git a/library/impargs.mli b/library/impargs.mli
index 327f84d9fa..3919a519c9 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -29,7 +29,7 @@ val is_reversible_pattern_implicit_args : unit -> bool
val is_contextual_implicit_args : unit -> bool
val is_maximal_implicit_args : unit -> bool
-val with_implicits : ('a -> 'b) -> 'a -> 'b
+val with_implicit_protection : ('a -> 'b) -> 'a -> 'b
(** {6 ... } *)
(** An [implicits_list] is a list of positions telling which arguments