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 /CREDITS | |
| parent | 3440a9fcc0690b66ff57a693b61dd6ccb13582c0 (diff) | |
Move interning the [hint_pattern] outside the Typeclasses hooks.
Close #7562.
[api] move hint_info ast to tactics.
Diffstat (limited to 'CREDITS')
0 files changed, 0 insertions, 0 deletions