diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-24 18:46:18 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-26 12:58:15 +0200 |
| commit | 81545ec98255e644be589d34a521924549e9e2fa (patch) | |
| tree | 65ab59d21e680a00e379deffa440f038b5d0c121 /tactics/hints.mli | |
| parent | 0f107c8a747af6bdb40d70d80236f84b325dc35d (diff) | |
[api] Move `hint_info_expr` to `Typeclasses`.
`hint_info_expr`, `hint_info_gen` do conceptually belong to the
typeclasses modules and should be able to be used without a dependency
on the concrete vernacular syntax.
Diffstat (limited to 'tactics/hints.mli')
| -rw-r--r-- | tactics/hints.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index 1811150c2..b06ede0e1 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -31,7 +31,7 @@ type debug = Debug | Info | Off val secvars_of_hyps : ('c, 't) Context.Named.pt -> Id.Pred.t -val empty_hint_info : 'a hint_info_gen +val empty_hint_info : 'a Typeclasses.hint_info_gen (** Pre-created hint databases *) @@ -144,7 +144,7 @@ type hint_db = Hint_db.t type hnf = bool -type hint_info = (patvar list * constr_pattern) hint_info_gen +type hint_info = (patvar list * constr_pattern) Typeclasses.hint_info_gen type hint_term = | IsGlobRef of global_reference |