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 /pretyping/typeclasses_errors.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 'pretyping/typeclasses_errors.mli')
0 files changed, 0 insertions, 0 deletions