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 03b0c77bbe..e888508277 100644 --- a/gramlib/gramext.mli +++ b/gramlib/gramext.mli @@ -34,7 +34,6 @@ and 'te g_symbol = | Sopt of 'te g_symbol | Sself | Snext - | Scut | Stoken of Plexing.pattern | Stree of 'te g_tree and g_action = Obj.t |