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 /kernel/nativecode.ml | |
| 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 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions