Stream: Coq devs & plugin devs

Topic: Locality for Declare ML Module


view this post on Zulip Ali Caglayan (Jun 08 2022 at 20:05):

Do these do anything?

#[global] Declare ML Module "ltac_plugin".
#[local] Declare ML Module "ltac_plugin".
Local Declare ML Module "ltac_plugin".
Global Declare ML Module "ltac_plugin".

view this post on Zulip Ali Caglayan (Jun 08 2022 at 20:08):

I'm under the impression that they are all equivalent.

view this post on Zulip Gaëtan Gilbert (Jun 08 2022 at 20:12):

Global is default
Local is module local

view this post on Zulip Gaëtan Gilbert (Jun 08 2022 at 20:12):

Local is also possibly buggy as I don't think anyone uses it


Last updated: Dec 06 2023 at 14:01 UTC