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 /plugins | |
| 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 'plugins')
| -rw-r--r-- | plugins/ltac/g_ltac.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index e713ab13b2..5baa23b3e9 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -342,7 +342,7 @@ GRAMMAR EXTEND Gram hint: [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>"; tac = Pltac.tactic -> - { Hints.HintsExtern (n,c, in_tac tac) } ] ] + { ComHints.HintsExtern (n,c, in_tac tac) } ] ] ; operconstr: LEVEL "0" [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> |