diff options
Diffstat (limited to 'tactics/hints.mli')
| -rw-r--r-- | tactics/hints.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index 6f5ee8ba5..6d5342e00 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -210,7 +210,7 @@ val run_hint : hint -> val repr_hint : hint -> (raw_hint * clausenv) hint_ast val extern_intern_tac : - (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t + (patvar list -> Genarg.raw_generic_argument -> Tacexpr.glob_tactic_expr) Hook.t (** Create a Hint database from the pairs (name, constr). Useful to take the current goal hypotheses as hints; |