diff options
Diffstat (limited to 'gramlib/gramext.mli')
| -rw-r--r-- | gramlib/gramext.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli index e888508277..8361e21645 100644 --- a/gramlib/gramext.mli +++ b/gramlib/gramext.mli @@ -59,7 +59,6 @@ val levels_of_rules : list -> 'te g_level list val srules : ('te g_symbol list * g_action) list -> 'te g_symbol -external action : 'a -> g_action = "%identity" val eq_symbol : 'a g_symbol -> 'a g_symbol -> bool val delete_rule_in_level_list : |