aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/classes.ml4
-rw-r--r--toplevel/command.ml18
-rw-r--r--toplevel/obligations.ml4
-rw-r--r--toplevel/record.ml8
-rw-r--r--toplevel/vernac.ml2
-rw-r--r--toplevel/vernacentries.ml23
6 files changed, 29 insertions, 30 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index d6a6162f9..26cb7451a 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -66,8 +66,8 @@ let existing_instance glob g pri =
match class_of_constr r with
| Some (_, ((tc,u), _)) -> add_instance (new_instance tc pri glob
(*FIXME*) (Flags.use_polymorphic_flag ()) c)
- | None -> user_err_loc (loc_of_reference g, "declare_instance",
- Pp.str "Constant does not build instances of a declared type class.")
+ | None -> user_err ~loc:(loc_of_reference g) "declare_instance"
+ (Pp.str "Constant does not build instances of a declared type class.")
let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
let mismatched_props env n m = mismatched_ctx_inst env Properties n m
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 097865648..b9a72fa33 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -57,8 +57,8 @@ let rec complete_conclusion a cs = function
| CHole (loc, k, _, _) ->
let (has_no_args,name,params) = a in
if not has_no_args then
- user_err_loc (loc,"",
- strbrk"Cannot infer the non constant arguments of the conclusion of "
+ user_err ~loc ""
+ (strbrk"Cannot infer the non constant arguments of the conclusion of "
++ pr_id cs ++ str ".");
let args = List.map (fun id -> CRef(Ident(loc,id),None)) params in
CAppExpl (loc,(None,Ident(loc,name),None),List.rev args)
@@ -330,7 +330,7 @@ let do_assumptions kind nl l = match l with
| (Discharge, _, _) when Lib.sections_are_opened () ->
let loc = fst id in
let msg = Pp.str "Section variables cannot be polymorphic." in
- user_err_loc (loc, "", msg)
+ user_err ~loc "" msg
| _ -> ()
in
do_assumptions_bound_univs coe kind nl id (Some pl) c
@@ -342,7 +342,7 @@ let do_assumptions kind nl l = match l with
let loc = fst id in
let msg =
Pp.str "Assumptions with bound universes can only be defined one at a time." in
- user_err_loc (loc, "", msg)
+ user_err ~loc "" msg
in
(coe, (List.map map idl, c))
in
@@ -438,7 +438,7 @@ let interp_ind_arity env evdref ind =
let t, impls = understand_tcc_evars env evdref ~expected_type:IsType c, imps in
let pseudo_poly = check_anonymous_type c in
let () = if not (Reduction.is_arity env t) then
- user_err_loc (constr_loc ind.ind_arity, "", str "Not an arity")
+ user_err ~loc:(constr_loc ind.ind_arity) "" (str "Not an arity")
in
t, pseudo_poly, impls
@@ -553,7 +553,7 @@ let check_named (loc, na) = match na with
| Name _ -> ()
| Anonymous ->
let msg = str "Parameters must be named." in
- user_err_loc (loc, "", msg)
+ user_err ~loc "" msg
let check_param = function
@@ -954,9 +954,9 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let relty = Typing.unsafe_type_of env !evdref rel in
let relargty =
let error () =
- user_err_loc (constr_loc r,
- "Command.build_wellfounded",
- Printer.pr_constr_env env !evdref rel ++ str " is not an homogeneous binary relation.")
+ user_err ~loc:(constr_loc r)
+ "Command.build_wellfounded"
+ (Printer.pr_constr_env env !evdref rel ++ str " is not an homogeneous binary relation.")
in
try
let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 29d745732..38d4a62b4 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -34,7 +34,7 @@ let check_evars env evm =
| Evar_kinds.QuestionMark _
| Evar_kinds.ImplicitArg (_,_,false) -> ()
| _ ->
- Pretype_errors.error_unsolvable_implicit loc env evm key None)
+ Pretype_errors.error_unsolvable_implicit ~loc env evm key None)
(Evd.undefined_map evm)
type oblinfo =
@@ -985,7 +985,7 @@ and solve_obligation_by_tac prg obls i tac =
let (e, _) = CErrors.push e in
match e with
| Refiner.FailError (_, s) ->
- user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
+ user_err ~loc:(fst obl.obl_location) "solve_obligation" (Lazy.force s)
| e -> None (* FIXME really ? *)
and solve_prg_obligations prg ?oblset tac =
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 71d070776..6a64b0d66 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -102,7 +102,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
let error bk (loc, name) =
match bk, name with
| Default _, Anonymous ->
- user_err_loc (loc, "record", str "Record parameters must be named")
+ user_err ~loc "record" (str "Record parameters must be named")
| _ -> ()
in
List.iter
@@ -127,7 +127,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
sred, true
| None -> s, false
else s, false)
- | _ -> user_err_loc (constr_loc t,"", str"Sort expected."))
+ | _ -> user_err ~loc:(constr_loc t) "" (str"Sort expected."))
| None ->
let uvarkind = Evd.univ_flexible_alg in
mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), true
@@ -539,8 +539,8 @@ let declare_existing_class g =
match g with
| ConstRef x -> add_constant_class x
| IndRef x -> add_inductive_class x
- | _ -> user_err_loc (Loc.dummy_loc, "declare_existing_class",
- Pp.str"Unsupported class type, only constants and inductives are allowed")
+ | _ -> user_err "declare_existing_class"
+ (Pp.str"Unsupported class type, only constants and inductives are allowed")
open Vernacexpr
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index f83ada466..00655497b 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -70,7 +70,7 @@ let disable_drop = function
| Drop -> CErrors.error "Drop is forbidden."
| e -> e
-let user_error loc s = CErrors.user_err_loc (loc,"_",str s)
+let user_error loc s = CErrors.user_err ~loc "_" (str s)
(* Opening and closing a channel. Open it twice when verbose: the first
channel is used to read the commands, and the second one to print them.
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f69c4fa18..3f784fd8a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -380,9 +380,9 @@ let err_unmapped_library loc ?from qid =
| Some from ->
str " and prefix " ++ pr_dirpath from ++ str "."
in
- user_err_loc
- (loc,"locate_library",
- strbrk "Cannot find a physical path bound to logical path matching suffix " ++
+ user_err ~loc
+ "locate_library"
+ (strbrk "Cannot find a physical path bound to logical path matching suffix " ++
pr_dirpath dir ++ prefix)
let err_notfound_library loc ?from qid =
@@ -391,9 +391,8 @@ let err_notfound_library loc ?from qid =
| Some from ->
str " with prefix " ++ pr_dirpath from ++ str "."
in
- user_err_loc
- (loc,"locate_library",
- strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix)
+ user_err ~loc "locate_library"
+ (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix)
let print_located_library r =
let (loc,qid) = qualid_of_reference r in
@@ -605,15 +604,15 @@ let vernac_combined_scheme lid l =
let vernac_universe loc poly l =
if poly && not (Lib.sections_are_opened ()) then
- user_err_loc (loc, "vernac_universe",
- str"Polymorphic universes can only be declared inside sections, " ++
+ user_err ~loc "vernac_universe"
+ (str"Polymorphic universes can only be declared inside sections, " ++
str "use Monomorphic Universe instead");
do_universe poly l
let vernac_constraint loc poly l =
if poly && not (Lib.sections_are_opened ()) then
- user_err_loc (loc, "vernac_constraint",
- str"Polymorphic universe constraints can only be declared"
+ user_err ~loc "vernac_constraint"
+ (str"Polymorphic universe constraints can only be declared"
++ str " inside sections, use Monomorphic Constraint instead");
do_constraint poly l
@@ -1575,8 +1574,8 @@ let global_module r =
let (loc,qid) = qualid_of_reference r in
try Nametab.full_name_module qid
with Not_found ->
- user_err_loc (loc, "global_module",
- str "Module/section " ++ pr_qualid qid ++ str " not found.")
+ user_err ~loc "global_module"
+ (str "Module/section " ++ pr_qualid qid ++ str " not found.")
let interp_search_restriction = function
| SearchOutside l -> (List.map global_module l, true)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 15:07:09 +0000