diff options
| author | Emilio Jesus Gallego Arias | 2018-11-24 21:22:49 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-27 15:21:50 +0100 |
| commit | 9703ac1003b7c64fec624f1e7d4407f84fdea873 (patch) | |
| tree | 7621ce4f47844862a60004e870e6654a5bd86a89 /gramlib/gramext.mli | |
| parent | 786a522c18aa39a6d1d8312bd70132dfbfd16df6 (diff) | |
[gramlib] Remove unused function `gram_reinit`.
Diffstat (limited to 'gramlib/gramext.mli')
| -rw-r--r-- | gramlib/gramext.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli index a9c20d012b..ecb95ec61b 100644 --- a/gramlib/gramext.mli +++ b/gramlib/gramext.mli @@ -53,13 +53,13 @@ type position = | Like of string | Level of string -val levels_of_rules : warning:bool -> +val levels_of_rules : warning:(string -> unit) option -> 'te g_entry -> position option -> (string option * g_assoc option * ('te g_symbol list * g_action) list) list -> 'te g_level list -val srules : warning:bool -> ('te g_symbol list * g_action) list -> 'te g_symbol +val srules : warning:(string -> unit) option -> ('te g_symbol list * g_action) list -> 'te g_symbol val eq_symbol : 'a g_symbol -> 'a g_symbol -> bool val delete_rule_in_level_list : |