diff options
Diffstat (limited to 'vernac/class.ml')
| -rw-r--r-- | vernac/class.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/vernac/class.ml b/vernac/class.ml index febe8e34e4..6dba134764 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -355,27 +355,27 @@ let try_add_new_identity_coercion id ~local ~poly ~source ~target = let try_add_new_coercion_with_source ref ~local ~poly ~source = try_add_new_coercion_core ref ~local poly (Some source) None false -let add_coercion_hook poly _uctx _trans local ref = +let add_coercion_hook poly { DeclareDef.Hook.S.scope; dref; _ } = let open DeclareDef in - let local = match local with + let local = match scope with | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *) | Global ImportNeedQualified -> true | Global ImportDefaultBehavior -> false in - let () = try_add_new_coercion ref ~local ~poly in - let msg = Nametab.pr_global_env Id.Set.empty ref ++ str " is now a coercion" in + let () = try_add_new_coercion dref ~local ~poly in + let msg = Nametab.pr_global_env Id.Set.empty dref ++ str " is now a coercion" in Flags.if_verbose Feedback.msg_info msg let add_coercion_hook ~poly = DeclareDef.Hook.make (add_coercion_hook poly) -let add_subclass_hook ~poly _uctx _trans local ref = +let add_subclass_hook ~poly { DeclareDef.Hook.S.scope; dref; _ } = let open DeclareDef in - let stre = match local with + let stre = match scope with | Discharge -> assert false (* Local Subclass in section behaves like Local Definition *) | Global ImportNeedQualified -> true | Global ImportDefaultBehavior -> false in - let cl = class_of_global ref in + let cl = class_of_global dref in try_add_new_coercion_subclass cl ~local:stre ~poly let add_subclass_hook ~poly = DeclareDef.Hook.make (add_subclass_hook ~poly) |