diff options
Diffstat (limited to 'plugins/ltac/tacinterp.mli')
| -rw-r--r-- | plugins/ltac/tacinterp.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 494f36a95a..2ec45312ea 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -110,7 +110,7 @@ val interp_int : interp_sign -> Id.t Loc.located -> int val interp_int_or_var : interp_sign -> int or_var -> int -val error_ltac_variable : Loc.t -> Id.t -> +val error_ltac_variable : ?loc:Loc.t -> Id.t -> (Environ.env * Evd.evar_map) option -> value -> string -> 'a (** Transforms a constr-expecting tactic into a tactic finding its arguments in |