diff options
| author | coqbot-app[bot] | 2020-08-31 12:09:18 +0000 |
|---|---|---|
| committer | GitHub | 2020-08-31 12:09:18 +0000 |
| commit | daca83946ed5a001f2461fefa787a80f7dcdea01 (patch) | |
| tree | 0a746f4f5496290ca18c5d92d57cb7d3a9c89065 /interp/impargs.mli | |
| parent | b4ff2af4f43a2e0ba40c7f8a6260da1c75859045 (diff) | |
| parent | 8262041215c9bc3d13e768b1c422b52005083e85 (diff) | |
Merge PR #12875: Further extensions of About wrt Arguments and renaming
Reviewed-by: SkySkimmer
Ack-by: herbelin
Diffstat (limited to 'interp/impargs.mli')
| -rw-r--r-- | interp/impargs.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/impargs.mli b/interp/impargs.mli index 97841b37f2..c8bcef19c8 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -117,7 +117,7 @@ val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool -> (** [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 -> Glob_term.binding_kind list list -> unit +val set_implicits : bool -> GlobRef.t -> (Name.t * Glob_term.binding_kind) list list -> unit val implicits_of_global : GlobRef.t -> implicits_list list |