Stream: Coq users

Topic: Q on coercions defined in modules

view this post on Zulip Julio Di Egidio (Jan 12 2024 at 17:52):

I have sees that coercions defined in a module are not "active" unless the module is imported. Is there any way to have coercions defined in a module "active" if the module is only required, not imported?

Last updated: Oct 13 2024 at 01:02 UTC