From 2826683746569b9d78aa01e319315ab554e1619b Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 19:36:45 +0200 Subject: Fix omitted labels in function calls --- vernac/class.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac/class.ml') diff --git a/vernac/class.ml b/vernac/class.ml index 95114ec39..104f3c1db 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -311,7 +311,7 @@ let add_coercion_hook poly local ref = | Global -> false | Discharge -> assert false in - let () = try_add_new_coercion ref stre poly in + let () = try_add_new_coercion ref ~local:stre poly in let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in Flags.if_verbose Feedback.msg_info msg @@ -324,6 +324,6 @@ let add_subclass_hook poly local ref = | Discharge -> assert false in let cl = class_of_global ref in - try_add_new_coercion_subclass cl stre poly + try_add_new_coercion_subclass cl ~local:stre poly let add_subclass_hook poly = Lemmas.mk_hook (add_subclass_hook poly) -- cgit v1.2.3