diff options
| author | Emilio Jesus Gallego Arias | 2016-08-19 02:35:47 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2016-08-19 02:46:38 +0200 |
| commit | fc579fdc83b751a44a18d2373e86ab38806e7306 (patch) | |
| tree | b325c2ff65c505ad62ac7b3fce6bce28633a60f0 /plugins/syntax/numbers_syntax.ml | |
| parent | 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 (diff) | |
Make the user_err header an optional parameter.
Suggested by @ppedrot
Diffstat (limited to 'plugins/syntax/numbers_syntax.ml')
| -rw-r--r-- | plugins/syntax/numbers_syntax.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index ac28714f5c..a25ddb0622 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -100,7 +100,7 @@ let int31_of_pos_bigint dloc n = GApp (dloc, ref_construct, List.rev (args 31 n)) let error_negative dloc = - CErrors.user_err ~loc:dloc "interp_int31" (Pp.str "int31 are only non-negative numbers.") + CErrors.user_err ~loc:dloc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.") let interp_int31 dloc n = if is_pos_or_zero n then @@ -189,7 +189,7 @@ let bigN_of_pos_bigint dloc n = GApp (dloc, ref_constructor, args) let bigN_error_negative dloc = - CErrors.user_err ~loc:dloc "interp_bigN" (Pp.str "bigN are only non-negative numbers.") + CErrors.user_err ~loc:dloc ~hdr:"interp_bigN" (Pp.str "bigN are only non-negative numbers.") let interp_bigN dloc n = if is_pos_or_zero n then |