aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/classes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/classes.ml')
-rw-r--r--toplevel/classes.ml7
1 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 6d62ce24a..cff744534 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -66,8 +66,9 @@ 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)
+ ~hdr:"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
@@ -169,7 +170,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
Name id ->
let sp = Lib.make_path id in
if Nametab.exists_cci sp then
- user_err "new_instance" (Nameops.pr_id id ++ Pp.str " already exists.");
+ user_err ~hdr:"new_instance" (Nameops.pr_id id ++ Pp.str " already exists.");
id
| Anonymous ->
let i = Nameops.add_suffix (id_of_class k) "_instance_0" in