diff options
Diffstat (limited to 'parsing/egrammar.mli')
| -rw-r--r-- | parsing/egrammar.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index 091f98424..caa144ce9 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -50,3 +50,6 @@ val reset_extend_grammars_v8 : unit -> unit val subst_all_grammar_command : Names.substitution -> all_grammar_command -> all_grammar_command + +val interp_entry_name : string -> string -> + entry_type * Token.t Gramext.g_symbol |