From fc579fdc83b751a44a18d2373e86ab38806e7306 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Aug 2016 02:35:47 +0200 Subject: Make the user_err header an optional parameter. Suggested by @ppedrot --- plugins/syntax/ascii_syntax.ml | 2 +- plugins/syntax/nat_syntax.ml | 2 +- plugins/syntax/numbers_syntax.ml | 4 ++-- plugins/syntax/z_syntax.ml | 4 ++-- 4 files changed, 6 insertions(+), 6 deletions(-) (limited to 'plugins/syntax') diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index c6fe553c5..ed8cc6ab0 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -52,7 +52,7 @@ let interp_ascii_string dloc s = if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2] then int_of_string s else - user_err ~loc:dloc "interp_ascii_string" + user_err ~loc:dloc ~hdr:"interp_ascii_string" (str "Expects a single character or a three-digits ascii code.") in interp_ascii dloc p diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 6d62496ee..ab262fea7 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -47,7 +47,7 @@ let nat_of_int dloc n = mk_nat ref_O n end else - user_err "nat_of_int" + user_err ~hdr:"nat_of_int" (str "Cannot interpret a negative number as a number of type nat") (************************************************************************) diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index ac28714f5..a25ddb062 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 diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 851ea3b74..b7b5fb8a5 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -57,7 +57,7 @@ let pos_of_bignat dloc x = pos_of x let error_non_positive dloc = - user_err ~loc:dloc "interp_positive" + user_err ~loc:dloc ~hdr:"interp_positive" (str "Only strictly positive numbers in type \"positive\".") let interp_positive dloc n = @@ -113,7 +113,7 @@ let n_of_binnat dloc pos_or_neg n = GRef (dloc, glob_N0, None) let error_negative dloc = - user_err ~loc:dloc "interp_N" (str "No negative numbers in type \"N\".") + user_err ~loc:dloc ~hdr:"interp_N" (str "No negative numbers in type \"N\".") let n_of_int dloc n = if is_pos_or_zero n then n_of_binnat dloc true n -- cgit v1.2.3