diff options
| author | Jason Gross | 2018-09-19 09:32:15 -0400 |
|---|---|---|
| committer | Jason Gross | 2018-09-19 18:43:02 -0400 |
| commit | 4888eb7ea720eaa34af8df2769fa300f1ea37173 (patch) | |
| tree | c0776bc016413ba89d226d8fd9828a2d6c47be5e /plugins/syntax/string_syntax.ml | |
| parent | e39c84ff2dc20ce059ee6198e142ca076de8c6cb (diff) | |
Fix Numeral Notations (2/4 - exceptions, usr_err)
Switch to using exceptions rather than user errors. This will be
required because the machinery for printing constrs is not available in
notation.ml, so we move the error message printing to himsg.ml instead.
This is commit 2/4 in the fix for #8401.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions