diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-07 18:02:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-08 15:52:56 +0200 |
| commit | dfac5aa2285de5b89f08ada3c30c0a1594737440 (patch) | |
| tree | 37fa3f3481d03c4a777595e1ec0eab631cd528aa /tactics | |
| parent | 13266ce4c37cb648b5e4e391aa5d7486bbcdb4ee (diff) | |
Making Vernacexpr independent from Tacexpr.
Diffstat (limited to 'tactics')
| -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; |