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 --- proofs/redexpr.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'proofs/redexpr.ml') diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index cafd46849..41ad7d94e 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -73,7 +73,7 @@ let set_strategy_one ref l = let cb = Global.lookup_constant sp in (match cb.const_body with | OpaqueDef _ -> - user_err "set_transparent_const" + user_err ~hdr:"set_transparent_const" (str "Cannot make" ++ spc () ++ Nametab.pr_global_env Id.Set.empty (ConstRef sp) ++ spc () ++ str "transparent because it was declared opaque."); @@ -175,19 +175,19 @@ let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction" let declare_reduction s f = if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab - then user_err "Redexpr.declare_reduction" + then user_err ~hdr:"Redexpr.declare_reduction" (str "There is already a reduction expression of name " ++ str s) else reduction_tab := String.Map.add s f !reduction_tab let check_custom = function | ExtraRedExpr s -> if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab) - then user_err "Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s) + then user_err ~hdr:"Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s) |_ -> () let decl_red_expr s e = if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab - then user_err "Redexpr.decl_red_expr" + then user_err ~hdr:"Redexpr.decl_red_expr" (str "There is already a reduction expression of name " ++ str s) else begin check_custom e; @@ -247,7 +247,7 @@ let reduction_of_red_expr env = with Not_found -> (try reduction_of_red_expr (String.Map.find s !red_expr_tab) with Not_found -> - user_err "Redexpr.reduction_of_red_expr" + user_err ~hdr:"Redexpr.reduction_of_red_expr" (str "unknown user-defined reduction \"" ++ str s ++ str "\""))) | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast) | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast) -- cgit v1.2.3