diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-21 10:45:28 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-30 18:36:55 +0200 |
| commit | 8b302bfba8f98458087685c8d5fbca2cf647255f (patch) | |
| tree | 7534097143d330c48573aaa9e79e53b0e2dfa66d /vernac/pvernac.mli | |
| parent | 3440a9fcc0690b66ff57a693b61dd6ccb13582c0 (diff) | |
Move interning the [hint_pattern] outside the Typeclasses hooks.
Close #7562.
[api] move hint_info ast to tactics.
Diffstat (limited to 'vernac/pvernac.mli')
| -rw-r--r-- | vernac/pvernac.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli index 9d999793e..2993a1661 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -25,7 +25,7 @@ module Vernac_ : val noedit_mode : vernac_expr Gram.entry val command_entry : vernac_expr Gram.entry val red_expr : raw_red_expr Gram.entry - val hint_info : Typeclasses.hint_info_expr Gram.entry + val hint_info : Hints.hint_info_expr Gram.entry end (** The main entry: reads an optional vernac command *) |