Make the user_err header an optional parameter.

Suggested by @ppedrot

8 files changed, 37 insertions, 37 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 0ee13bb63..fad656223 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -155,7 +155,7 @@ let error_incompatible_inst clenv mv  =
   let na = meta_name clenv.evd mv in
   match na with
       Name id ->
-        user_err "clenv_assign"
+        user_err ~hdr:"clenv_assign"
           (str "An incompatible instantiation has already been found for " ++
            pr_id id)
     | _ ->
@@ -417,11 +417,11 @@ let qhyp_eq h1 h2 = match h1, h2 with
 let check_bindings bl =
   match List.duplicates qhyp_eq (List.map pi2 bl) with
     | NamedHyp s :: _ ->
-	user_err ""
+	user_err 
 	  (str "The variable " ++ pr_id s ++
 	   str " occurs more than once in binding list.");
     | AnonHyp n :: _ ->
-	user_err ""
+	user_err 
 	  (str "The position " ++ int n ++
 	   str " occurs more than once in binding list.")
     | [] -> ()
@@ -435,7 +435,7 @@ let explain_no_such_bound_variable evd id =
     if na != Anonymous then out_name na :: l else l
   in
   let mvl = List.fold_left fold [] (Evd.meta_list evd) in
-  user_err "Evd.meta_with_name"
+  user_err ~hdr:"Evd.meta_with_name"
     (str"No such bound variable " ++ pr_id id ++
      (if mvl == [] then str " (no bound variables at all in the expression)."
       else
@@ -460,7 +460,7 @@ let meta_with_name evd id =
     | ([n],_|_,[n]) ->
         n
     | _  ->
-        user_err "Evd.meta_with_name"
+        user_err ~hdr:"Evd.meta_with_name"
           (str "Binder name \"" ++ pr_id id ++
            strbrk "\" occurs more than once in clause.")
 
@@ -469,12 +469,12 @@ let meta_of_binder clause loc mvs = function
   | AnonHyp n ->
       try List.nth mvs (n-1)
       with (Failure _|Invalid_argument _) ->
-        user_err "" (str "No such binder.")
+        user_err  (str "No such binder.")
 
 let error_already_defined b =
   match b with
     | NamedHyp id ->
-        user_err ""
+        user_err 
           (str "Binder name \"" ++ pr_id id ++
            str"\" already defined with incompatible value.")
     | AnonHyp n ->
@@ -527,7 +527,7 @@ let clenv_constrain_last_binding c clenv =
   clenv_assign_binding clenv k c
 
 let error_not_right_number_missing_arguments n =
-  user_err ""
+  user_err 
     (strbrk "Not the right number of missing arguments (expected " ++
       int n ++ str ").")
 
@@ -641,7 +641,7 @@ let explain_no_such_bound_variable holes id =
   | [id] -> str "(possible name is: " ++ pr_id id ++ str ")."
   | _ -> str "(possible names are: " ++ pr_enum pr_id mvl ++ str ")."
   in
-  user_err "" (str "No such bound variable " ++ pr_id id ++ expl)
+  user_err  (str "No such bound variable " ++ pr_id id ++ expl)
 
 let evar_with_name holes id =
   let map h = match h.hole_name with
@@ -653,7 +653,7 @@ let evar_with_name holes id =
   | [] -> explain_no_such_bound_variable holes id
   | [h] -> h.hole_evar
   | _ ->
-    user_err ""
+    user_err 
       (str "Binder name \"" ++ pr_id id ++
         str "\" occurs more than once in clause.")
 
@@ -664,7 +664,7 @@ let evar_of_binder holes = function
     let h = List.nth holes (pred n) in
     h.hole_evar
   with e when CErrors.noncritical e ->
-    user_err "" (str "No such binder.")
+    user_err  (str "No such binder.")
 
 let define_with_type sigma env ev c =
   let t = Retyping.get_type_of env sigma ev in
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index ce216e563..ff0df9179 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -54,7 +54,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
       env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc
     with e when CErrors.noncritical e ->
       let loc = Glob_ops.loc_of_glob_constr rawc in
-      user_err ~loc ""
+      user_err ~loc 
                 (str "Instance is not well-typed in the environment of " ++
                  pr_existential_key sigma evk ++ str ".")
   in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 9f34f5cf6..3e77bef7e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -151,7 +151,7 @@ let reorder_context env sign ord =
       | top::ord' when mem_q top moved_hyps ->
           let ((d,h),mh) = find_q top moved_hyps in
           if occur_vars_in_decl env h d then
-            user_err "reorder_context"
+            user_err ~hdr:"reorder_context"
               (str "Cannot move declaration " ++ pr_id top ++ spc() ++
               str "before " ++
               pr_sequence pr_id
@@ -182,7 +182,7 @@ let check_decl_position env sign d =
   let needed = global_vars_set_of_decl env d in
   let deps = dependency_closure env (named_context_of_val sign) needed in
   if Id.List.mem x deps then
-    user_err "Logic.check_decl_position"
+    user_err ~hdr:"Logic.check_decl_position"
       (str "Cannot create self-referring hypothesis " ++ pr_id x);
   x::deps
 
@@ -252,7 +252,7 @@ let move_hyp toleft (left,declfrom,right) hto =
 	    if not (move_location_eq hto (MoveAfter hyp)) then
 	      (first, d::middle)
             else
-	      user_err "move_hyp" (str "Cannot move " ++ pr_id (get_id declfrom) ++
+	      user_err ~hdr:"move_hyp" (str "Cannot move " ++ pr_id (get_id declfrom) ++
 	        Miscprint.pr_move_location pr_id hto ++
 	        str (if toleft then ": it occurs in " else ": it depends on ")
 	        ++ pr_id hyp ++ str ".")
@@ -287,7 +287,7 @@ let move_hyp toleft (left,declfrom,right) hto =
 variables only in Application and Case *)
 
 let error_unsupported_deep_meta c =
-  user_err "" (strbrk "Application of lemmas whose beta-iota normal " ++
+  user_err  (strbrk "Application of lemmas whose beta-iota normal " ++
     strbrk "form contains metavariables deep inside the term is not " ++
     strbrk "supported; try \"refine\" instead.")
 
@@ -498,10 +498,10 @@ let convert_hyp check sign sigma d =
         let _,c,ct = to_tuple d' in
         let env = Global.env_of_context sign in
         if check && not (is_conv env sigma bt ct) then
-	  user_err "Logic.convert_hyp"
+	  user_err ~hdr:"Logic.convert_hyp"
             (str "Incorrect change of the type of " ++ pr_id id ++ str ".");
         if check && not (Option.equal (is_conv env sigma) b c) then
-	  user_err "Logic.convert_hyp"
+	  user_err ~hdr:"Logic.convert_hyp"
             (str "Incorrect change of the body of "++ pr_id id ++ str ".");
        if check then reorder := check_decl_position env sign d;
        d) in
@@ -534,7 +534,7 @@ let prim_refiner r sigma goal =
 	      t,cl,sigma
 	  else
             (if !check && mem_named_context id (named_context_of_val sign) then
-	      user_err "Logic.prim_refiner"
+	      user_err ~hdr:"Logic.prim_refiner"
                 (str "Variable " ++ pr_id id ++ str " is already declared.");
 	     push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in
         let (sg2,ev2,sigma) = 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index b86582def..86c2b7a57 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -131,7 +131,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
     | CList.IndexOutOfRange ->
         match gi with
 	| Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in
-	                            CErrors.user_err "" msg
+	                            CErrors.user_err  msg
         | _ -> assert false
 
 let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
@@ -228,7 +228,7 @@ let solve_by_implicit_tactic env sigma evk =
       when
 	Context.Named.equal (Environ.named_context_of_val evi.evar_hyps)
 	(Environ.named_context env) ->
-      let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError ("",Pp.str"Proof is not complete."))) []) in
+      let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in
       (try
         let c = Evarutil.nf_evars_universes sigma evi.evar_concl in
         if Evarutil.has_undefined_evars sigma c then raise Exit;
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 2e5330b4b..16278b456 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -68,9 +68,9 @@ let _ = CErrors.register_handler begin function
   | CannotUnfocusThisWay ->
     CErrors.error "This proof is focused, but cannot be unfocused this way"
   | NoSuchGoals (i,j) when Int.equal i j ->
-      CErrors.user_err "Focus" Pp.(str"No such goal (" ++ int i ++ str").")
+      CErrors.user_err ~hdr:"Focus" Pp.(str"No such goal (" ++ int i ++ str").")
   | NoSuchGoals (i,j) ->
-      CErrors.user_err "Focus" Pp.(
+      CErrors.user_err ~hdr:"Focus" Pp.(
         str"Not every goal in range ["++ int i ++ str","++int j++str"] exist."
       )
   | FullyUnfocused -> CErrors.error "The proof is not focused"
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 107a3a7e5..da0af3c62 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -203,7 +203,7 @@ let discard (loc,id) =
   discard_gen id;
   if Int.equal (List.length !pstates) n then
     CErrors.user_err ~loc
-      "Pfedit.delete_proof" (str"No such proof" ++ msg_proofs ())
+      ~hdr:"Pfedit.delete_proof" (str"No such proof" ++ msg_proofs ())
 
 let discard_current () =
   if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates
@@ -408,7 +408,7 @@ let return_proof ?(allow_partial=false) () =
   let evd =
     let error s =
       let prf = str " (in proof " ++ Id.print pid ++ str ")" in
-      raise (CErrors.UserError("last tactic before Qed",s ++ prf))
+      raise (CErrors.UserError(Some "last tactic before Qed",s ++ prf))
     in
     try Proof.return proof with
     | Proof.UnfinishedProof ->
@@ -519,7 +519,7 @@ module Bullet = struct
 	(function
 	| FailedBullet (b,sugg) ->
 	  let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in
-	  CErrors.user_err "Focus" (prefix ++ suggest_on_error sugg)
+	  CErrors.user_err ~hdr:"Focus" (prefix ++ suggest_on_error sugg)
 	| _ -> raise CErrors.Unhandled)
 
 
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)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 65a889882..3e59631b7 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -60,7 +60,7 @@ let tclIDTAC_MESSAGE s gls =
   Feedback.msg_info (hov 0 s); tclIDTAC gls
 
 (* General failure tactic *)
-let tclFAIL_s s gls = user_err "Refiner.tclFAIL_s" (str s)
+let tclFAIL_s s gls = user_err ~hdr:"Refiner.tclFAIL_s" (str s)
 
 (* A special exception for levels for the Fail tactic *)
 exception FailError of int * std_ppcmds Lazy.t
@@ -82,7 +82,7 @@ let thens3parts_tac tacfi tac tacli (sigr,gs) =
   let nf = Array.length tacfi in
   let nl = Array.length tacli in
   let ng = List.length gs in
-  if ng<nf+nl then user_err "Refiner.thensn_tac" (str "Not enough subgoals.");
+  if ng<nf+nl then user_err ~hdr:"Refiner.thensn_tac" (str "Not enough subgoals.");
   let gll =
       (List.map_i (fun i ->
         apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
@@ -164,14 +164,14 @@ the goal unchanged *)
 let tclWEAK_PROGRESS tac ptree =
   let rslt = tac ptree in
   if Goal.V82.weak_progress rslt ptree then rslt
-  else user_err "Refiner.WEAK_PROGRESS" (str"Failed to progress.")
+  else user_err ~hdr:"Refiner.WEAK_PROGRESS" (str"Failed to progress.")
 
 (* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
 the goal unchanged *)
 let tclPROGRESS tac ptree =
   let rslt = tac ptree in
   if Goal.V82.progress rslt ptree then rslt
-  else user_err "Refiner.PROGRESS" (str"Failed to progress.")
+  else user_err ~hdr:"Refiner.PROGRESS" (str"Failed to progress.")
 
 (* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals,
    one of them being identical to the original goal *)
@@ -182,7 +182,7 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
   let rslt = tac goal in
   let {it=gls;sigma=sigma} = rslt in
   if List.exists (same_goal goal sigma) gls
-  then user_err "Refiner.tclNOTSAMEGOAL"
+  then user_err ~hdr:"Refiner.tclNOTSAMEGOAL"
       (str"Tactic generated a subgoal identical to the original goal.")
   else rslt
 
@@ -316,7 +316,7 @@ let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl)
 
 let tclDO n t =
   let rec dorec k =
-    if k < 0 then user_err "Refiner.tclDO"
+    if k < 0 then user_err ~hdr:"Refiner.tclDO"
       (str"Wrong argument : Do needs a positive integer.");
     if Int.equal k 0 then tclIDTAC
     else if Int.equal k 1 then t else (tclTHEN t (dorec (k-1)))