diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egrammar.ml | 3 | ||||
| -rw-r--r-- | parsing/egrammar.mli | 5 |
2 files changed, 6 insertions, 2 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 5880c0263b..25333b6848 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -26,7 +26,8 @@ type all_grammar_command = int list option) | Grammar of grammar_command | TacticGrammar of - (string * (string * grammar_production list) * Tacexpr.raw_tactic_expr) + (string * (string * grammar_production list) * + (Names.dir_path * Tacexpr.raw_tactic_expr)) list let subst_all_grammar_command subst = function diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index e1f4dc6b10..47b8beced3 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 |