diff options
Diffstat (limited to 'gramlib/gramext.ml')
| -rw-r--r-- | gramlib/gramext.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml index 72468b540e..43a70ca13b 100644 --- a/gramlib/gramext.ml +++ b/gramlib/gramext.ml @@ -149,8 +149,6 @@ let srules rl = in Stree t -external action : 'a -> g_action = "%identity" - let is_level_labelled n lev = match lev.lname with Some n1 -> n = n1 |