diff options
| author | Paolo G. Giarrusso | 2020-07-11 18:10:18 +0200 |
|---|---|---|
| committer | GitHub | 2020-07-11 18:10:18 +0200 |
| commit | f91f2ac64fbc7035c77592195c67050640abc3cb (patch) | |
| tree | 722f93abd2f359bc51ea616cfa514558644430dc /dev | |
| parent | f4593ab277c12eda7e000011eeb2276716ac9a09 (diff) | |
tactics.rst: `Require A` is enough for `A`'s hints
As the text says later:
> Hints should only be made available when the module they are defined in is imported, not just required.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions