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: Jun 20 2024 at 13:02 UTC