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/g_proofs.mlg | |
| 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/g_proofs.mlg')
| -rw-r--r-- | vernac/g_proofs.mlg | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index 058fa691ee..e84fce5504 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -14,6 +14,7 @@ open Glob_term open Constrexpr open Vernacexpr open Hints +open ComHints open Pcoq open Pcoq.Prim |