diff options
| author | Gaëtan Gilbert | 2019-05-05 16:42:36 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-04 09:33:41 +0200 |
| commit | 33b18aaffd999fb6d31fd5e9c7ca4426d5186983 (patch) | |
| tree | 0b0f5efeb5e9cbe2fb3eabaff058e25cf4b5eac9 /plugins/syntax/plugin_base.dune | |
| parent | 1bf2a088387949c13602997d181e6f7d0f014b3f (diff) | |
instance_name grammar entry isn't global
Not needed since we don't allow anonymous Declare Instance
anymore (was needed for factorization or some such before that I think)
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions