diff options
Diffstat (limited to 'interp/impargs.mli')
| -rw-r--r-- | interp/impargs.mli | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/interp/impargs.mli b/interp/impargs.mli index 43c26b024f..0070423530 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -112,13 +112,20 @@ val declare_implicits : bool -> GlobRef.t -> unit Unsets implicits if [l] is empty. *) val declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool -> - manual_implicits list -> unit + manual_implicits -> unit (** If the list is empty, do nothing, otherwise declare the implicits. *) val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool -> manual_implicits -> unit +type implicit_kind = Implicit | MaximallyImplicit | NotImplicit + +(** [set_implicits local ref l] + Manual declaration of implicit arguments. + `l` is a list of possible sequences of implicit statuses. *) +val set_implicits : bool -> GlobRef.t -> implicit_kind list list -> unit + val implicits_of_global : GlobRef.t -> implicits_list list val extract_impargs_data : |