diff options
Diffstat (limited to 'parsing/egrammar.mli')
| -rw-r--r-- | parsing/egrammar.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index e1f4dc6b1..47b8beced 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -22,7 +22,10 @@ type all_grammar_command = (int * Gramext.g_assoc option * notation * prod_item list * int list option) | Grammar of grammar_command - | TacticGrammar of (string * (string * grammar_production list) * Tacexpr.raw_tactic_expr) list + | TacticGrammar of + (string * (string * grammar_production list) * + (Names.dir_path * Tacexpr.raw_tactic_expr)) + list val extend_grammar : all_grammar_command -> unit |