diff options
| author | Jason Gross | 2018-08-31 17:01:43 -0400 |
|---|---|---|
| committer | Jason Gross | 2018-08-31 20:05:55 -0400 |
| commit | 17cb475550a0f4efe9f3f4c58fdbd9039f5fdd68 (patch) | |
| tree | 7a9ef8ae3a878dd1e29a176d45c552da006379fb /plugins/syntax/plugin_base.dune | |
| parent | 31d58c9ee979699e733a561ec4eef6b0829fe73a (diff) | |
Give a proper error message on num-not in functor
Numeral Notations are not well-supported inside functors. We now give a
proper error message rather than an anomaly when this occurs.
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions