aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr_ops.ml16
-rw-r--r--interp/constrextern.ml4
-rw-r--r--interp/constrintern.ml129
-rw-r--r--interp/coqlib.ml2
-rw-r--r--interp/implicit_quantifiers.ml16
-rw-r--r--interp/modintern.ml8
-rw-r--r--interp/notation.ml30
-rw-r--r--interp/notation_ops.ml16
-rw-r--r--interp/reserve.ml8
-rw-r--r--interp/smartlocate.ml10
-rw-r--r--interp/syntax_def.ml2
-rw-r--r--interp/topconstr.ml8
-rw-r--r--interp/topconstr.mli2
13 files changed, 125 insertions, 126 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 04429851fd..59c24900d2 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 ~hdr:"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)
+ ~hdr:"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) ~hdr:"coerce_to_name"
+ (str "This expression should be a name.")
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e71daef999..f7fcbb4eed 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) ~hdr:"encode_record"
+ (str "This type is not a structure type.");
indsp
module PrintingRecordRecord =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 30016dedcf..630f8d1402 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 ~hdr:"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:
@@ -366,19 +366,19 @@ let check_hidden_implicit_parameters id impls =
| (Inductive indparams,_,_,_) -> Id.List.mem id indparams
| _ -> false) impls
then
- errorlabstrm "" (strbrk "A parameter of an inductive type " ++
+ user_err (strbrk "A parameter of an inductive type " ++
pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.")
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 ~hdr:"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 ~hdr:"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 ~hdr:"find_constructor" error
in
cstr, match add_params with
| Some nb_args ->
@@ -1083,8 +1083,8 @@ let sort_fields ~complete loc fields completer =
let gr = global_reference_of_reference first_field_ref in
(gr, Recordops.find_projection gr)
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) ~hdr:"intern"
+ (pr_reference first_field_ref ++ str": Not a projection")
in
(* the number of parameters *)
let nparams = record.Recordops.s_EXPECTEDPARAM in
@@ -1113,7 +1113,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
@@ -1126,7 +1126,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
@@ -1140,15 +1140,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) ~hdr:"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)
| [] ->
@@ -1219,7 +1218,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
@@ -1344,8 +1343,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
@@ -1360,7 +1359,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 =
@@ -1412,11 +1411,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
@@ -1424,8 +1423,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 *)
@@ -1464,10 +1463,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) ->
@@ -1477,11 +1476,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)
@@ -1532,7 +1531,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 ->
@@ -1636,7 +1635,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 ~hdr:"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
@@ -1859,7 +1858,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"."));
[]
@@ -1890,8 +1889,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 ~hdr:"internalize"
+ (explain_internalization_error e)
(**************************************************************************)
(* Functions to translate constr_expr into glob_constr *)
@@ -1930,7 +1929,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 ~hdr:"internalize" (explain_internalization_error e)
(*********************************************************************)
@@ -2041,13 +2040,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 ~hdr:"internalize" (explain_internalization_error e)
let interp_rawcontext_evars env evdref k bl =
let (env, par, _, impls) =
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 588637b76e..9539980f04 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -86,7 +86,7 @@ let check_required_library d =
(Loc.ghost,make_qualid (DirPath.make (List.rev prefix)) m)
*)
(* or failing ...*)
- errorlabstrm "Coqlib.check_required_library"
+ user_err ~hdr:"Coqlib.check_required_library"
(str "Library " ++ pr_dirpath dir ++ str " has to be required first.")
(************************************************************************)
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 4d9386b9da..bfa01532fd 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -29,12 +29,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 ~hdr:"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 ~hdr:"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 =
@@ -80,8 +80,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 ~hdr:"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 =
@@ -205,7 +205,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
@@ -239,7 +239,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 6279622bf9..29d1f01eb9 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -98,7 +98,7 @@ let declare_scope scope =
scope_map := String.Map.add scope empty_scope !scope_map
let error_unknown_scope sc =
- errorlabstrm "Notation"
+ user_err ~hdr:"Notation"
(str "Scope " ++ str sc ++ str " is not declared.")
let find_scope scope =
@@ -211,7 +211,7 @@ let remove_delimiters scope =
let sc = find_scope scope in
let newsc = { sc with delimiters = None } in
match sc.delimiters with
- | None -> CErrors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".")
+ | None -> CErrors.user_err (str "No bound key for scope " ++ str scope ++ str ".")
| Some key ->
scope_map := String.Map.add scope newsc !scope_map;
try
@@ -223,8 +223,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 ~hdr:"find_delimiters"
+ (str "Unknown scope delimiting key " ++ str key ++ str ".")
(* Uninterpretation tables *)
@@ -340,8 +340,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 ~hdr:"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 *)
@@ -461,8 +461,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 ~hdr:"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 ".")
@@ -486,8 +486,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)
@@ -893,11 +893,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 =
@@ -1020,8 +1020,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 ~hdr:"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 fcb4a345e2..af87aae1b6 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -242,8 +242,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'
@@ -292,8 +292,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) ||
@@ -333,8 +333,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
@@ -386,7 +386,7 @@ let check_variables nenv (found,foundrec,foundrecbinding) =
let vars = Id.Map.filter filter nenv.ninterp_var_type in
let check_recvar x =
if Id.List.mem x found then
- errorlabstrm "" (pr_id x ++
+ user_err (pr_id x ++
strbrk " should only be used in the recursive part of a pattern.") in
let check (x, y) = check_recvar x; check_recvar y in
let () = List.iter check foundrec in
@@ -405,7 +405,7 @@ let check_variables nenv (found,foundrec,foundrecbinding) =
in
let check_pair s x y where =
if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then
- errorlabstrm "" (strbrk "in the right-hand side, " ++ pr_id x ++
+ user_err (strbrk "in the right-hand side, " ++ pr_id x ++
str " and " ++ pr_id y ++ strbrk " should appear in " ++ str s ++
str " position as part of a recursive pattern.") in
let check_type x typ =
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 388ca08050..a4d4f40277 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 ~hdr:"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 ~hdr:"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..178c1c1f96 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) ~hdr:"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/syntax_def.ml b/interp/syntax_def.ml
index d2dcbd92aa..870b4bbcf6 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -30,7 +30,7 @@ let add_syntax_constant kn c onlyparse =
let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
if Nametab.exists_cci sp then
- errorlabstrm "cache_syntax_constant"
+ user_err ~hdr:"cache_syntax_constant"
(pr_id (basename sp) ++ str " already exists");
add_syntax_constant kn pat onlyparse;
Nametab.push_syndef (Nametab.Until i) sp kn
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 2b860173a6..0f894019b0 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:32:32 +0000