From 688a0869f6b8ab3048a545f821f45bc5599ba63b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 18 Apr 2020 20:22:13 -0400
Subject: [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.
---
 plugins/ltac/g_ltac.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

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; ")" ->
-- 
cgit v1.2.3