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: Jun 18 2024 at 22:01 UTC