Merge PR #244.

6 files changed, 38 insertions, 41 deletions

diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index 9f2c0a93e7..c67af33e23 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -36,8 +36,8 @@ let genarg_of_uconstr c = in_gen (rawwit Constrarg.wit_uconstr) c
 let reference_to_id = function
   | Libnames.Ident (loc, id) -> (loc, id)
   | Libnames.Qualid (loc,_) ->
-      CErrors.user_err_loc (loc, "",
-        str "This expression should be a simple identifier.")
+      CErrors.user_err ~loc 
+       (str "This expression should be a simple identifier.")
 
 let tactic_mode = Gram.entry_create "vernac:tactic_command"
 
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index b559864bd4..8e74249de9 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1502,7 +1502,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
 	Evar.Set.fold 
 	  (fun ev acc -> 
 	   if not (Evd.is_defined acc ev) then 
-	     errorlabstrm "rewrite"
+	     user_err ~hdr:"rewrite"
 			  (str "Unsolved constraint remaining: " ++ spc () ++
 			   Evd.pr_evar_info (Evd.find acc ev))
 	   else Evd.remove acc ev) 
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 673ac832a3..2fed0e14f2 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -429,8 +429,8 @@ let register_ltac local tacl =
         let kn = Lib.make_kn id in
         let id_pp = pr_id id in
         let () = if is_defined_tac kn then
-          CErrors.user_err_loc (loc, "",
-            str "There is already an Ltac named " ++ id_pp ++ str".")
+          CErrors.user_err ~loc 
+            (str "There is already an Ltac named " ++ id_pp ++ str".")
         in
         let is_shadowed =
           try
@@ -446,8 +446,8 @@ let register_ltac local tacl =
         let kn =
           try Nametab.locate_tactic (snd (qualid_of_reference ident))
           with Not_found ->
-            CErrors.user_err_loc (loc, "",
-                        str "There is no Ltac named " ++ pr_reference ident ++ str ".")
+            CErrors.user_err ~loc 
+                       (str "There is no Ltac named " ++ pr_reference ident ++ str ".")
         in
         UpdateTac kn, body
   in
diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml
index c709ab114e..e3c2b4ad51 100644
--- a/ltac/tacenv.ml
+++ b/ltac/tacenv.ml
@@ -65,7 +65,7 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } =
     let () = if Array.length tacs <= i then raise Not_found in
     tacs.(i)
   with Not_found ->
-    CErrors.errorlabstrm ""
+    CErrors.user_err 
       (str "The tactic " ++ pr_tacname s ++ str " is not installed.")
 
 (***************************************************************************)
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index c5bb0ed076..cd791398d9 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -32,11 +32,8 @@ open Locus
 
 let dloc = Loc.ghost
 
-let error_global_not_found_loc (loc,qid) =
-  error_global_not_found_loc loc qid
-
-let error_tactic_expected loc =
-  user_err_loc (loc,"",str "Tactic expected.")
+let error_tactic_expected ?loc =
+  user_err ?loc  (str "Tactic expected.")
 
 (** Generic arguments *)
 
@@ -85,7 +82,7 @@ let intern_hyp ist (loc,id as locid) =
   else if find_ident id ist then
     (dloc,id)
   else
-    Pretype_errors.error_var_not_found_loc loc id
+    Pretype_errors.error_var_not_found ~loc id
 
 let intern_or_var f ist = function
   | ArgVar locid -> ArgVar (intern_hyp ist locid)
@@ -99,7 +96,7 @@ let intern_global_reference ist = function
   | r ->
       let loc,_ as lqid = qualid_of_reference r in
       try ArgArg (loc,locate_global_with_alias lqid)
-      with Not_found -> error_global_not_found_loc lqid
+      with Not_found -> error_global_not_found (snd lqid)
 
 let intern_ltac_variable ist = function
   | Ident (loc,id) ->
@@ -143,7 +140,7 @@ let intern_isolated_tactic_reference strict ist r =
   try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
   with Not_found ->
   (* Reference not found *)
-  error_global_not_found_loc (qualid_of_reference r)
+  error_global_not_found (snd (qualid_of_reference r))
 
 (* Internalize an applied tactic reference *)
 
@@ -159,7 +156,7 @@ let intern_applied_tactic_reference ist r =
   try intern_applied_global_tactic_reference r
   with Not_found ->
   (* Reference not found *)
