diff options
Diffstat (limited to 'ltac/tacinterp.mli')
| -rw-r--r-- | ltac/tacinterp.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/tacinterp.mli b/ltac/tacinterp.mli index 6f64981ef..adbd1d32b 100644 --- a/ltac/tacinterp.mli +++ b/ltac/tacinterp.mli @@ -115,7 +115,7 @@ val error_ltac_variable : Loc.t -> Id.t -> (** Transforms a constr-expecting tactic into a tactic finding its arguments in the Ltac environment according to the given names. *) -val lift_constr_tac_to_ml_tac : Id.t option list -> +val lift_constr_tac_to_ml_tac : Name.t list -> (constr list -> Geninterp.interp_sign -> unit Proofview.tactic) -> Tacenv.ml_tactic val default_ist : unit -> Geninterp.interp_sign |