diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-01 20:16:18 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-01 20:17:49 +0200 |
| commit | d1c71b1f3b11e2eb29a5898610d6128b7d535337 (patch) | |
| tree | a0e662edaa5c8c0d17feef652876b2a2166288f2 /tactics/auto.mli | |
| parent | 785f82ee1ecd9a4500ce3e8f3f42946b8205c065 (diff) | |
Made Tacsubst independent of Auto at linking time so that Tacenv does
not draw Auto.
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 5fde1d2de..26dcee8cc 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 *) |