-  error_global_not_found_loc (qualid_of_reference r)
+  error_global_not_found (snd (qualid_of_reference r))
 
 (* Intern a reference parsed in a non-tactic entry *)
 
@@ -180,7 +177,7 @@ let intern_non_tactic_reference strict ist r =
     TacGeneric ipat
   | _ ->
   (* Reference not found *)
-  error_global_not_found_loc (qualid_of_reference r)
+  error_global_not_found (snd (qualid_of_reference r))
 
 let intern_message_token ist = function
   | (MsgString _ | MsgInt _ as x) -> x
@@ -291,7 +288,7 @@ let intern_evaluable_global_reference ist r =
   with Not_found ->
   match r with
   | Ident (loc,id) when not !strict_check -> EvalVarRef id
-  | _ -> error_global_not_found_loc lqid
+  | _ -> error_global_not_found (snd lqid)
 
 let intern_evaluable_reference_or_by_notation ist = function
   | AN r -> intern_evaluable_global_reference ist r
@@ -463,8 +460,8 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function
 (* Utilities *)
 let extract_let_names lrc =
   let fold accu ((loc, name), _) =
-    if Id.Set.mem name accu then user_err_loc
-      (loc, "glob_tactic", str "This variable is bound several times.")
+    if Id.Set.mem name accu then user_err ~loc
+      ~hdr:"glob_tactic" (str "This variable is bound several times.")
     else Id.Set.add name accu
   in
   List.fold_left fold Id.Set.empty lrc
@@ -641,7 +638,7 @@ and intern_tactic_as_arg loc onlytac ist a =
   | TacGeneric _ as a -> TacArg (loc,a)
   | Tacexp a -> a
   | ConstrMayEval _ | TacFreshId _ | TacPretype _ | TacNumgoals as a ->
-      if onlytac then error_tactic_expected loc else TacArg (loc,a)
+      if onlytac then error_tactic_expected ~loc else TacArg (loc,a)
 
 and intern_tactic_or_tacarg ist = intern_tactic false ist
 
@@ -751,7 +748,7 @@ let print_ltac id =
     ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined
  with
   Not_found ->
-   errorlabstrm "print_ltac"
+   user_err ~hdr:"print_ltac"
     (pr_qualid id ++ spc() ++ str "is not a user defined tactic.")
 
 (** Registering *)
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index ddebac5ab5..177867abd8 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -168,7 +168,7 @@ module Value = struct
     let pr_v = Pptactic.pr_value Pptactic.ltop v in
     let Val.Dyn (tag, _) = v in
     let tag = Val.pr tag in
-    errorlabstrm "" (str "Type error: value " ++ pr_v ++ str " is a " ++ tag
+    user_err  (str "Type error: value " ++ pr_v ++ str " is a " ++ tag
       ++ str " while type " ++ Val.pr wit ++ str " was expected.")
 
   let unbox wit v ans = match ans with
@@ -315,8 +315,8 @@ let append_trace trace v =
 (* Dynamically check that an argument is a tactic *)
 let coerce_to_tactic loc id v =
   let v = Value.normalize v in
-  let fail () = user_err_loc
-    (loc, "", str "Variable " ++ pr_id id ++ str " should be bound to a tactic.")
+  let fail () = user_err ~loc 
+    (str "Variable " ++ pr_id id ++ str " should be bound to a tactic.")
   in
   let v = Value.normalize v in
   if has_type v (topwit wit_tacvalue) then
@@ -371,7 +371,7 @@ let debugging_exception_step ist signal_anomaly e pp =
     pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e)
 
 let error_ltac_variable loc id env v s =
-   user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++
+   user_err ~loc  (str "Ltac variable " ++ pr_id id ++
    strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
    strbrk "which cannot be coerced to " ++ str s ++ str".")
 
@@ -404,8 +404,8 @@ let interp_intro_pattern_naming_var loc ist env sigma id =
 let interp_int ist locid =
   try try_interp_ltac_var coerce_to_int ist None locid
   with Not_found ->
-    user_err_loc(fst locid,"interp_int",
-      str "Unbound variable "  ++ pr_id (snd locid) ++ str".")
+    user_err ~loc:(fst locid) ~hdr:"interp_int"
+     (str "Unbound variable "  ++ pr_id (snd locid) ++ str".")
 
 let interp_int_or_var ist = function
   | ArgVar locid -> interp_int ist locid
