diff options
| author | Emilio Jesus Gallego Arias | 2020-04-18 20:22:13 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-21 08:39:12 +0200 |
| commit | 688a0869f6b8ab3048a545f821f45bc5599ba63b (patch) | |
| tree | 057e56abc232ccaeac63723f9add8f969e67393c /vernac/pvernac.mli | |
| parent | c30594f55750996398eb3947838eaf1f906f08c9 (diff) | |
[hints] Move and split Hint Declaration AST to vernac
This moves the vernacular part of hints to `vernac`; in particular, it
helps removing the declaration of constants as parts of the `tactic`
folder.
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 4de12f5e3b..2b6beaf2e3 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -28,7 +28,7 @@ module Vernac_ : val command_entry : vernac_expr Entry.t val main_entry : vernac_control option Entry.t val red_expr : raw_red_expr Entry.t - val hint_info : Hints.hint_info_expr Entry.t + val hint_info : ComHints.hint_info_expr Entry.t end (* To be removed when the parser is made functional wrt the tactic |