Stream: Coq users

Topic: ✔ Global Hint Extern

view this post on Zulip Marco Molè (May 11 2023 at 16:25):

Is there a way to declare a Hint Extern inside a section, but with a global scope?

view this post on Zulip Gaëtan Gilbert (May 11 2023 at 16:36):

no

view this post on Zulip Marco Molè (May 11 2023 at 16:55):

ok thanks!

view this post on Zulip Notification Bot (May 11 2023 at 16:55):

Marco Molè has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC