Merge PR #244.

8 files changed, 39 insertions, 39 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 0a90e0dbd3..fad656223a 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 ->
-        errorlabstrm "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 :: _ ->
-	errorlabstrm ""
+	user_err 
 	  (str "The variable " ++ pr_id s ++
 	   str " occurs more than once in binding list.");
     | AnonHyp n :: _ ->
-	errorlabstrm ""
+	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
-  errorlabstrm "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
     | _  ->
-        errorlabstrm "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 _) ->
-        errorlabstrm "" (str "No such binder.")
+        user_err  (str "No such binder.")
 
 let error_already_defined b =
   match b with
     | NamedHyp id ->
-        errorlabstrm ""
+        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 =
-  errorlabstrm ""
+  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
-  errorlabstrm "" (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
   | _ ->
-    errorlabstrm ""
+    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 ->
-    errorlabstrm "" (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 5f0cc73d2c..ff0df9179f 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -54,8 +54,8 @@ 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
-        (loc,"", str "Instance is not well-typed in the environment of " ++
+      user_err ~loc 
+                (str "Instance is not well-typed in the environment of " ++
                  pr_existential_key sigma evk ++ str ".")
   in
   define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e12fe5d70a..5aba6b614f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -153,7 +153,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
-            errorlabstrm "reorder_context"
+            user_err ~hdr:"reorder_context"
               (str "Cannot move declaration " ++ pr_id top ++ spc() ++
               str "before " ++
               pr_sequence pr_id
@@ -184,7 +184,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
-    errorlabstrm "Logic.check_decl_position"
+    user_err ~hdr:"Logic.check_decl_position"
       (str "Cannot create self-referring hypothesis " ++ pr_id x);
   x::deps
 
@@ -254,7 +254,7 @@ let move_hyp toleft (left,declfrom,right) hto =
 	    if not (move_location_eq hto (MoveAfter hyp)) then
 	      (first, d::middle)
             else
-	      errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id (NamedDecl.get_id declfrom) ++
+	      user_err ~hdr:"move_hyp" (str "Cannot move " ++ pr_id (NamedDecl.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 ".")
@@ -289,7 +289,7 @@ let move_hyp toleft (left,declfrom,right) hto =
 variables only in Application and Case *)
 
 let error_unsupported_deep_meta c =
-  errorlabstrm "" (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.")
 
@@ -501,10 +501,10 @@ let convert_hyp check sign sigma d =
         let c = NamedDecl.get_value d' in
         let env = Global.env_of_context sign in
         if check && not (is_conv env sigma (NamedDecl.get_type d) (NamedDecl.get_type d')) then
-	  errorlabstrm "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
-	  errorlabstrm "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
@@ -537,7 +537,7 @@ let prim_refiner r sigma goal =
 	      t,cl,sigma
 	  else
             (if !check && mem_named_context id (named_context_of_val sign) then
-	      errorlabstrm "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 e4bae20128..86c2b7a573 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.errorlabstrm "" 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 5fe29653d3..16278b456a 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.errorlabstrm "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.errorlabstrm "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 17cc928030..f3ca19a903 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -204,8 +204,8 @@ let discard (loc,id) =
   let n = List.length !pstates in
   discard_gen id;
   if Int.equal (List.length !pstates) n then
-    CErrors.user_err_loc
-      (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ())
+    CErrors.user_err ~loc
+      ~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
@@ -410,7 +410,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 ->
@@ -521,7 +521,7 @@ module Bullet = struct
 	(function
 	| FailedBullet (b,sugg) ->
 	  let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in
-	  CErrors.errorlabstrm "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 8a9ce4f944..41ad7d94e5 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 _ ->
-            errorlabstrm "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 errorlabstrm "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 errorlabstrm "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 errorlabstrm "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 ->
-	   errorlabstrm "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 fdd0df4457..9a0b56b84b 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -61,7 +61,7 @@ let tclIDTAC_MESSAGE s gls =
   Feedback.msg_info (hov 0 s); tclIDTAC gls
 
 (* General failure tactic *)
-let tclFAIL_s s gls = errorlabstrm "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
@@ -83,7 +83,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 errorlabstrm "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))
@@ -165,14 +165,14 @@ the goal unchanged *)
 let tclWEAK_PROGRESS tac ptree =
   let rslt = tac ptree in
   if Goal.V82.weak_progress rslt ptree then rslt
-  else errorlabstrm "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 errorlabstrm "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 *)
@@ -183,7 +183,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 errorlabstrm "Refiner.tclNOTSAMEGOAL"
+  then user_err ~hdr:"Refiner.tclNOTSAMEGOAL"
       (str"Tactic generated a subgoal identical to the original goal.")
   else rslt
 
@@ -317,7 +317,7 @@ let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl)
 
 let tclDO n t =
   let rec dorec k =
-    if k < 0 then errorlabstrm "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)))