diff options
| author | Pierre-Marie Pédrot | 2018-11-30 15:04:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-12-05 17:58:01 +0100 |
| commit | 3edf9e19972a11eb652ed2fb9a8288d005dc2927 (patch) | |
| tree | 1749d7e0f98253d231935c512faf3ec1b8f913a7 /gramlib/gramext.mli | |
| parent | c03c4ea72e920bf69f29b9ef48c7be64c504d293 (diff) | |
Remove the Like level modifier from gramlib.
Apart from the fact we did not use it, its semantics was somewhat flaky as
it was looking for any rule containing some token.
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 -> |