diff options
Diffstat (limited to 'tactics/auto.mli')
| -rw-r--r-- | tactics/auto.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli index 5fe5ebb86..a8d8cf1df 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -118,10 +118,11 @@ val make_extern : -> constr_label * pri_auto_tactic val set_extern_interp : - ((int * constr) list -> Tacexpr.glob_tactic_expr -> tactic) -> unit + (patvar_map -> Tacexpr.glob_tactic_expr -> tactic) -> unit val set_extern_intern_tac : - (int list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) -> unit + (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) + -> unit val set_extern_subst_tactic : (Names.substitution -> Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_expr) |