@@ -427,7 +427,7 @@ let interp_hyp ist env sigma (loc,id as locid) =
   with Not_found ->
   (* Then look if bound in the proof context at calling time *)
   if is_variable env id then id
-  else Loc.raise loc (Logic.RefinerError (Logic.NoSuchHyp id))
+  else Loc.raise ~loc (Logic.RefinerError (Logic.NoSuchHyp id))
 
 let interp_hyp_list_as_list ist env sigma (loc,id as x) =
   try coerce_to_hyp_list env (Id.Map.find id ist.lfun)
@@ -449,7 +449,7 @@ let interp_reference ist env sigma = function
     with Not_found ->
       try
         VarRef (get_id (Environ.lookup_named id env))
-      with Not_found -> error_global_not_found_loc loc (qualid_of_ident id)
+      with Not_found -> error_global_not_found ~loc (qualid_of_ident id)
 
 let try_interp_evaluable env (loc, id) =
   let v = Environ.lookup_named id env in
@@ -465,14 +465,14 @@ let interp_evaluable ist env sigma = function
       with Not_found ->
         match r with
         | EvalConstRef _ -> r
-        | _ -> error_global_not_found_loc loc (qualid_of_ident id)
+        | _ -> error_global_not_found ~loc (qualid_of_ident id)
     end
   | ArgArg (r,None) -> r
   | ArgVar (loc, id) ->
     try try_interp_ltac_var (coerce_to_evaluable_ref env) ist (Some (env,sigma)) (loc, id)
     with Not_found ->
       try try_interp_evaluable env (loc, id)
-      with Not_found -> error_global_not_found_loc loc (qualid_of_ident id)
+      with Not_found -> error_global_not_found ~loc (qualid_of_ident id)
 
 (* Interprets an hypothesis name *)
 let interp_occurrences ist occs =
@@ -739,7 +739,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
         Inr (pattern_of_constr env sigma c) in
     (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id)
      with Not_found ->
-       error_global_not_found_loc loc (qualid_of_ident id))
+       error_global_not_found ~loc (qualid_of_ident id))
   | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
   | Inr c -> Inr (interp_typed_pattern ist env sigma c) in
   interp_occurrences ist occs, p
@@ -795,8 +795,8 @@ let interp_may_eval f ist env sigma = function
 	!evdref , c
       with
 	| Not_found ->
-	    user_err_loc (loc, "interp_may_eval",
-	    str "Unbound context identifier" ++ pr_id s ++ str"."))
+	    user_err ~loc ~hdr:"interp_may_eval"
+	    (str "Unbound context identifier" ++ pr_id s ++ str"."))
   | ConstrTypeOf c ->
       let (sigma,c_interp) = f ist env sigma c in
       Typing.type_of ~refresh:true env sigma c_interp
@@ -1032,8 +1032,8 @@ let interp_destruction_arg ist gl arg =
       }
   | keep,ElimOnAnonHyp n as x -> x
   | keep,ElimOnIdent (loc,id) ->
-      let error () = user_err_loc (loc, "",
-        strbrk "Cannot coerce " ++ pr_id id ++
+      let error () = user_err ~loc 
+       (strbrk "Cannot coerce " ++ pr_id id ++
         strbrk " neither to a quantified hypothesis nor to a term.")
       in
       let try_cast_id id' =
@@ -1043,7 +1043,7 @@ let interp_destruction_arg ist gl arg =
           (keep, ElimOnConstr { delayed = begin fun env sigma ->
           try Sigma.here (constr_of_id env id', NoBindings) sigma
           with Not_found ->
-            user_err_loc (loc, "interp_destruction_arg",
+            user_err ~loc  ~hdr:"interp_destruction_arg" (
             pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.")
           end })
       in
@@ -1111,7 +1111,7 @@ let read_pattern lfun ist env sigma = function
 (* Reads the hypotheses of a Match Context rule *)
 let cons_and_check_name id l =
   if Id.List.mem id l then
-    user_err_loc (dloc,"read_match_goal_hyps",
+    user_err ~hdr:"read_match_goal_hyps" (
       str "Hypothesis pattern-matching variable " ++ pr_id id ++
       str " used twice in the same pattern.")
   else id::l
@@ -1867,7 +1867,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
               let (sigma, c) = interp_constr ist env sigma c in
               Sigma.Unsafe.of_pair (c, sigma)
             with e when to_catch e (* Hack *) ->
-              errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
+              user_err  (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
         end } in
         Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)
       end }