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.

11 files changed, 118 insertions, 119 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 04429851fd..9097a56f85 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -382,18 +382,18 @@ let rec prod_constr_expr c = function
 let coerce_reference_to_id = function
   | Ident (_,id) -> id
   | Qualid (loc,_) ->
-      CErrors.user_err_loc (loc, "coerce_reference_to_id",
-        str "This expression should be a simple identifier.")
+      CErrors.user_err ~loc "coerce_reference_to_id"
+        (str "This expression should be a simple identifier.")
 
 let coerce_to_id = function
   | CRef (Ident (loc,id),_) -> (loc,id)
-  | a -> CErrors.user_err_loc
-        (constr_loc a,"coerce_to_id",
-         str "This expression should be a simple identifier.")
+  | a -> CErrors.user_err ~loc:(constr_loc a)
+       "coerce_to_id"
+         (str "This expression should be a simple identifier.")
 
 let coerce_to_name = function
   | CRef (Ident (loc,id),_) -> (loc,Name id)
   | CHole (loc,_,_,_) -> (loc,Anonymous)
-  | a -> CErrors.user_err_loc
-        (constr_loc a,"coerce_to_name",
-         str "This expression should be a name.")
+  | a -> CErrors.user_err
+         ~loc:(constr_loc a) "coerce_to_name"
+         (str "This expression should be a name.")
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e71daef999..3e6bc80f23 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -94,8 +94,8 @@ let is_record indsp =
 let encode_record r =
   let indsp = global_inductive r in
   if not (is_record indsp) then
-    user_err_loc (loc_of_reference r,"encode_record",
-    str "This type is not a structure type.");
+    user_err ~loc:(loc_of_reference r) "encode_record"
+      (str "This type is not a structure type.");
   indsp
 
 module PrintingRecordRecord =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7c4688f9fb..f4907e92a5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -154,17 +154,17 @@ let explain_internalization_error e =
   | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2
   in pp ++ str "."
 
