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 7fad01c6a4..f1e294fb4c 100644 --- a/gramlib/gramext.mli +++ b/gramlib/gramext.mli @@ -50,7 +50,6 @@ type position = | Last | Before of string | After of string - | Like of string | Level of string val levels_of_rules : warning:(string -> unit) option -> |