Stream: Coq devs & plugin devs

Topic: Locality for Declare ML Module

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".

Ali Caglayan (Jun 08 2022 at 20:08):

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

Gaëtan Gilbert (Jun 08 2022 at 20:12):

Global is default
Local is module local

Gaëtan Gilbert (Jun 08 2022 at 20:12):

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

Last updated: Feb 05 2023 at 21:03 UTC