Make the user_err header an optional parameter.

Suggested by @ppedrot

1 files changed, 5 insertions, 5 deletions

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)