Unify location handling of error functions.

In some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.

We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.

This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.

4 files changed, 33 insertions, 36 deletions

diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index 9f2c0a93e7..85f1a0225f 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/tacentries.ml b/ltac/tacentries.ml
index 673ac832a3..1b7430c3ff 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/tacintern.ml b/ltac/tacintern.ml
index c5bb0ed076..dc216da114 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
+      "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
 
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index aa7e096a9d..76c46ea7c4 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -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) "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 "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  "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 "read_match_goal_hyps" (
       str "Hypothesis pattern-matching variable " ++ pr_id id ++
       str " used twice in the same pattern.")
   else id::l