diff options
Diffstat (limited to 'toplevel/record.ml')
| -rw-r--r-- | toplevel/record.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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 |