diff options
Diffstat (limited to 'tactics/auto.mli')
| -rw-r--r-- | tactics/auto.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli index 5fde1d2de1..26dcee8ccc 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -203,9 +203,6 @@ val extern_interp : val extern_intern_tac : (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t -val extern_subst_tactic : - (substitution -> Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t - (** Create a Hint database from the pairs (name, constr). Useful to take the current goal hypotheses as hints; Boolean tells if lemmas with evars are allowed *) |