Merge PR #244.

10 files changed, 65 insertions, 65 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 4750056480..7628b7885f 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -65,7 +65,7 @@ let raw_find_base bas = String.Map.find bas !rewtab
 let find_base bas =
   try raw_find_base bas
   with Not_found ->
-    errorlabstrm "AutoRewrite"
+    user_err ~hdr:"AutoRewrite"
       (str "Rewriting base " ++ str bas ++ str " does not exist.")
 
 let find_rewrites bas =
@@ -294,8 +294,8 @@ let find_applied_relation metas loc env sigma c left2right =
     match decompose_applied_relation metas env sigma c ctype left2right with
     | Some c -> c
     | None ->
-	user_err_loc (loc, "decompose_applied_relation",
-		     str"The type" ++ spc () ++ Printer.pr_constr_env env sigma ctype ++
+	user_err ~loc ~hdr:"decompose_applied_relation"
+		    (str"The type" ++ spc () ++ Printer.pr_constr_env env sigma ctype ++
 		       spc () ++ str"of this term does not end with an applied relation.")
 
 (* To add rewriting rules to a base *)
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index ba9a2d95c8..ba21950707 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -97,8 +97,8 @@ let prolog_tac l n =
   in
   let l = List.map map l in
   try (prolog l n gl)
-  with UserError ("Refiner.tclFIRST",_) ->
-    errorlabstrm "Prolog.prolog" (str "Prolog failed.")
+  with UserError (Some "Refiner.tclFIRST",_) ->
+    user_err ~hdr:"Prolog.prolog" (str "Prolog failed.")
   end
 
 open Auto
@@ -431,7 +431,7 @@ let cons a l = a :: l
 let autounfolds db occs cls gl =
   let unfolds = List.concat (List.map (fun dbname -> 
     let db = try searchtable_map dbname 
-      with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
+      with Not_found -> user_err ~hdr:"autounfold" (str "Unknown database " ++ str dbname)
     in
     let (ids, csts) = Hint_db.unfolds db in
     let hyps = pf_ids_of_hyps gl in
@@ -498,7 +498,7 @@ let autounfold_one db cl =
   let st =
     List.fold_left (fun (i,c) dbname -> 
       let db = try searchtable_map dbname 
-	with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
+	with Not_found -> user_err ~hdr:"autounfold" (str "Unknown database " ++ str dbname)
       in
       let (ids, csts) = Hint_db.unfolds db in
 	(Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d078532b5d..d4b372837d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -361,7 +361,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
 	      let _ = Global.lookup_constant c1' in
 		c1'
 	    with Not_found -> 
-	      errorlabstrm "Equality.find_elim"
+	      user_err ~hdr:"Equality.find_elim"
                 (str "Cannot find rewrite principle " ++ pr_label l' ++ str ".")
 	  end
 	| _ -> destConstRef pr1
@@ -890,7 +890,7 @@ let build_selector env sigma dirn c ind special default =
           on (c bool true) = (c bool false)
           CP : changed assert false in a more informative error
        *)
-      errorlabstrm "Equality.construct_discriminator"
+      user_err ~hdr:"Equality.construct_discriminator"
 	(str "Cannot discriminate on inductive constructors with \
 		 dependent types.") in
   let (indp,_) = dest_ind_family indf in
@@ -976,7 +976,7 @@ let apply_on_clause (f,t) clause =
   let argmv =
     (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with
      | Meta mv -> mv
-     | _  -> errorlabstrm "" (str "Ill-formed clause applicator.")) in
+     | _  -> user_err  (str "Ill-formed clause applicator.")) in
   clenv_fchain ~with_univs:false argmv f_clause clause
 
 let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
@@ -1054,7 +1054,7 @@ let discrEverywhere with_evars =
      else (* <= 8.2 compat *)
        tryAllHypsAndConcl (discrSimpleClause with_evars))
 (*    (fun gls ->
-       errorlabstrm "DiscrEverywhere" (str"No discriminable equalities."))
+       user_err ~hdr:"DiscrEverywhere" (str"No discriminable equalities."))
 *)
 let discr_tac with_evars = function
   | None -> discrEverywhere with_evars
@@ -1727,7 +1727,7 @@ let subst_one_var dep_proof_ok x =
           let hyps = Proofview.Goal.hyps gl in
           let test hyp _ = is_eq_x gl x hyp in
           Context.Named.fold_outside test ~init:() hyps;
-          errorlabstrm "Subst"
+          user_err ~hdr:"Subst"
             (str "Cannot find any non-recursive equality over " ++ pr_id x ++
 	       str".")
         with FoundHyp res -> res in
diff --git a/tactics/hints.ml b/tactics/hints.ml
index a74fceb8f2..4b43a9e696 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -633,7 +633,7 @@ let current_pure_db () =
   List.map snd (Hintdbmap.bindings (Hintdbmap.remove "v62" !searchtable))
 
 let error_no_such_hint_database x =
-  errorlabstrm "Hints" (str "No such Hint database: " ++ str x ++ str ".")
+  user_err ~hdr:"Hints" (str "No such Hint database: " ++ str x ++ str ".")
 
 (**************************************************************************)
 (*                       Definition of the summary                        *)
@@ -775,7 +775,7 @@ let make_resolves env sigma flags pri poly ?name cr =
     [make_exact_entry env sigma pri poly ?name; make_apply_entry env sigma flags pri poly ?name]
   in
   if List.is_empty ents then
-    errorlabstrm "Hint"
+    user_err ~hdr:"Hint"
       (pr_lconstr c ++ spc() ++
         (if pi1 flags then str"cannot be used as a hint."
 	else str "can be used as a hint only for eauto."));
@@ -818,7 +818,7 @@ let make_mode ref m =
   let n = List.length ctx in
   let m' = Array.of_list m in
     if not (n == Array.length m') then
-      errorlabstrm "Hint"
+      user_err ~hdr:"Hint"
 	(pr_global ref ++ str" has " ++ int n ++ 
 	   str" arguments while the mode declares " ++ int (Array.length m'))
     else m'
@@ -1412,6 +1412,6 @@ let run_hint tac k = match !warn_hint with
   else Proofview.tclBIND (k tac.obj) (fun x -> warn tac x)
 | `STRICT ->
   if is_imported tac then k tac.obj
-  else Proofview.tclZERO (UserError ("", (str "Tactic failure.")))
+  else Proofview.tclZERO (UserError (None, (str "Tactic failure.")))
 
 let repr_hint h = h.obj
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 36770925f0..72c3523da0 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -452,7 +452,7 @@ let find_this_eq_data_decompose gl eqn =
     try (*first_match (match_eq eqn) inversible_equalities*)
       find_eq_data eqn
     with PatternMatchingFailure ->
-      errorlabstrm "" (str "No primitive equality found.") in
+      user_err  (str "No primitive equality found.") in
   let eq_args =
     try extract_eq_args gl eq_args
     with PatternMatchingFailure ->
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 575710ecc9..291bc09650 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -77,7 +77,7 @@ let make_inv_predicate env evd indf realargs id status concl =
 	    (hyps_arity,concl)
       | Dep dflt_concl ->
 	  if not (occur_var env id concl) then
-	    errorlabstrm "make_inv_predicate"
+	    user_err ~hdr:"make_inv_predicate"
               (str "Current goal does not depend on " ++ pr_id id ++ str".");
           (* We abstract the conclusion of goal with respect to
              realargs and c to * be concl in order to rewrite and have
@@ -441,7 +441,7 @@ let raw_inversion inv_kind id status names =
       try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c)
       with UserError _ ->
         let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in
-        CErrors.errorlabstrm "" msg
+        CErrors.user_err  msg
     in
     let IndType (indf,realargs) = find_rectype env sigma t in
     let evdref = ref sigma in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 1639ec54ca..d80e862418 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -185,7 +185,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let ind =
     try find_rectype env sigma i
     with Not_found ->
-      errorlabstrm "inversion_scheme" (no_inductive_inconstr env sigma i)
+      user_err ~hdr:"inversion_scheme" (no_inductive_inconstr env sigma i)
   in
   let (invEnv,invGoal) =
     compute_first_inversion_scheme env sigma ind sort dep_option
@@ -195,7 +195,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
        (global_vars env invGoal)
        (ids_of_named_context (named_context invEnv)));
   (*
-    errorlabstrm "lemma_inversion"
+    user_err ~hdr:"lemma_inversion"
     (str"Computed inversion goal was not closed in initial signature.");
   *)
   let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
@@ -249,8 +249,8 @@ let add_inversion_lemma_exn na com comsort bool tac =
   try
     add_inversion_lemma na env sigma c sort bool tac
   with
-    |   UserError ("Case analysis",s) -> (* Reference to Indrec *)
-	  errorlabstrm "Inv needs Nodep Prop Set" s
+    |   UserError (Some "Case analysis",s) -> (* Reference to Indrec *)
+	  user_err ~hdr:"Inv needs Nodep Prop Set" s
 
 (* ================================= *)
 (* Applying a given inversion lemma  *)
@@ -263,10 +263,10 @@ let lemInv id c gls =
     Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls
   with
     | NoSuchBinding ->
-	errorlabstrm ""
+	user_err 
 	  (hov 0 (pr_constr c ++ spc () ++ str "does not refer to an inversion lemma."))
     | UserError (a,b) ->
-	 errorlabstrm "LemInv"
+	 user_err ~hdr:"LemInv"
 	   (str "Cannot refine current goal with the lemma " ++
 	      pr_lconstr_env (Refiner.pf_env gls) (Refiner.project gls) c)
 
diff --git a/tactics/tactic_matching.ml b/tactics/tactic_matching.ml
index a5ccd500c9..ef45ee47e1 100644
--- a/tactics/tactic_matching.ml
+++ b/tactics/tactic_matching.ml
@@ -105,7 +105,7 @@ let verify_metas_coherence env sigma (ln1,lcm) (ln,lm) =
   (merged, Id.Map.merge merge lcm lm)
 
 let matching_error =
-  CErrors.UserError ("tactic matching" , Pp.str "No matching clauses for match.")
+  CErrors.UserError (Some "tactic matching" , Pp.str "No matching clauses for match.")
 
 let imatching_error = (matching_error, Exninfo.null)
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index ae23071907..203d975428 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -173,14 +173,14 @@ let check_or_and_pattern_size check_and loc names branchsigns =
   let n = Array.length branchsigns in
   let msg p1 p2 = strbrk "a conjunctive pattern made of " ++ int p1 ++ (if p1 == p2 then mt () else str " or " ++ int p2) ++ str " patterns" in
   let err1 p1 p2 =
-    user_err_loc (loc,"",str "Expects " ++ msg p1 p2 ++ str ".") in
+    user_err ~loc  (str "Expects " ++ msg p1 p2 ++ str ".") in
   let errn n =
-    user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n
+    user_err ~loc  (str "Expects a disjunctive pattern with " ++ int n
 	++ str " branches.") in
   let err1' p1 p2 =
-    user_err_loc (loc,"",strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in
+    user_err ~loc  (strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in
   let errforthcoming loc =
-    user_err_loc (loc,"",strbrk "Unexpected non atomic pattern.") in
+    user_err ~loc  (strbrk "Unexpected non atomic pattern.") in
   match names with
   | IntroAndPattern l ->
       if not (Int.equal n 1) then errn n;
@@ -312,7 +312,7 @@ module New = struct
     tclZERO (Refiner.FailError (lvl,lazy msg))
 
   let tclZEROMSG ?loc msg =
-    let err = UserError ("", msg) in
+    let err = UserError (None, msg) in
     let info = match loc with
     | None -> Exninfo.null
     | Some loc -> Loc.add_loc Exninfo.null loc
@@ -509,7 +509,7 @@ module New = struct
     | [] -> ()
     | (evk,evi) :: _ ->
       let (loc,_) = evi.Evd.evar_source in
-      Pretype_errors.error_unsolvable_implicit loc env sigma evk None
+      Pretype_errors.error_unsolvable_implicit ~loc env sigma evk None
 
   let tclWITHHOLES accept_unresolved_holes tac sigma =
     tclEVARMAP >>= fun sigma_initial ->
@@ -644,7 +644,7 @@ module New = struct
 	    | Var id -> string_of_id id
 	    | _ -> "\b"
 	  in
-	  errorlabstrm "Tacticals.general_elim_then_using"
+	  user_err ~hdr:"Tacticals.general_elim_then_using"
             (str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
     in
     let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b54624f897..85b6e8de9e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -185,7 +185,7 @@ let introduction ?(check=true) id =
     let store = Proofview.Goal.extra gl in
     let env = Proofview.Goal.env gl in
     let () = if check && mem_named_context id hyps then
-      errorlabstrm "Tactics.introduction"
+      user_err ~hdr:"Tactics.introduction"
         (str "Variable " ++ pr_id id ++ str " is already declared.")
     in
     let open Context.Named.Declaration in
@@ -258,7 +258,7 @@ let clear_dependency_msg env sigma id = function
       Printer.pr_existential env sigma ev ++ str"."
 
 let error_clear_dependency env sigma id err =
-  errorlabstrm "" (clear_dependency_msg env sigma id err)
+  user_err  (clear_dependency_msg env sigma id err)
 
 let replacing_dependency_msg env sigma id = function
   | Evarutil.OccurHypInSimpleClause None ->
@@ -272,7 +272,7 @@ let replacing_dependency_msg env sigma id = function
       Printer.pr_existential env sigma ev ++ str"."
 
 let error_replacing_dependency env sigma id err =
-  errorlabstrm "" (replacing_dependency_msg env sigma id err)
+  user_err  (replacing_dependency_msg env sigma id err)
 
 (* This tactic enables the user to remove hypotheses from the signature.
  * Some care is taken to prevent him from removing variables that are
@@ -352,7 +352,7 @@ let rename_hyp repl =
       let () =
         try
           let elt = Id.Set.choose (Id.Set.inter dst mods) in
-          CErrors.errorlabstrm "" (pr_id elt ++ str " is already used")
+          CErrors.user_err  (pr_id elt ++ str " is already used")
         with Not_found -> ()
       in
       (** All is well *)
@@ -425,7 +425,7 @@ let find_name mayrepl decl naming gl = match naming with
       let ids_of_hyps = Tacmach.New.pf_ids_of_hyps gl in
       let id' = next_ident_away id ids_of_hyps in
       if not mayrepl && not (Id.equal id' id) then
-        user_err_loc (loc,"",pr_id id ++ str" is already used.");
+        user_err ~loc  (pr_id id ++ str" is already used.");
       id
 
 (**************************************************************)
@@ -510,7 +510,7 @@ let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl ->
     if not (eq_mind sp sp') then
       error "Fixpoints should be on the same mutual inductive declaration.";
     if mem_named_context f (named_context_of_val sign) then
-      errorlabstrm "Logic.prim_refiner"
+      user_err ~hdr:"Logic.prim_refiner"
         (str "Name " ++ pr_id f ++ str " already used in the environment");
     mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
   in
@@ -601,7 +601,7 @@ let pf_reduce_decl redfun where decl gl =
   match decl with
   | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str " has no value.");
+	user_err  (pr_id id ++ str " has no value.");
       LocalAssum (id,redfun' ty)
   | LocalDef (id,b,ty) ->
       let b' = if where != InHypTypeOnly then redfun' b else b in
@@ -702,7 +702,7 @@ let pf_e_reduce_decl redfun where decl gl =
   match decl with
   | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str " has no value.");
+	user_err  (pr_id id ++ str " has no value.");
     let Sigma (ty', sigma, p) = redfun sigma ty in
     Sigma (LocalAssum (id, ty'), sigma, p)
   | LocalDef (id,b,ty) ->
@@ -742,7 +742,7 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigm
   match decl with
   | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str " has no value.");
+	user_err  (pr_id id ++ str " has no value.");
     let Sigma (ty', sigma, p) = (redfun false).e_redfun env sigma ty in
     Sigma (LocalAssum (id, ty'), sigma, p)
   | LocalDef (id,b,ty) ->
@@ -780,12 +780,12 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
         isSort (whd_all env sigma t2)
       then (mayneedglobalcheck := true; sigma)
       else
-        errorlabstrm "convert-check-hyp" (str "Types are incompatible.")
+        user_err ~hdr:"convert-check-hyp" (str "Types are incompatible.")
     else sigma
   end
   else
     if not (isSort (whd_all env sigma t1)) then
-      errorlabstrm "convert-check-hyp" (str "Not a type.")
+      user_err ~hdr:"convert-check-hyp" (str "Not a type.")
     else sigma
 
 (* Now we introduce different instances of the previous tacticals *)
@@ -794,7 +794,7 @@ let change_and_check cv_pb mayneedglobalcheck deep t = { e_redfun = begin fun en
   let sigma = Sigma.to_evar_map sigma in
   let sigma = check_types env sigma mayneedglobalcheck deep t' c in
   let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in
-  if not b then errorlabstrm "convert-check-hyp" (str "Not convertible.");
+  if not b then user_err ~hdr:"convert-check-hyp" (str "Not convertible.");
   Sigma.Unsafe.of_pair (t', sigma)
 end }
 
@@ -888,7 +888,7 @@ let reduce redexp cl =
 let unfold_constr = function
   | ConstRef sp -> unfold_in_concl [AllOccurrences,EvalConstRef sp]
   | VarRef id -> unfold_in_concl [AllOccurrences,EvalVarRef id]
-  | _ -> errorlabstrm "unfold_constr" (str "Cannot unfold a non-constant.")
+  | _ -> user_err ~hdr:"unfold_constr" (str "Cannot unfold a non-constant.")
 
 (*******************************************)
 (*         Introduction tactics            *)
@@ -1081,7 +1081,7 @@ let depth_of_quantified_hypothesis red h gl =
   match lookup_hypothesis_as_renamed_gen red h gl with
     | Some depth -> depth
     | None ->
-        errorlabstrm "lookup_quantified_hypothesis"
+        user_err ~hdr:"lookup_quantified_hypothesis"
           (str "No " ++ msg_quantified_hypothesis h ++
 	  strbrk " in current goal" ++
 	  (if red then strbrk " even after head-reduction" else mt ()) ++
@@ -1230,7 +1230,7 @@ let cut c =
 let error_uninstantiated_metas t clenv =
   let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
   let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta")
-  in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".")
+  in user_err  (str "Cannot find an instance for " ++ pr_id id ++ str".")
 
 let check_unresolved_evars_of_metas sigma clenv =
   (* This checks that Metas turned into Evars by *)
@@ -1363,7 +1363,7 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags
   let indmv =
     (match kind_of_term (nth_arg i elimclause.templval.rebus) with
        | Meta mv -> mv
-       | _  -> errorlabstrm "elimination_clause"
+       | _  -> user_err ~hdr:"elimination_clause"
              (str "The type of elimination clause is not well-formed."))
   in
   let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
@@ -1528,7 +1528,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
     try match List.remove Int.equal indmv (clenv_independent elimclause) with
       | [a] -> a
       | _ -> failwith ""
-    with Failure _ -> errorlabstrm "elimination_clause"
+    with Failure _ -> user_err ~hdr:"elimination_clause"
           (str "The type of elimination clause is not well-formed.") in
   let elimclause'  = clenv_fchain ~flags indmv elimclause indclause in
   let hyp = mkVar id in
@@ -1537,7 +1537,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
   let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in
   let new_hyp_typ  = clenv_type elimclause'' in
   if Term.eq_constr hyp_typ new_hyp_typ then
-    errorlabstrm "general_rewrite_in"
+    user_err ~hdr:"general_rewrite_in"
       (str "Nothing to rewrite in " ++ pr_id id ++ str".");
   clenv_refine_in with_evars id id sigma elimclause''
     (fun id -> Proofview.tclUNIT ())
@@ -2017,7 +2017,7 @@ let clear_body ids =
     let map = function
     | LocalAssum (id,t) as decl ->
       let () = if List.mem_f Id.equal id ids then
-        errorlabstrm "" (str "Hypothesis " ++ pr_id id ++ str " is not a local definition")
+        user_err  (str "Hypothesis " ++ pr_id id ++ str " is not a local definition")
       in
       decl
     | LocalDef (id,_,t) as decl ->
@@ -2147,7 +2147,7 @@ let check_number_of_constructors expctdnumopt i nconstr =
   if Int.equal i 0 then error "The constructors are numbered starting from 1.";
   begin match expctdnumopt with
     | Some n when not (Int.equal n nconstr) ->
-	errorlabstrm "Tactics.check_number_of_constructors"
+	user_err ~hdr:"Tactics.check_number_of_constructors"
           (str "Not an inductive goal with " ++ int n ++ str (String.plural n " constructor") ++ str ".")
     | _ -> ()
   end;
@@ -2236,7 +2236,7 @@ let error_unexpected_extra_pattern loc bound pat =
   | IntroNaming (IntroIdentifier _) ->
       "name", (String.plural nb " introduction pattern"), "no"
   | _ -> "introduction pattern", "", "none" in
-  user_err_loc (loc,"",str "Unexpected " ++ str s1 ++ str " (" ++
+  user_err ~loc  (str "Unexpected " ++ str s1 ++ str " (" ++
     (if Int.equal nb 0 then (str s3 ++ str s2) else
       (str "at most " ++ int nb ++ str s2)) ++ spc () ++
        str (if Int.equal nb 1 then "was" else "were") ++
@@ -2476,8 +2476,8 @@ and prepare_intros_loc loc with_evars dft destopt = function
           (fun _ l -> clear_wildcards l) in
       fun id ->
         intro_pattern_action loc with_evars true true ipat [] destopt tac id)
-  | IntroForthcoming _ -> user_err_loc
-      (loc,"",str "Introduction pattern for one hypothesis expected.")
+  | IntroForthcoming _ -> user_err ~loc 
+      (str "Introduction pattern for one hypothesis expected.")
 
 let intro_patterns_bound_to with_evars n destopt =
   intro_patterns_core with_evars true [] [] [] destopt
@@ -2643,7 +2643,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
       | IntroFresh heq_base -> fresh_id_in_env [id] heq_base env
       | IntroIdentifier id ->
           if List.mem id (ids_of_named_context (named_context env)) then
-            user_err_loc (loc,"",pr_id id ++ str" is already used.");
+            user_err ~loc  (pr_id id ++ str" is already used.");
           id in
       let eqdata = build_coq_eq_data () in
       let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
@@ -2725,7 +2725,7 @@ let enough_by na t tac = forward false (Some (Some tac)) (ipat_of_name na) t
 let generalized_name c t ids cl = function
   | Name id as na ->
       if Id.List.mem id ids then
-	errorlabstrm "" (pr_id id ++ str " is already used.");
+	user_err  (pr_id id ++ str " is already used.");
       na
   | Anonymous ->
       match kind_of_term c with
@@ -2885,7 +2885,7 @@ let specialize (c,lbind) ipat =
       let tstack = chk tstack in
       let term = applist(thd,List.map (nf_evar clause.evd) tstack) in
       if occur_meta term then
-	errorlabstrm "" (str "Cannot infer an instance for " ++
+	user_err  (str "Cannot infer an instance for " ++
 
           pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++
 	  str ".");
@@ -2930,7 +2930,7 @@ let unfold_body x =
   (** We normalize the given hypothesis immediately. *)
   let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
   let xval = match Context.Named.lookup x hyps with
-  | LocalAssum _ -> errorlabstrm "unfold_body"
+  | LocalAssum _ -> user_err ~hdr:"unfold_body"
     (pr_id x ++ str" is not a defined hypothesis.")
   | LocalDef (_,xval,_) -> xval
   in
@@ -3027,7 +3027,7 @@ let safe_dest_intro_patterns with_evars avoid thin dest pat tac =
   Proofview.tclORELSE
     (dest_intro_patterns with_evars avoid thin dest pat tac)
     begin function (e, info) -> match e with
-      | UserError ("move_hyp",_) ->
+      | UserError (Some "move_hyp",_) ->
        (* May happen e.g. with "destruct x using s" with an hypothesis
           which is morally an induction hypothesis to be "MoveLast" if
           known as such but which is considered instead as a subterm of
@@ -3426,7 +3426,7 @@ let make_up_names n ind_opt cname =
 
 let error_ind_scheme s =
   let s = if not (String.is_empty s) then s^" " else s in
-  errorlabstrm "Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.")
+  user_err ~hdr:"Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.")
 
 let glob = Universes.constr_of_global
 
@@ -4043,7 +4043,7 @@ let recolle_clenv i params args elimclause gl =
       (fun x ->
 	match kind_of_term x with
 	  | Meta mv -> mv
-	  | _  -> errorlabstrm "elimination_clause"
+	  | _  -> user_err ~hdr:"elimination_clause"
               (str "The type of the elimination clause is not well-formed."))
       arr in
   let k = match i with -1 -> Array.length lindmv - List.length args | _ -> i in
@@ -4188,7 +4188,7 @@ let clear_unselected_context id inhyps cls =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   if occur_var (Tacmach.New.pf_env gl) id (Tacmach.New.pf_concl gl) &&
     cls.concl_occs == NoOccurrences
-  then errorlabstrm ""
+  then user_err 
     (str "Conclusion must be mentioned: it depends on " ++ pr_id id
      ++ str ".");
   match cls.onhyps with
@@ -4387,7 +4387,7 @@ let induction_gen_l isrec with_evars elim names lc =
   let lc = List.map (function
     | (c,None) -> c
     | (c,Some(loc,eqname)) ->
-      user_err_loc (loc,"",str "Do not know what to do with " ++
+      user_err ~loc  (str "Do not know what to do with " ++
                          Miscprint.pr_intro_pattern_naming eqname)) lc in
   let rec atomize_list l =
     match l with