-let error_bad_inductive_type loc =
-  user_err_loc (loc,"",str
+let error_bad_inductive_type ?loc =
+  user_err ?loc "" (str
     "This should be an inductive type applied to patterns.")
 
-let error_parameter_not_implicit loc =
-  user_err_loc (loc,"", str
+let error_parameter_not_implicit ?loc =
+  user_err ?loc "" (str
    "The parameters do not bind in patterns;" ++ spc () ++ str
     "they must be replaced by '_'.")
 
-let error_ldots_var loc =
-  user_err_loc (loc,"",str "Special token " ++ pr_id ldots_var ++
+let error_ldots_var ?loc =
+  user_err ?loc "" (str "Special token " ++ pr_id ldots_var ++
     str " is for use in the Notation command.")
 
 (**********************************************************************)
@@ -262,15 +262,15 @@ let pr_scope_stack = function
   | l -> str "scope stack " ++
       str "[" ++ prlist_with_sep pr_comma str l ++ str "]"
 
-let error_inconsistent_scope loc id scopes1 scopes2 =
-  user_err_loc (loc,"set_var_scope",
-    pr_id id ++ str " is here used in " ++
+let error_inconsistent_scope ?loc id scopes1 scopes2 =
+  user_err ?loc "set_var_scope"
+   (pr_id id ++ str " is here used in " ++
     pr_scope_stack scopes2 ++ strbrk " while it was elsewhere used in " ++
     pr_scope_stack scopes1)
 
-let error_expect_binder_notation_type loc id =
-  user_err_loc (loc,"",
-    pr_id id ++
+let error_expect_binder_notation_type ?loc id =
+  user_err ?loc ""
+   (pr_id id ++
     str " is expected to occur in binding position in the right-hand side.")
 
 let set_var_scope loc id istermvar env ntnvars =
@@ -284,12 +284,12 @@ let set_var_scope loc id istermvar env ntnvars =
       | Some (tmp, scope) ->
         let s1 = make_current_scope tmp scope in
         let s2 = make_current_scope env.tmp_scope env.scopes in
-        if not (List.equal String.equal s1 s2) then error_inconsistent_scope loc id s1 s2
+        if not (List.equal String.equal s1 s2) then error_inconsistent_scope ~loc id s1 s2
       end
     in
     match typ with
     | NtnInternTypeBinder ->
-	if istermvar then error_expect_binder_notation_type loc id
+	if istermvar then error_expect_binder_notation_type ~loc id
     | NtnInternTypeConstr ->
 	(* We need sometimes to parse idents at a constr level for
 	   factorization and we cannot enforce this constraint:
@@ -373,12 +373,12 @@ let push_name_env ?(global_level=false) ntnvars implargs env =
   function
   | loc,Anonymous ->
       if global_level then
-	user_err_loc (loc,"", str "Anonymous variables not allowed");
+	user_err ~loc "" (str "Anonymous variables not allowed");
       env
   | loc,Name id ->
       check_hidden_implicit_parameters id env.impls ;
       if Id.Map.is_empty ntnvars && Id.equal id ldots_var
-        then error_ldots_var loc;
+        then error_ldots_var ~loc;
       set_var_scope loc id false env ntnvars;
       if global_level then Dumpglob.dump_definition (loc,id) true "var"
       else Dumpglob.dump_binding loc id;
@@ -764,7 +764,7 @@ let string_of_ty = function
 let gvar (loc, id) us = match us with
 | None -> GVar (loc, id)
 | Some _ ->
-  user_err_loc (loc, "", str "Variable " ++ pr_id id ++
+  user_err ~loc "" (str "Variable " ++ pr_id id ++
     str " cannot have a universe instance")
 
 let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
@@ -788,12 +788,12 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
   (* Is [id] the special variable for recursive notations *)
   else if Id.equal id ldots_var
   then if Id.Map.is_empty ntnvars
-    then error_ldots_var loc
+    then error_ldots_var ~loc
     else gvar (loc,id) us, [], [], []
   else if Id.Set.mem id ltacvars.ltac_bound then
     (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
-    user_err_loc (loc,"intern_var",
-      str "variable " ++ pr_id id ++ str " should be bound to a term.")
+    user_err ~loc "intern_var"
+     (str "variable " ++ pr_id id ++ str " should be bound to a term.")
   else
     (* Is [id] a goal or section variable *)
     let _ = Context.Named.lookup id namedctx in
@@ -825,7 +825,7 @@ let find_appl_head_data c =
   | x -> x,[],[],[]
 
 let error_not_enough_arguments loc =
-  user_err_loc (loc,"",str "Abbreviation is not applied enough.")
+  user_err ~loc "" (str "Abbreviation is not applied enough.")
 
 let check_no_explicitation l =
   let is_unset (a, b) = match b with None -> false | Some _ -> true in
@@ -834,7 +834,7 @@ let check_no_explicitation l =
   | [] -> ()
   | (_, None) :: _ -> assert false
   | (_, Some (loc, _)) :: _ ->
-    user_err_loc (loc,"",str"Unexpected explicitation of the argument of an abbreviation.")
+    user_err ~loc "" (str"Unexpected explicitation of the argument of an abbreviation.")
 
 let dump_extended_global loc = function
   | TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob loc ref
@@ -847,7 +847,7 @@ let intern_reference ref =
   let qid = qualid_of_reference ref in
   let r =
     try intern_extended_global_of_qualid qid
-    with Not_found -> error_global_not_found_loc (fst qid) (snd qid)
+    with Not_found -> error_global_not_found ~loc:(fst qid) (snd qid)
   in
   Smartlocate.global_of_extended_global r
 
@@ -872,7 +872,7 @@ let intern_qualid loc qid intern env lvar us args =
       | Some _, GApp (loc, GRef (loc', ref, None), arg) ->
          GApp (loc, GRef (loc', ref, us), arg)
       | Some _, _ ->
-        user_err_loc (loc, "", str "Notation " ++ pr_qualid qid ++
+        user_err ~loc "" (str "Notation " ++ pr_qualid qid ++
           str " cannot have a universe instance, its expanded head
                does not start with a reference")
       in
@@ -888,7 +888,7 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args =
   | Qualid (loc, qid) ->
       let r,projapp,args2 =
 	try intern_qualid loc qid intern env ntnvars us args
-	with Not_found -> error_global_not_found_loc loc qid
+	with Not_found -> error_global_not_found ~loc qid
       in
       let x, imp, scopes, l = find_appl_head_data r in
 	(x,imp,scopes,l), args2
@@ -904,7 +904,7 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args =
 	(* Extra allowance for non globalizing functions *)
 	if !interning_grammar || env.unb then
 	  (gvar (loc,id) us, [], [], []), args
-	else error_global_not_found_loc loc qid
+	else error_global_not_found ~loc qid
 
 let interp_reference vars r =
   let (r,_,_,_),_ =
@@ -982,7 +982,7 @@ let check_number_of_pattern loc n l =
 
 let check_or_pat_variables loc ids idsl =
   if List.exists (fun ids' -> not (List.eq_set Id.equal ids ids')) idsl then
-    user_err_loc (loc, "", str
+    user_err ~loc "" (str
     "The components of this disjunctive pattern must bind the same variables.")
 
 (** Use only when params were NOT asked to the user.
@@ -991,7 +991,7 @@ let check_constructor_length env loc cstr len_pl pl0 =
   let n = len_pl + List.length pl0 in
   if Int.equal n (Inductiveops.constructor_nallargs cstr) then false else
     (Int.equal n (Inductiveops.constructor_nalldecls cstr) ||
-      (error_wrong_numarg_constructor_loc loc env cstr
+      (error_wrong_numarg_constructor ~loc env cstr
          (Inductiveops.constructor_nrealargs cstr)))
 
 let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 =
@@ -1016,14 +1016,14 @@ let add_implicits_check_constructor_length env loc c len_pl1 pl2 =
   let nargs = Inductiveops.constructor_nallargs c in
   let nargs' = Inductiveops.constructor_nalldecls c in
   let impls_st = implicits_of_global (ConstructRef c) in
-  add_implicits_check_length (error_wrong_numarg_constructor_loc loc env c)
+  add_implicits_check_length (error_wrong_numarg_constructor ~loc env c)
     nargs nargs' impls_st len_pl1 pl2
 
 let add_implicits_check_ind_length env loc c len_pl1 pl2 =
   let nallargs = inductive_nallargs_env env c in
   let nalldecls = inductive_nalldecls_env env c in
   let impls_st = implicits_of_global (IndRef c) in
-  add_implicits_check_length (error_wrong_numarg_inductive_loc loc env c)
+  add_implicits_check_length (error_wrong_numarg_inductive ~loc env c)
     nallargs nalldecls impls_st len_pl1 pl2
 
 (** Do not raise NotEnoughArguments thanks to preconditions*)
@@ -1034,7 +1034,7 @@ let chop_params_pattern loc ind args with_letin =
   assert (nparams <= List.length args);
   let params,args = List.chop nparams args in
   List.iter (function PatVar(_,Anonymous) -> ()
-    | PatVar (loc',_) | PatCstr(loc',_,_,_) -> error_parameter_not_implicit loc') params;
+    | PatVar (loc',_) | PatCstr(loc',_,_,_) -> error_parameter_not_implicit ~loc:loc') params;
   args
 
 let find_constructor loc add_params ref =
@@ -1042,10 +1042,10 @@ let find_constructor loc add_params ref =
   | ConstructRef cstr -> cstr
   | IndRef _ ->
     let error = str "There is an inductive name deep in a \"in\" clause." in
-    user_err_loc (loc, "find_constructor", error)
+    user_err ~loc "find_constructor" error
   | ConstRef _ | VarRef _ ->
     let error = str "This reference is not a constructor." in
-    user_err_loc (loc, "find_constructor", error)
+    user_err ~loc "find_constructor" error
   in
   cstr, match add_params with
     | Some nb_args ->
@@ -1085,8 +1085,8 @@ let sort_fields ~complete loc fields completer =
         let record =
           try Recordops.find_projection first_field_glob_ref
           with Not_found ->
-            user_err_loc (loc_of_reference first_field_ref, "intern",
-                          pr_reference first_field_ref ++ str": Not a projection")
+            user_err ~loc:(loc_of_reference first_field_ref) "intern"
+                         (pr_reference first_field_ref ++ str": Not a projection")
         in
         (* the number of parameters *)
         let nparams = record.Recordops.s_EXPECTEDPARAM in
@@ -1114,7 +1114,7 @@ let sort_fields ~complete loc fields completer =
                            by a let-in in the record declaration
                            (its value is fixed from other fields). *)
                        if first_field && not regular && complete then
-                         user_err_loc (loc, "", str "No local fields allowed in a record construction.")
+                         user_err ~loc "" (str "No local fields allowed in a record construction.")
                        else if first_field then
                          build_proj_list projs proj_kinds (idx+1) ~acc_first_idx:idx acc
                        else if not regular && complete then
@@ -1127,7 +1127,7 @@ let sort_fields ~complete loc fields completer =
               | None :: projs ->
                  if complete then
                    (* we don't want anonymous fields *)
-                   user_err_loc (loc, "", str "This record contains anonymous fields.")
+                   user_err ~loc "" (str "This record contains anonymous fields.")
                  else
                    (* anonymous arguments don't appear in proj_kinds *)
                    build_proj_list projs proj_kinds (idx+1) ~acc_first_idx acc
@@ -1141,15 +1141,14 @@ let sort_fields ~complete loc fields completer =
             | (field_ref, field_value) :: fields ->
                let field_glob_ref = try global_reference_of_reference field_ref
                with Not_found ->
-                 user_err_loc (loc_of_reference field_ref, "intern",
-                               str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
+                 user_err ~loc:(loc_of_reference field_ref) "intern"
+                               (str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
                let remaining_projs, (field_index, _) =
                  let the_proj (idx, glob_ref) = eq_gr field_glob_ref glob_ref in
                  try CList.extract_first the_proj remaining_projs
                  with Not_found ->
-                   user_err_loc
-                     (loc, "",
-                      str "This record contains fields of different records.")
+                   user_err ~loc ""
+                     (str "This record contains fields of different records.")
                in
                index_fields fields remaining_projs ((field_index, field_value) :: acc)
             | [] ->
@@ -1220,7 +1219,7 @@ let drop_notations_pattern looked_for =
       if top then looked_for g else
       match g with ConstructRef _ -> () | _ -> raise Not_found
     with Not_found ->
-      error_invalid_pattern_notation loc
+      error_invalid_pattern_notation ~loc
   in
   let test_kind top =
     if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found
@@ -1345,8 +1344,8 @@ let drop_notations_pattern looked_for =
 		 List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @
 		 List.map (in_pat false scopes) args, [])
     | NList (x,y,iter,terminator,lassoc) ->
-      if not (List.is_empty args) then user_err_loc
-        (loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns.");
+      if not (List.is_empty args) then user_err ~loc ""
+        (strbrk "Application of arguments to a recursive notation not supported in patterns.");
       (try
          (* All elements of the list are in scopes (scopt,subscopes) *)
 	 let (l,(scopt,subscopes)) = Id.Map.find x substlist in
@@ -1361,7 +1360,7 @@ let drop_notations_pattern looked_for =
     | NHole _ ->
       let () = assert (List.is_empty args) in
       RCPatAtom (loc, None)
-    | t -> error_invalid_pattern_notation loc
+    | t -> error_invalid_pattern_notation ~loc
   in in_pat true
 
 let rec intern_pat genv aliases pat =
@@ -1413,11 +1412,11 @@ let intern_ind_pattern genv scopes pat =
   let no_not =
     try
       drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat
-    with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type loc
+    with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ~loc
   in
   match no_not with
     | RCPatCstr (loc, head, expl_pl, pl) ->
-      let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type loc) head in
+      let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ~loc) head in
       let with_letin, pl2 = add_implicits_check_ind_length genv loc c
 	(List.length expl_pl) pl in
       let idslpl1 = List.rev_map (intern_pat genv empty_alias) expl_pl in
@@ -1425,8 +1424,8 @@ let intern_ind_pattern genv scopes pat =
       (with_letin,
        match product_of_cases_patterns [] (List.rev_append idslpl1 idslpl2) with
        | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin)
-       | _ -> error_bad_inductive_type loc)
-    | x -> error_bad_inductive_type (raw_cases_pattern_expr_loc x)
+       | _ -> error_bad_inductive_type ~loc)
+    | x -> error_bad_inductive_type ~loc:(raw_cases_pattern_expr_loc x)
 
 (**********************************************************************)
 (* Utilities for application                                          *)
@@ -1465,10 +1464,10 @@ let extract_explicit_arg imps args =
 	  let id = match pos with
 	  | ExplByName id ->
 	      if not (exists_implicit_name id imps) then
-		user_err_loc
-		  (loc,"",str "Wrong argument name: " ++ pr_id id ++ str ".");
+		user_err ~loc ""
+		  (str "Wrong argument name: " ++ pr_id id ++ str ".");
 	      if Id.Map.mem id eargs then
-		user_err_loc (loc,"",str "Argument name " ++ pr_id id
+		user_err ~loc "" (str "Argument name " ++ pr_id id
 		++ str " occurs more than once.");
 	      id
 	  | ExplByPos (p,_id) ->
@@ -1478,11 +1477,11 @@ let extract_explicit_arg imps args =
 		  if not (is_status_implicit imp) then failwith "imp";
 		  name_of_implicit imp
 		with Failure _ (* "nth" | "imp" *) ->
-		  user_err_loc
-		    (loc,"",str"Wrong argument position: " ++ int p ++ str ".")
+		  user_err ~loc ""
+		    (str"Wrong argument position: " ++ int p ++ str ".")
 	      in
 	      if Id.Map.mem id eargs then
-		user_err_loc (loc,"",str"Argument at position " ++ int p ++
+		user_err ~loc "" (str"Argument at position " ++ int p ++
 		  str " is mentioned more than once.");
 	      id in
 	  (Id.Map.add id (loc, a) eargs, rargs)
@@ -1533,7 +1532,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
                  (function
                   | BDRawDef a -> a
                   | BDPattern (loc,_,_,_,_) ->
-                      Loc.raise loc (Stream.Error "pattern with quote not allowed after fix")) rbl in
+                      Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix")) rbl in
 	       ((n, ro), bl, intern_type env' ty, env')) dl in
         let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') ->
 	     let env'' = List.fold_left_i (fun i en name -> 
@@ -1637,7 +1636,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
        in
        begin
 	  match fields with
-	    | None -> user_err_loc (loc, "intern", str"No constructor inference.")
+	    | None -> user_err ~loc "intern" (str"No constructor inference.")
 	    | Some (n, constrname, args) ->
 		let pars = List.make n (CHole (loc, None, Misctypes.IntroAnonymous, None)) in
                 let app = CAppExpl (loc, (None, constrname,None), List.rev_append pars args) in
@@ -1860,7 +1859,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
       | (imp::impl', []) ->
 	  if not (Id.Map.is_empty eargs) then
 	    (let (id,(loc,_)) = Id.Map.choose eargs in
-	       user_err_loc (loc,"",str "Not enough non implicit \
+	       user_err ~loc "" (str "Not enough non implicit \
 	    arguments to accept the argument bound to " ++
 		 pr_id id ++ str"."));
 	  []
@@ -1891,8 +1890,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     intern env c
   with
       InternalizationError (loc,e) ->
-	user_err_loc (loc,"internalize",
-	  explain_internalization_error e)
+	user_err ~loc "internalize"
+	  (explain_internalization_error e)
 
 (**************************************************************************)
 (* Functions to translate constr_expr into glob_constr                    *)
@@ -1931,7 +1930,7 @@ let intern_pattern globalenv patt =
     intern_cases_pattern globalenv (None,[]) empty_alias patt
   with
       InternalizationError (loc,e) ->
-	user_err_loc (loc,"internalize",explain_internalization_error e)
+	user_err ~loc "internalize" (explain_internalization_error e)
 
 
 (*********************************************************************)
@@ -2042,13 +2041,13 @@ let intern_context global_level env impl_env binders =
                    (function
                     | BDRawDef a -> a
                     | BDPattern (loc,_,_,_,_) ->
-                        Loc.raise loc (Stream.Error "pattern with quote not allowed here")) bl in
+                        Loc.raise ~loc (Stream.Error "pattern with quote not allowed here")) bl in
 	       (env, bl))
 	    ({ids = extract_ids env; unb = false;
 	      tmp_scope = None; scopes = []; impls = impl_env}, []) binders in
   (lenv.impls, List.map snd bl)
   with InternalizationError (loc,e) ->
-    user_err_loc (loc,"internalize", explain_internalization_error e)
+    user_err ~loc "internalize" (explain_internalization_error e)
 
 let interp_rawcontext_evars env evdref k bl =
   let (env, par, _, impls) =
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 10cfbe58fa..8908e1f6f9 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -27,12 +27,12 @@ let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident"
 
 let declare_generalizable_ident table (loc,id) =
   if not (Id.equal id (root_of_id id)) then
-    user_err_loc(loc,"declare_generalizable_ident",
-    (pr_id id ++ str
+    user_err ~loc "declare_generalizable_ident"
+    ((pr_id id ++ str
       " is not declarable as generalizable identifier: it must have no trailing digits, quote, or _"));
   if Id.Pred.mem id table then
-    user_err_loc(loc,"declare_generalizable_ident",
-		(pr_id id++str" is already declared as a generalizable identifier"))
+    user_err ~loc "declare_generalizable_ident"
+		((pr_id id++str" is already declared as a generalizable identifier"))
   else Id.Pred.add id table
 
 let add_generalizable gen table =
@@ -78,8 +78,8 @@ let is_freevar ids env x =
 (* Auxiliary functions for the inference of implicitly quantified variables. *)
 
 let ungeneralizable loc id =
-  user_err_loc (loc, "Generalization", 
-	       str "Unbound and ungeneralizable variable " ++ pr_id id)
+  user_err ~loc "Generalization"
+	       (str "Unbound and ungeneralizable variable " ++ pr_id id)
 
 let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
   let found loc id bdvars l =
@@ -203,7 +203,7 @@ let combine_params avoid fn applied needed =
             | Anonymous -> false
             in
 	    if not (List.exists is_id needed) then
-	      user_err_loc (loc,"",str "Wrong argument name: " ++ Nameops.pr_id id);
+	      user_err ~loc "" (str "Wrong argument name: " ++ Nameops.pr_id id);
 	    true
 	| _ -> false) applied
   in
@@ -237,7 +237,7 @@ let combine_params avoid fn applied needed =
 	    aux (t' :: ids) avoid' app need
 
       | (x,_) :: _, [] ->
-	  user_err_loc (Constrexpr_ops.constr_loc x,"",str "Typeclass does not expect more arguments")
+	  user_err ~loc:(Constrexpr_ops.constr_loc x) "" (str "Typeclass does not expect more arguments")
   in aux [] avoid applied needed
 
 let combine_params_freevar =
diff --git a/interp/modintern.ml b/interp/modintern.ml
index e5dce5ccf3..d4ade7058a 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -26,16 +26,16 @@ let error_not_a_module_loc kind loc qid =
     | ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s)
     | ModAny -> ModuleInternalizationError (NotAModuleNorModtype s)
   in
-  Loc.raise loc e
+  Loc.raise ~loc e
 
 let error_application_to_not_path loc me =
-  Loc.raise loc (Modops.ModuleTypingError (Modops.ApplicationToNotPath me))
+  Loc.raise ~loc (Modops.ModuleTypingError (Modops.ApplicationToNotPath me))
 
 let error_incorrect_with_in_module loc =
-  Loc.raise loc (ModuleInternalizationError IncorrectWithInModule)
+  Loc.raise ~loc (ModuleInternalizationError IncorrectWithInModule)
 
 let error_application_to_module_type loc =
-  Loc.raise loc (ModuleInternalizationError IncorrectModuleApplication)
+  Loc.raise ~loc (ModuleInternalizationError IncorrectModuleApplication)
 
 (** Searching for a module name in the Nametab.
 
diff --git a/interp/notation.ml b/interp/notation.ml
index 0798d385d4..0c15e91b84 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -220,8 +220,8 @@ let remove_delimiters scope =
 let find_delimiters_scope loc key =
   try String.Map.find key !delimiters_map
   with Not_found ->
-    user_err_loc
-    (loc, "find_delimiters", str "Unknown scope delimiting key " ++ str key ++ str ".")
+    user_err ~loc "find_delimiters"
+      (str "Unknown scope delimiting key " ++ str key ++ str ".")
 
 (* Uninterpretation tables *)
 
@@ -337,8 +337,8 @@ let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
 let check_required_module loc sc (sp,d) =
   try let _ = Nametab.global_of_path sp in ()
   with Not_found ->
-    user_err_loc (loc,"prim_token_interpreter",
-    str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".")
+    user_err ~loc "prim_token_interpreter"
+    (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".")
 
 (* Look if some notation or numeral printer in [scope] can be used in
    the scope stack [scopes], and if yes, using delimiters or not *)
@@ -458,8 +458,8 @@ let interp_prim_token_gen g loc p local_scopes =
   let p_as_ntn = try notation_of_prim_token p with Not_found -> "" in
   try find_interpretation p_as_ntn (find_prim_token g loc p) scopes
   with Not_found ->
-    user_err_loc (loc,"interp_prim_token",
-    (match p with
+    user_err ~loc "interp_prim_token"
+    ((match p with
       | Numeral n -> str "No interpretation for numeral " ++ str (to_string n)
       | String s -> str "No interpretation for string " ++ qs s) ++ str ".")
 
@@ -483,8 +483,8 @@ let interp_notation loc ntn local_scopes =
   let scopes = make_current_scopes local_scopes in
   try find_interpretation ntn (find_notation ntn) scopes
   with Not_found ->
-    user_err_loc
-    (loc,"",str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".")
+    user_err ~loc ""
+    (str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".")
 
 let uninterp_notations c =
   List.map_append (fun key -> keymap_find key !notations_key_table)
@@ -890,11 +890,11 @@ let global_reference_of_notation test (ntn,(sc,c,_)) =
   | _ -> None
 
 let error_ambiguous_notation loc _ntn =
-  user_err_loc (loc,"",str "Ambiguous notation.")
+  user_err ~loc "" (str "Ambiguous notation.")
 
 let error_notation_not_reference loc ntn =
-  user_err_loc (loc,"",
-    str "Unable to interpret " ++ quote (str ntn) ++
+  user_err ~loc ""
+   (str "Unable to interpret " ++ quote (str ntn) ++
     str " as a reference.")
 
 let interp_notation_as_global_reference loc test ntn sc =
@@ -1017,8 +1017,8 @@ let add_notation_extra_printing_rule ntn k v =
       let p, pp, gr = String.Map.find ntn !notation_rules in
       String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules
   with Not_found ->
-    user_err_loc (Loc.ghost,"add_notation_extra_printing_rule",
-      str "No such Notation.")
+    user_err "add_notation_extra_printing_rule"
+      (str "No such Notation.")
 
 (**********************************************************************)
 (* Synchronisation with reset *)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index f3e0682bd7..7ab6ebb265 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -233,8 +233,8 @@ let split_at_recursive_part c =
 let subtract_loc loc1 loc2 = Loc.make_loc (fst (Loc.unloc loc1),fst (Loc.unloc loc2)-1)
 
 let check_is_hole id = function GHole _ -> () | t ->
-  user_err_loc (loc_of_glob_constr t,"",
-    strbrk "In recursive notation with binders, " ++ pr_id id ++
+  user_err ~loc:(loc_of_glob_constr t) ""
+   (strbrk "In recursive notation with binders, " ++ pr_id id ++
     strbrk " is expected to come without type.")
 
 let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b'
@@ -283,8 +283,8 @@ let compare_recursive_parts found f f' (iterator,subc) =
 	let loc1 = loc_of_glob_constr iterator in
 	let loc2 = loc_of_glob_constr (Option.get !terminator) in
 	(* Here, we would need a loc made of several parts ... *)
-	user_err_loc (subtract_loc loc1 loc2,"",
-          str "Both ends of the recursive pattern are the same.")
+	user_err ~loc:(subtract_loc loc1 loc2) ""
+          (str "Both ends of the recursive pattern are the same.")
     | Some (x,y,Some lassoc) ->
         let newfound,x,y,lassoc =
           if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) ||
@@ -324,8 +324,8 @@ let notation_constr_and_vars_of_glob_constr a =
     | GApp (_,GVar (loc,f),[c]) when Id.equal f ldots_var ->
 	(* Fall on the second part of the recursive pattern w/o having
 	   found the first part *)
-	user_err_loc (loc,"",
-	str "Cannot find where the recursive pattern starts.")
+	user_err ~loc ""
+	(str "Cannot find where the recursive pattern starts.")
     | c ->
 	aux' c
   and aux' = function
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 388ca08050..31425fb980 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -86,13 +86,13 @@ let in_reserved : Id.t * notation_constr -> obj =
 
 let declare_reserved_type_binding (loc,id) t =
   if not (Id.equal id (root_of_id id)) then
-    user_err_loc(loc,"declare_reserved_type",
-    (pr_id id ++ str
+    user_err ~loc "declare_reserved_type"
+      ((pr_id id ++ str
       " is not reservable: it must have no trailing digits, quote, or _"));
   begin try
     let _ = Id.Map.find id !reserve_table in
-    user_err_loc(loc,"declare_reserved_type",
-    (pr_id id++str" is already bound to a type"))
+    user_err ~loc "declare_reserved_type"
+    ((pr_id id++str" is already bound to a type"))
   with Not_found -> () end;
   add_anonymous_leaf (in_reserved (id,t))
 
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 478774219e..08425129b9 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -46,7 +46,7 @@ let locate_global_with_alias ?(head=false) (loc,qid) =
     if head then global_of_extended_global_head ref
     else global_of_extended_global ref
   with Not_found ->
-    user_err_loc (loc,"",pr_qualid qid ++
+    user_err ~loc "" (pr_qualid qid ++
       str " is bound to a notation that does not denote a reference.")
 
 let global_inductive_with_alias r =
@@ -54,14 +54,14 @@ let global_inductive_with_alias r =
   try match locate_global_with_alias lqid with
   | IndRef ind -> ind
   | ref ->
-      user_err_loc (loc_of_reference r,"global_inductive",
-        pr_reference r ++ spc () ++ str "is not an inductive type.")
-  with Not_found -> Nametab.error_global_not_found_loc loc qid
+      user_err ~loc:(loc_of_reference r) "global_inductive"
+        (pr_reference r ++ spc () ++ str "is not an inductive type.")
+  with Not_found -> Nametab.error_global_not_found ~loc qid
 
 let global_with_alias ?head r =
   let (loc,qid as lqid) = qualid_of_reference r in
   try locate_global_with_alias ?head lqid
-  with Not_found -> Nametab.error_global_not_found_loc loc qid
+  with Not_found -> Nametab.error_global_not_found ~loc qid
 
 let smart_global ?head = function
   | AN r ->
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 2b860173a6..ed44e66ffd 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -32,8 +32,8 @@ let _ = Goptions.declare_bool_option {
 (**********************************************************************)
 (* Miscellaneous *)
 
-let error_invalid_pattern_notation loc =
-  user_err_loc (loc,"",str "Invalid notation for pattern.")
+let error_invalid_pattern_notation ?loc =
+  user_err ?loc "" (str "Invalid notation for pattern.")
 
 (**********************************************************************)
 (* Functions on constr_expr *)
@@ -175,8 +175,8 @@ let split_at_annot bl na =
 	| LocalRawDef _ as x :: rest -> aux (x :: acc) rest
         | LocalPattern _ :: rest -> assert false
 	| [] ->
-            user_err_loc(loc,"",
-			 str "No parameter named " ++ Nameops.pr_id id ++ str".")
+            user_err ~loc ""
+			 (str "No parameter named " ++ Nameops.pr_id id ++ str".")
       in aux [] bl
 
 (* Used in correctness and interface *)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 58edd4ddf8..ac98331c6b 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -46,4 +46,4 @@ val patntn_loc :
 
 (** For cases pattern parsing errors *)
 
-val error_invalid_pattern_notation : Loc.t -> 'a
+val error_invalid_pattern_notation : ?loc:Loc.t -> 'a